# . * SAT 0 * UNSAT 0 * TIMEOUT 44 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-4-smtcomp2025-QF_LIA-timeout_20min-vsids-aggressivebacktrack
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 8e294820a0bcdbe59f6282f7a0a3f73f594bd601
Z3 branch: backbones
Z3 options: "-T:60 -v:0 smt.threads=4 tactic.default_tactic=smt smt.auto_config=false"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_LIA
Z3 commit message: backtrack more aggressively in search tree: close matching external targets (i.e. repeat literals on other branches)
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled103783.smt2 | 60.014s | 42.288MiB| timeout | 0 | | | |scrambled65181.smt2 | 60.023s | 42.472MiB| timeout | 0 | | | |scrambled79867.smt2 | 60.024s | 41.832MiB| timeout | 0 | | | |scrambled39514.smt2 | 60.025s | 41.872MiB| timeout | 0 | | | |scrambled59713.smt2 | 60.032s | 41.82MiB| timeout | 0 | | | |scrambled45952.smt2 | 60.036s | 42.036MiB| timeout | 0 | | | |scrambled1417.smt2 | 60.049s | 122.0MiB| timeout | 0 | | | |scrambled3854.smt2 | 60.051s | 42.62MiB| timeout | 0 | | | |scrambled79766.smt2 | 60.052s | 42.304MiB| timeout | 0 | | | |scrambled125888.smt2 | 60.096s | 599.0MiB| timeout | 0 | | | |scrambled118793.smt2 | 60.098s | 357.0MiB| timeout | 0 | | | |scrambled20101.smt2 | 60.101s | 629.0MiB| timeout | 0 | | | |scrambled125827.smt2 | 60.124s | 398.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 60.145s | 999.0MiB| timeout | 0 | | | |scrambled32836.smt2 | 60.174s | 851.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 60.178s | 1190.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 60.203s | 1286.0MiB| timeout | 0 | | | |scrambled72668.smt2 | 60.240s | 1479.0MiB| timeout | 0 | | | |scrambled95803.smt2 | 60.251s | 830.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 60.278s | 1244.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 60.289s | 1419.0MiB| timeout | 0 | | | |scrambled25238.smt2 | 60.306s | 1790.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 60.329s | 1243.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 60.337s | 1466.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 60.372s | 1485.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 60.373s | 1941.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 60.396s | 1767.0MiB| timeout | 0 | | | |scrambled102166.smt2 | 60.410s | 2608.0MiB| timeout | 0 | | | |scrambled94658.smt2 | 60.435s | 3305.0MiB| timeout | 0 | | | |scrambled4299.smt2 | 60.467s | 2164.0MiB| timeout | 0 | | | |scrambled4198.smt2 | 60.472s | 3478.0MiB| timeout | 0 | | | |scrambled61922.smt2 | 60.485s | 3016.0MiB| timeout | 0 | | | |scrambled108840.smt2 | 60.496s | 2271.0MiB| timeout | 0 | | | |scrambled55680.smt2 | 60.564s | 2912.0MiB| timeout | 0 | | | |scrambled12042.smt2 | 60.588s | 3357.0MiB| timeout | 0 | | | |scrambled43577.smt2 | 60.630s | 4663.0MiB| timeout | 0 | | | |scrambled107115.smt2 | 60.634s | 4775.0MiB| timeout | 0 | | | |scrambled107826.smt2 | 60.674s | 5239.0MiB| timeout | 0 | | | |scrambled27843.smt2 | 60.703s | 5114.0MiB| timeout | 0 | | | |scrambled19335.smt2 | 60.709s | 5898.0MiB| timeout | 0 | | | |scrambled79760.smt2 | 60.721s | 5756.0MiB| timeout | 0 | | | |scrambled111627.smt2 | 60.919s | 6798.0MiB| timeout | 0 | | | |scrambled68944.smt2 | 60.958s | 7456.0MiB| timeout | 0 | | | |scrambled75189.smt2 | 61.017s | 7170.0MiB| timeout | 0 | | |