# . * SAT 7 * UNSAT 0 * TIMEOUT 37 * 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-bb2-newexpand
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 8e294820a0bcdbe59f6282f7a0a3f73f594bd601
Z3 branch: backbones
Z3 options: "-T:1260 -v:0 smt.threads=4 tactic.default_tactic=smt smt.auto_config=false smt_parallel.num_global_bb_threads=2"
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 | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled20101.smt2 | 68.601s | 923.0MiB| sat | 0 | | | |scrambled118793.smt2 | 122.821s | 553.0MiB| sat | 0 | | | |scrambled125888.smt2 | 168.393s | 968.0MiB| sat | 0 | | | |scrambled32836.smt2 | 413.999s | 1549.0MiB| sat | 0 | | | |scrambled125827.smt2 | 476.205s | 606.0MiB| sat | 0 | | | |scrambled95803.smt2 | 909.609s | 1504.0MiB| sat | 0 | | | |scrambled25238.smt2 | 1118.957s | 4415.0MiB| sat | 0 | | | |scrambled65181.smt2 | 1260.014s | 42.304MiB| timeout | 0 | | | |scrambled45952.smt2 | 1260.015s | 41.508MiB| timeout | 0 | | | |scrambled79766.smt2 | 1260.028s | 42.552MiB| timeout | 0 | | | |scrambled3854.smt2 | 1260.029s | 42.308MiB| timeout | 0 | | | |scrambled59713.smt2 | 1260.029s | 42.04MiB| timeout | 0 | | | |scrambled79867.smt2 | 1260.030s | 42.28MiB| timeout | 0 | | | |scrambled39514.smt2 | 1260.039s | 74.676MiB| timeout | 0 | | | |scrambled103783.smt2 | 1260.051s | 42.312MiB| timeout | 0 | | | |scrambled1417.smt2 | 1260.052s | 217.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 1260.228s | 1436.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1260.327s | 2948.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1260.352s | 2680.0MiB| timeout | 0 | | | |scrambled72668.smt2 | 1260.376s | 3133.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1260.392s | 3054.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1260.484s | 3865.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1260.488s | 3127.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1260.499s | 3851.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1260.549s | 5652.0MiB| timeout | 0 | | | |scrambled61922.smt2 | 1260.609s | 5776.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1260.689s | 4047.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1260.758s | 6958.0MiB| timeout | 0 | | | |scrambled107115.smt2 | 1260.858s | 9052.0MiB| timeout | 0 | | | |scrambled27843.smt2 | 1261.232s | 11.61GiB| timeout | 0 | | | |scrambled107826.smt2 | 1261.442s | 15.218GiB| timeout | 0 | | | |scrambled43577.smt2 | 1261.544s | 16.2GiB| timeout | 0 | | | |scrambled19335.smt2 | 1261.651s | 16.45GiB| timeout | 0 | | | |scrambled75189.smt2 | 1261.698s | 17.935GiB| timeout | 0 | | | |scrambled111627.smt2 | 1262.098s | 19.822GiB| timeout | 0 | | | |scrambled108840.smt2 | 1262.184s | 23.383GiB| timeout | 0 | | | |scrambled102166.smt2 | 1262.323s | 24.727GiB| timeout | 0 | | | |scrambled4198.smt2 | 1262.375s | 25.752GiB| timeout | 0 | | | |scrambled68944.smt2 | 1262.378s | 25.297GiB| timeout | 0 | | | |scrambled55680.smt2 | 1262.493s | 26.361GiB| timeout | 0 | | | |scrambled4299.smt2 | 1262.512s | 27.482GiB| timeout | 0 | | | |scrambled79760.smt2 | 1262.665s | 22.863GiB| timeout | 0 | | | |scrambled12042.smt2 | 1262.956s | 31.652GiB| timeout | 0 | | | |scrambled94658.smt2 | 1263.880s | 32.378GiB| timeout | 0 | | |