# . * 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_bb1
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=1"
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 | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled118793.smt2 | 111.173s | 466.0MiB| sat | 0 | | | |scrambled125827.smt2 | 165.681s | 505.0MiB| sat | 0 | | | |scrambled20101.smt2 | 167.040s | 820.0MiB| sat | 0 | | | |scrambled125888.smt2 | 318.656s | 823.0MiB| sat | 0 | | | |scrambled32836.smt2 | 560.452s | 1312.0MiB| sat | 0 | | | |scrambled128732.smt2 | 949.638s | 2414.0MiB| sat | 0 | | | |scrambled25238.smt2 | 991.332s | 3700.0MiB| sat | 0 | | | |scrambled103783.smt2 | 1260.013s | 42.696MiB| timeout | 0 | | | |scrambled39514.smt2 | 1260.014s | 74.672MiB| timeout | 0 | | | |scrambled59713.smt2 | 1260.016s | 41.796MiB| timeout | 0 | | | |scrambled45952.smt2 | 1260.025s | 41.54MiB| timeout | 0 | | | |scrambled3854.smt2 | 1260.036s | 42.38MiB| timeout | 0 | | | |scrambled79766.smt2 | 1260.036s | 42.568MiB| timeout | 0 | | | |scrambled79867.smt2 | 1260.038s | 42.188MiB| timeout | 0 | | | |scrambled65181.smt2 | 1260.038s | 42.54MiB| timeout | 0 | | | |scrambled1417.smt2 | 1260.061s | 190.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 1260.180s | 1377.0MiB| timeout | 0 | | | |scrambled95803.smt2 | 1260.197s | 1280.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1260.356s | 2304.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1260.419s | 3255.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1260.447s | 2648.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1260.485s | 2444.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1260.512s | 3232.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1260.577s | 3578.0MiB| timeout | 0 | | | |scrambled72668.smt2 | 1260.596s | 2630.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1260.629s | 4823.0MiB| timeout | 0 | | | |scrambled61922.smt2 | 1260.704s | 5673.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1260.778s | 5576.0MiB| timeout | 0 | | | |scrambled107115.smt2 | 1261.079s | 8882.0MiB| timeout | 0 | | | |scrambled107826.smt2 | 1261.552s | 14.789GiB| timeout | 0 | | | |scrambled27843.smt2 | 1261.591s | 11.349GiB| timeout | 0 | | | |scrambled43577.smt2 | 1261.643s | 15.764GiB| timeout | 0 | | | |scrambled19335.smt2 | 1261.720s | 16.152GiB| timeout | 0 | | | |scrambled111627.smt2 | 1261.756s | 20.312GiB| timeout | 0 | | | |scrambled75189.smt2 | 1261.811s | 17.507GiB| timeout | 0 | | | |scrambled68944.smt2 | 1262.187s | 24.856GiB| timeout | 0 | | | |scrambled79760.smt2 | 1262.364s | 22.812GiB| timeout | 0 | | | |scrambled102166.smt2 | 1262.380s | 24.175GiB| timeout | 0 | | | |scrambled55680.smt2 | 1262.671s | 25.727GiB| timeout | 0 | | | |scrambled4299.smt2 | 1262.742s | 26.869GiB| timeout | 0 | | | |scrambled108840.smt2 | 1262.784s | 22.874GiB| timeout | 0 | | | |scrambled4198.smt2 | 1263.109s | 25.134GiB| timeout | 0 | | | |scrambled12042.smt2 | 1263.119s | 30.92GiB| timeout | 0 | | | |scrambled94658.smt2 | 1263.577s | 31.664GiB| timeout | 0 | | |