# . * SAT 7 * UNSAT 0 * TIMEOUT 37 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_LIA-timeout20min-bb1
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: c383004968f5bf66a9668a7ae254c83d45ac3afe
Z3 branch: fmcad26_artifact
Z3 options: "-T:1200 -v:0 smt.threads=8 tactic.default_tactic=smt smt.auto_config=false smt_parallel.num_global_bb_batch_threads=1"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_LIA
Z3 commit message: add ablate_backtracking experiment
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled125888.smt2 | 92.745s | 1418.0MiB| sat | 0 | | | |scrambled118793.smt2 | 101.818s | 849.0MiB| sat | 0 | | | |scrambled20101.smt2 | 110.509s | 1475.0MiB| sat | 0 | | | |scrambled25238.smt2 | 197.520s | 5310.0MiB| sat | 0 | | | |scrambled125827.smt2 | 370.759s | 926.0MiB| sat | 0 | | | |scrambled95803.smt2 | 417.284s | 2250.0MiB| sat | 0 | | | |scrambled32836.smt2 | 923.687s | 2408.0MiB| sat | 0 | | | |scrambled59713.smt2 | 1200.016s | 41.7MiB| timeout | 0 | | | |scrambled45952.smt2 | 1200.017s | 42.06MiB| timeout | 0 | | | |scrambled65181.smt2 | 1200.027s | 42.692MiB| timeout | 0 | | | |scrambled79867.smt2 | 1200.028s | 41.788MiB| timeout | 0 | | | |scrambled39514.smt2 | 1200.033s | 74.716MiB| timeout | 0 | | | |scrambled79766.smt2 | 1200.040s | 42.688MiB| timeout | 0 | | | |scrambled103783.smt2 | 1200.040s | 42.912MiB| timeout | 0 | | | |scrambled3854.smt2 | 1200.041s | 43.116MiB| timeout | 0 | | | |scrambled1417.smt2 | 1200.049s | 346.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 1200.300s | 2855.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1200.550s | 4595.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1200.580s | 5840.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1200.609s | 4544.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1200.683s | 4675.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1200.685s | 5782.0MiB| timeout | 0 | | | |scrambled72668.smt2 | 1200.772s | 4850.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1200.777s | 4180.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1200.959s | 8720.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1201.040s | 10.169GiB| timeout | 0 | | | |scrambled7741.smt2 | 1201.127s | 6165.0MiB| timeout | 0 | | | |scrambled61922.smt2 | 1201.173s | 10.707GiB| timeout | 0 | | | |scrambled27843.smt2 | 1202.129s | 20.717GiB| timeout | 0 | | | |scrambled107826.smt2 | 1202.393s | 27.573GiB| timeout | 0 | | | |scrambled107115.smt2 | 1202.428s | 17.528GiB| timeout | 0 | | | |scrambled75189.smt2 | 1202.890s | 31.365GiB| timeout | 0 | | | |scrambled19335.smt2 | 1203.167s | 32.06GiB| timeout | 0 | | | |scrambled43577.smt2 | 1203.261s | 33.847GiB| timeout | 0 | | | |scrambled111627.smt2 | 1203.371s | 37.451GiB| timeout | 0 | | | |scrambled108840.smt2 | 1203.864s | 42.579GiB| timeout | 0 | | | |scrambled79760.smt2 | 1203.917s | 43.896GiB| timeout | 0 | | | |scrambled4198.smt2 | 1204.347s | 48.455GiB| timeout | 0 | | | |scrambled102166.smt2 | 1204.546s | 47.578GiB| timeout | 0 | | | |scrambled12042.smt2 | 1204.775s | 53.827GiB| timeout | 0 | | | |scrambled68944.smt2 | 1204.845s | 46.803GiB| timeout | 0 | | | |scrambled4299.smt2 | 1204.958s | 56.341GiB| timeout | 0 | | | |scrambled55680.smt2 | 1205.675s | 50.069GiB| timeout | 0 | | | |scrambled94658.smt2 | 1207.195s | 62.059GiB| timeout | 0 | | |