# . * SAT 6 * UNSAT 0 * TIMEOUT 38 * 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
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 | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled118793.smt2 | 116.532s | 552.0MiB| sat | 0 | | | |scrambled20101.smt2 | 308.644s | 1027.0MiB| sat | 0 | | | |scrambled125827.smt2 | 505.296s | 605.0MiB| sat | 0 | | | |scrambled95803.smt2 | 514.824s | 1477.0MiB| sat | 0 | | | |scrambled125888.smt2 | 677.504s | 1000.0MiB| sat | 0 | | | |scrambled32836.smt2 | 986.459s | 1591.0MiB| sat | 0 | | | |scrambled45952.smt2 | 1260.016s | 41.54MiB| timeout | 0 | | | |scrambled79766.smt2 | 1260.018s | 42.824MiB| timeout | 0 | | | |scrambled59713.smt2 | 1260.023s | 41.792MiB| timeout | 0 | | | |scrambled3854.smt2 | 1260.026s | 42.828MiB| timeout | 0 | | | |scrambled79867.smt2 | 1260.032s | 42.004MiB| timeout | 0 | | | |scrambled65181.smt2 | 1260.034s | 42.308MiB| timeout | 0 | | | |scrambled39514.smt2 | 1260.044s | 74.612MiB| timeout | 0 | | | |scrambled103783.smt2 | 1260.046s | 42.556MiB| timeout | 0 | | | |scrambled1417.smt2 | 1260.058s | 218.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 1260.286s | 1437.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1260.370s | 2938.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1260.376s | 3106.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1260.399s | 2660.0MiB| timeout | 0 | | | |scrambled72668.smt2 | 1260.420s | 3139.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1260.461s | 3859.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1260.469s | 4064.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1260.473s | 3836.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1260.506s | 3058.0MiB| timeout | 0 | | | |scrambled25238.smt2 | 1260.538s | 4459.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1260.635s | 5899.0MiB| timeout | 0 | | | |scrambled61922.smt2 | 1260.668s | 5772.0MiB| timeout | 0 | | | |scrambled107115.smt2 | 1260.851s | 9046.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1260.958s | 7086.0MiB| timeout | 0 | | | |scrambled27843.smt2 | 1261.154s | 11.597GiB| timeout | 0 | | | |scrambled107826.smt2 | 1261.515s | 15.255GiB| timeout | 0 | | | |scrambled19335.smt2 | 1261.609s | 16.465GiB| timeout | 0 | | | |scrambled43577.smt2 | 1261.618s | 16.17GiB| timeout | 0 | | | |scrambled75189.smt2 | 1261.802s | 17.942GiB| timeout | 0 | | | |scrambled111627.smt2 | 1261.889s | 19.996GiB| timeout | 0 | | | |scrambled79760.smt2 | 1262.038s | 23.011GiB| timeout | 0 | | | |scrambled108840.smt2 | 1262.267s | 23.36GiB| timeout | 0 | | | |scrambled68944.smt2 | 1262.347s | 25.149GiB| timeout | 0 | | | |scrambled4198.smt2 | 1262.362s | 25.723GiB| timeout | 0 | | | |scrambled102166.smt2 | 1262.380s | 24.742GiB| timeout | 0 | | | |scrambled55680.smt2 | 1262.487s | 26.432GiB| timeout | 0 | | | |scrambled4299.smt2 | 1262.697s | 27.439GiB| timeout | 0 | | | |scrambled94658.smt2 | 1262.899s | 32.313GiB| timeout | 0 | | | |scrambled12042.smt2 | 1263.526s | 31.615GiB| timeout | 0 | | |