# . * SAT 10 * UNSAT 2 * TIMEOUT 32 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_LIA-timeout20min-bb2-no_default_tactic
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 51b65dd20e8f6976ead894f2a5db45cce220ca6c
Z3 branch: core_min
Z3 options: "-T:1200 -v:0 smt.threads=8 smt.auto_config=false 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 | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled61922.smt2 | 6.726s | 409.0MiB| unsat | 0 | | | |scrambled125888.smt2 | 98.454s | 1670.0MiB| sat | 0 | | | |scrambled125827.smt2 | 104.462s | 990.0MiB| sat | 0 | | | |scrambled118793.smt2 | 166.575s | 965.0MiB| sat | 0 | | | |scrambled131241.smt2 | 166.663s | 4700.0MiB| sat | 0 | | | |scrambled51053.smt2 | 204.661s | 530.0MiB| sat | 0 | | | |scrambled25238.smt2 | 455.798s | 6908.0MiB| sat | 0 | | | |scrambled95803.smt2 | 507.662s | 2391.0MiB| sat | 0 | | | |scrambled20101.smt2 | 609.757s | 1744.0MiB| sat | 0 | | | |scrambled32836.smt2 | 643.753s | 2490.0MiB| sat | 0 | | | |scrambled72668.smt2 | 990.076s | 5247.0MiB| sat | 0 | | | |scrambled19335.smt2 | 1005.549s | 1288.0MiB| unsat | 0 | | | |scrambled3854.smt2 | 1200.017s | 42.9MiB| timeout | 0 | | | |scrambled59713.smt2 | 1200.017s | 42.44MiB| timeout | 0 | | | |scrambled45952.smt2 | 1200.017s | 42.296MiB| timeout | 0 | | | |scrambled103783.smt2 | 1200.035s | 43.34MiB| timeout | 0 | | | |scrambled79766.smt2 | 1200.038s | 43.072MiB| timeout | 0 | | | |scrambled39514.smt2 | 1200.042s | 75.264MiB| timeout | 0 | | | |scrambled65181.smt2 | 1200.043s | 43.288MiB| timeout | 0 | | | |scrambled79867.smt2 | 1200.045s | 42.808MiB| timeout | 0 | | | |scrambled1417.smt2 | 1200.045s | 284.0MiB| timeout | 0 | | | |scrambled27843.smt2 | 1200.110s | 680.0MiB| timeout | 0 | | | |scrambled107115.smt2 | 1200.112s | 641.0MiB| timeout | 0 | | | |scrambled75189.smt2 | 1200.152s | 1099.0MiB| timeout | 0 | | | |scrambled107826.smt2 | 1200.160s | 1162.0MiB| timeout | 0 | | | |scrambled68944.smt2 | 1200.170s | 1144.0MiB| timeout | 0 | | | |scrambled43577.smt2 | 1200.178s | 1183.0MiB| timeout | 0 | | | |scrambled108840.smt2 | 1200.189s | 1571.0MiB| timeout | 0 | | | |scrambled111627.smt2 | 1200.197s | 1293.0MiB| timeout | 0 | | | |scrambled79760.smt2 | 1200.231s | 1749.0MiB| timeout | 0 | | | |scrambled4299.smt2 | 1200.267s | 2116.0MiB| timeout | 0 | | | |scrambled4198.smt2 | 1200.318s | 2767.0MiB| timeout | 0 | | | |scrambled55680.smt2 | 1200.327s | 2772.0MiB| timeout | 0 | | | |scrambled102166.smt2 | 1200.407s | 2935.0MiB| timeout | 0 | | | |scrambled12042.smt2 | 1200.419s | 2866.0MiB| timeout | 0 | | | |scrambled94658.smt2 | 1200.449s | 2881.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1200.670s | 5059.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1200.728s | 6306.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1200.735s | 4477.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1200.762s | 4957.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1200.820s | 4912.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1200.830s | 6905.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1201.307s | 9857.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1201.463s | 9280.0MiB| timeout | 0 | | |