# . * 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_bb2
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 6b8cb1099d311aac105cfc6fa658466f4ef6af67
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: restore unrelated code to master
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled20101.smt2 | 91.764s | 955.0MiB| sat | 0 | | | |scrambled118793.smt2 | 126.307s | 553.0MiB| sat | 0 | | | |scrambled125888.smt2 | 156.428s | 963.0MiB| sat | 0 | | | |scrambled125827.smt2 | 177.703s | 598.0MiB| sat | 0 | | | |scrambled32836.smt2 | 541.981s | 1553.0MiB| sat | 0 | | | |scrambled25238.smt2 | 619.836s | 4260.0MiB| sat | 0 | | | |scrambled72668.smt2 | 1186.352s | 3138.0MiB| sat | 0 | | | |scrambled3854.smt2 | 1260.021s | 42.772MiB| timeout | 0 | | | |scrambled79766.smt2 | 1260.021s | 42.556MiB| timeout | 0 | | | |scrambled59713.smt2 | 1260.025s | 41.788MiB| timeout | 0 | | | |scrambled45952.smt2 | 1260.027s | 42.076MiB| timeout | 0 | | | |scrambled65181.smt2 | 1260.031s | 42.568MiB| timeout | 0 | | | |scrambled79867.smt2 | 1260.032s | 41.796MiB| timeout | 0 | | | |scrambled1417.smt2 | 1260.052s | 223.0MiB| timeout | 0 | | | |scrambled103783.smt2 | 1260.060s | 42.336MiB| timeout | 0 | | | |scrambled39514.smt2 | 1260.061s | 74.676MiB| timeout | 0 | | | |scrambled51053.smt2 | 1260.186s | 1435.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1260.341s | 2704.0MiB| timeout | 0 | | | |scrambled95803.smt2 | 1260.386s | 1514.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1260.400s | 3901.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1260.406s | 3129.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1260.427s | 2985.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1260.445s | 2950.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1260.496s | 4062.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1260.541s | 5817.0MiB| timeout | 0 | | | |scrambled61922.smt2 | 1260.615s | 5787.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1260.637s | 6759.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1260.765s | 3853.0MiB| timeout | 0 | | | |scrambled107115.smt2 | 1260.869s | 9056.0MiB| timeout | 0 | | | |scrambled27843.smt2 | 1261.121s | 11.603GiB| timeout | 0 | | | |scrambled107826.smt2 | 1261.481s | 15.252GiB| timeout | 0 | | | |scrambled43577.smt2 | 1261.575s | 16.261GiB| timeout | 0 | | | |scrambled75189.smt2 | 1261.720s | 17.943GiB| timeout | 0 | | | |scrambled19335.smt2 | 1261.916s | 16.467GiB| timeout | 0 | | | |scrambled111627.smt2 | 1262.000s | 20.001GiB| timeout | 0 | | | |scrambled108840.smt2 | 1262.058s | 23.371GiB| timeout | 0 | | | |scrambled79760.smt2 | 1262.063s | 23.362GiB| timeout | 0 | | | |scrambled102166.smt2 | 1262.298s | 24.757GiB| timeout | 0 | | | |scrambled4299.smt2 | 1262.409s | 27.447GiB| timeout | 0 | | | |scrambled4198.smt2 | 1262.409s | 25.78GiB| timeout | 0 | | | |scrambled55680.smt2 | 1262.447s | 26.41GiB| timeout | 0 | | | |scrambled68944.smt2 | 1262.591s | 25.419GiB| timeout | 0 | | | |scrambled94658.smt2 | 1262.920s | 32.394GiB| timeout | 0 | | | |scrambled12042.smt2 | 1262.930s | 31.668GiB| timeout | 0 | | |