# . * SAT 6 * UNSAT 0 * TIMEOUT 38 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_LIA-timeout20min-bb2-partial_share
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 6045ce393fc70dffef4ebb7a9ce331b9ce5095c6
Z3 branch: 6045ce393fc70dffef4ebb7a9ce331b9ce5095c6
Z3 options: "-T:1200 -v:0 smt.threads=8 tactic.default_tactic=smt smt.auto_config=false smt_parallel.num_global_bb_batch_threads=2"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_LIA
Z3 commit message: change share units ordering
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled20101.smt2 | 133.688s | 1640.0MiB| sat | 0 | | | |scrambled125888.smt2 | 140.458s | 1608.0MiB| sat | 0 | | | |scrambled125827.smt2 | 140.868s | 1010.0MiB| sat | 0 | | | |scrambled25238.smt2 | 213.766s | 5932.0MiB| sat | 0 | | | |scrambled118793.smt2 | 222.419s | 989.0MiB| sat | 0 | | | |scrambled72668.smt2 | 1143.780s | 5271.0MiB| sat | 0 | | | |scrambled3854.smt2 | 1200.014s | 42.296MiB| timeout | 0 | | | |scrambled79867.smt2 | 1200.015s | 41.796MiB| timeout | 0 | | | |scrambled65181.smt2 | 1200.016s | 42.796MiB| timeout | 0 | | | |scrambled59713.smt2 | 1200.016s | 41.792MiB| timeout | 0 | | | |scrambled45952.smt2 | 1200.017s | 41.54MiB| timeout | 0 | | | |scrambled39514.smt2 | 1200.032s | 74.92MiB| timeout | 0 | | | |scrambled103783.smt2 | 1200.039s | 42.804MiB| timeout | 0 | | | |scrambled79766.smt2 | 1200.052s | 43.032MiB| timeout | 0 | | | |scrambled1417.smt2 | 1200.088s | 374.0MiB| timeout | 0 | | | |scrambled95803.smt2 | 1200.330s | 2538.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 1200.394s | 2915.0MiB| timeout | 0 | | | |scrambled32836.smt2 | 1200.495s | 2684.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1200.569s | 4637.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1200.593s | 5200.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1200.626s | 5188.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1200.632s | 6483.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1200.711s | 5052.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1200.761s | 6731.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1200.892s | 9414.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1200.974s | 6432.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1201.142s | 11.042GiB| timeout | 0 | | | |scrambled61922.smt2 | 1201.277s | 10.831GiB| timeout | 0 | | | |scrambled107115.smt2 | 1201.741s | 17.784GiB| timeout | 0 | | | |scrambled27843.smt2 | 1202.586s | 20.887GiB| timeout | 0 | | | |scrambled107826.smt2 | 1202.609s | 27.974GiB| timeout | 0 | | | |scrambled75189.smt2 | 1202.923s | 31.688GiB| timeout | 0 | | | |scrambled111627.smt2 | 1203.735s | 37.746GiB| timeout | 0 | | | |scrambled19335.smt2 | 1203.805s | 32.17GiB| timeout | 0 | | | |scrambled108840.smt2 | 1203.903s | 43.071GiB| timeout | 0 | | | |scrambled43577.smt2 | 1203.916s | 34.289GiB| timeout | 0 | | | |scrambled79760.smt2 | 1204.007s | 44.262GiB| timeout | 0 | | | |scrambled102166.smt2 | 1204.279s | 48.143GiB| timeout | 0 | | | |scrambled68944.smt2 | 1204.447s | 46.888GiB| timeout | 0 | | | |scrambled4198.smt2 | 1204.450s | 48.996GiB| timeout | 0 | | | |scrambled55680.smt2 | 1204.452s | 50.682GiB| timeout | 0 | | | |scrambled12042.smt2 | 1204.892s | 54.502GiB| timeout | 0 | | | |scrambled4299.smt2 | 1204.981s | 56.788GiB| timeout | 0 | | | |scrambled94658.smt2 | 1205.968s | 63.01GiB| timeout | 0 | | |