# . * 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_bb0
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=0"
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 | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled25238.smt2 | 98.525s | 1962.0MiB| sat | 0 | | | |scrambled118793.smt2 | 132.075s | 371.0MiB| sat | 0 | | | |scrambled20101.smt2 | 144.469s | 646.0MiB| sat | 0 | | | |scrambled125827.smt2 | 212.884s | 408.0MiB| sat | 0 | | | |scrambled125888.smt2 | 356.992s | 654.0MiB| sat | 0 | | | |scrambled32836.smt2 | 421.318s | 1001.0MiB| sat | 0 | | | |scrambled59713.smt2 | 1260.023s | 41.848MiB| timeout | 0 | | | |scrambled45952.smt2 | 1260.023s | 41.9MiB| timeout | 0 | | | |scrambled65181.smt2 | 1260.024s | 42.424MiB| timeout | 0 | | | |scrambled1417.smt2 | 1260.030s | 158.0MiB| timeout | 0 | | | |scrambled39514.smt2 | 1260.040s | 74.536MiB| timeout | 0 | | | |scrambled3854.smt2 | 1260.041s | 42.272MiB| timeout | 0 | | | |scrambled79766.smt2 | 1260.041s | 42.556MiB| timeout | 0 | | | |scrambled103783.smt2 | 1260.045s | 42.556MiB| timeout | 0 | | | |scrambled79867.smt2 | 1260.048s | 42.028MiB| timeout | 0 | | | |scrambled55777.smt2 | 1260.183s | 1805.0MiB| timeout | 0 | | | |scrambled95803.smt2 | 1260.228s | 1015.0MiB| timeout | 0 | | | |scrambled72668.smt2 | 1260.304s | 2143.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 1260.307s | 1317.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1260.387s | 2609.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1260.406s | 1989.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1260.408s | 2593.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1260.418s | 2051.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1260.452s | 2109.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1260.465s | 2702.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1260.581s | 3661.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1260.682s | 4528.0MiB| timeout | 0 | | | |scrambled61922.smt2 | 1260.991s | 5563.0MiB| timeout | 0 | | | |scrambled107115.smt2 | 1261.092s | 8692.0MiB| timeout | 0 | | | |scrambled43577.smt2 | 1261.571s | 15.328GiB| timeout | 0 | | | |scrambled107826.smt2 | 1261.626s | 14.247GiB| timeout | 0 | | | |scrambled27843.smt2 | 1261.676s | 11.107GiB| timeout | 0 | | | |scrambled19335.smt2 | 1261.778s | 15.592GiB| timeout | 0 | | | |scrambled111627.smt2 | 1261.863s | 18.954GiB| timeout | 0 | | | |scrambled75189.smt2 | 1261.940s | 17.035GiB| timeout | 0 | | | |scrambled4198.smt2 | 1262.031s | 24.382GiB| timeout | 0 | | | |scrambled79760.smt2 | 1262.342s | 21.921GiB| timeout | 0 | | | |scrambled108840.smt2 | 1262.416s | 22.289GiB| timeout | 0 | | | |scrambled55680.smt2 | 1262.429s | 25.007GiB| timeout | 0 | | | |scrambled68944.smt2 | 1262.489s | 23.399GiB| timeout | 0 | | | |scrambled102166.smt2 | 1262.499s | 23.381GiB| timeout | 0 | | | |scrambled4299.smt2 | 1262.518s | 26.066GiB| timeout | 0 | | | |scrambled12042.smt2 | 1262.828s | 29.83GiB| timeout | 0 | | | |scrambled94658.smt2 | 1263.454s | 31.17GiB| timeout | 0 | | |