# . * 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-bb2-auto_config-ablate
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 00f2b5e671e82aec1f9a4a88741b8e2b10ac0ea1
Z3 branch: 00f2b5e671e82aec1f9a4a88741b8e2b10ac0ea1
Z3 options: "-T:1200 -v:0 smt.threads=8 tactic.default_tactic=smt smt_parallel.num_global_bb_batch_threads=2"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_LIA
Z3 commit message: Merge branch 'master' of github.com:Z3Prover/z3 into core_min
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled125827.smt2 | 40.534s | 934.0MiB| sat | 0 | | | |scrambled25238.smt2 | 86.487s | 3597.0MiB| sat | 0 | | | |scrambled128128.smt2 | 324.730s | 4759.0MiB| sat | 0 | | | |scrambled125888.smt2 | 599.596s | 1608.0MiB| sat | 0 | | | |scrambled20101.smt2 | 686.503s | 1676.0MiB| sat | 0 | | | |scrambled118793.smt2 | 835.515s | 987.0MiB| sat | 0 | | | |scrambled72668.smt2 | 971.956s | 5147.0MiB| sat | 0 | | | |scrambled59713.smt2 | 1200.015s | 41.8MiB| timeout | 0 | | | |scrambled45952.smt2 | 1200.016s | 41.54MiB| timeout | 0 | | | |scrambled79867.smt2 | 1200.030s | 42.044MiB| timeout | 0 | | | |scrambled65181.smt2 | 1200.030s | 42.552MiB| timeout | 0 | | | |scrambled103783.smt2 | 1200.037s | 42.556MiB| timeout | 0 | | | |scrambled39514.smt2 | 1200.040s | 74.7MiB| timeout | 0 | | | |scrambled3854.smt2 | 1200.058s | 42.544MiB| timeout | 0 | | | |scrambled79766.smt2 | 1200.065s | 42.808MiB| timeout | 0 | | | |scrambled1417.smt2 | 1200.116s | 515.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 1200.379s | 2889.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1200.380s | 3232.0MiB| timeout | 0 | | | |scrambled32836.smt2 | 1200.415s | 2634.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1200.471s | 4675.0MiB| timeout | 0 | | | |scrambled95803.smt2 | 1200.473s | 2354.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1200.624s | 5037.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1200.640s | 5949.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1200.644s | 4749.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1200.738s | 7102.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1200.824s | 6364.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1200.831s | 4706.0MiB| timeout | 0 | | | |scrambled61922.smt2 | 1201.097s | 10.755GiB| timeout | 0 | | | |scrambled107115.smt2 | 1201.703s | 17.681GiB| timeout | 0 | | | |scrambled107826.smt2 | 1202.652s | 27.653GiB| timeout | 0 | | | |scrambled75189.smt2 | 1202.898s | 31.477GiB| timeout | 0 | | | |scrambled19335.smt2 | 1202.960s | 32.099GiB| timeout | 0 | | | |scrambled43577.smt2 | 1202.987s | 34.098GiB| timeout | 0 | | | |scrambled27843.smt2 | 1203.136s | 20.818GiB| timeout | 0 | | | |scrambled111627.smt2 | 1203.676s | 37.481GiB| timeout | 0 | | | |scrambled108840.smt2 | 1203.749s | 42.78GiB| timeout | 0 | | | |scrambled79760.smt2 | 1203.831s | 44.157GiB| timeout | 0 | | | |scrambled68944.smt2 | 1204.194s | 46.51GiB| timeout | 0 | | | |scrambled102166.smt2 | 1204.223s | 47.797GiB| timeout | 0 | | | |scrambled4198.smt2 | 1204.327s | 48.976GiB| timeout | 0 | | | |scrambled55680.smt2 | 1204.392s | 50.305GiB| timeout | 0 | | | |scrambled12042.smt2 | 1204.781s | 54.122GiB| timeout | 0 | | | |scrambled4299.smt2 | 1205.217s | 56.475GiB| timeout | 0 | | | |scrambled94658.smt2 | 1205.703s | 62.593GiB| timeout | 0 | | |