# . * SAT 1 * UNSAT 3 * TIMEOUT 41 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_IDL-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.arith.solver=4 smt_parallel.num_global_bb_batch_threads=2"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_IDL
Z3 commit message: Merge branch 'master' of github.com:Z3Prover/z3 into core_min
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled96514.smt2 | 286.984s | 493.0MiB| unsat | 0 | | | |scrambled79181.smt2 | 421.719s | 20.26MiB| unsat | 0 | | | |scrambled62536.smt2 | 722.451s | 554.0MiB| unsat | 0 | | | |scrambled15284.smt2 | 792.602s | 431.0MiB| sat | 0 | | | |scrambled1447.smt2 | 1200.068s | 632.0MiB| timeout | 0 | | | |scrambled23483.smt2 | 1200.069s | 462.0MiB| timeout | 0 | | | |scrambled116992.smt2 | 1200.077s | 548.0MiB| timeout | 0 | | | |scrambled119992.smt2 | 1200.079s | 472.0MiB| timeout | 0 | | | |scrambled41773.smt2 | 1200.090s | 503.0MiB| timeout | 0 | | | |scrambled78432.smt2 | 1200.093s | 731.0MiB| timeout | 0 | | | |scrambled75206.smt2 | 1200.094s | 534.0MiB| timeout | 0 | | | |scrambled100416.smt2 | 1200.096s | 669.0MiB| timeout | 0 | | | |scrambled6373.smt2 | 1200.097s | 523.0MiB| timeout | 0 | | | |scrambled41312.smt2 | 1200.098s | 447.0MiB| timeout | 0 | | | |scrambled1379.smt2 | 1200.098s | 466.0MiB| timeout | 0 | | | |scrambled14967.smt2 | 1200.104s | 662.0MiB| timeout | 0 | | | |scrambled90733.smt2 | 1200.106s | 795.0MiB| timeout | 0 | | | |scrambled98799.smt2 | 1200.108s | 687.0MiB| timeout | 0 | | | |scrambled35345.smt2 | 1200.111s | 529.0MiB| timeout | 0 | | | |scrambled78606.smt2 | 1200.112s | 650.0MiB| timeout | 0 | | | |scrambled89071.smt2 | 1200.114s | 698.0MiB| timeout | 0 | | | |scrambled96733.smt2 | 1200.118s | 777.0MiB| timeout | 0 | | | |scrambled4441.smt2 | 1200.118s | 801.0MiB| timeout | 0 | | | |scrambled109208.smt2 | 1200.121s | 877.0MiB| timeout | 0 | | | |scrambled122413.smt2 | 1200.132s | 580.0MiB| timeout | 0 | | | |scrambled122058.smt2 | 1200.133s | 891.0MiB| timeout | 0 | | | |scrambled9927.smt2 | 1200.136s | 731.0MiB| timeout | 0 | | | |scrambled54073.smt2 | 1200.139s | 663.0MiB| timeout | 0 | | | |scrambled117178.smt2 | 1200.140s | 530.0MiB| timeout | 0 | | | |scrambled21544.smt2 | 1200.151s | 733.0MiB| timeout | 0 | | | |scrambled58720.smt2 | 1200.152s | 654.0MiB| timeout | 0 | | | |scrambled128361.smt2 | 1200.152s | 780.0MiB| timeout | 0 | | | |scrambled42287.smt2 | 1200.156s | 1428.0MiB| timeout | 0 | | | |scrambled103851.smt2 | 1200.157s | 1465.0MiB| timeout | 0 | | | |scrambled15552.smt2 | 1200.157s | 1167.0MiB| timeout | 0 | | | |scrambled62859.smt2 | 1200.159s | 1488.0MiB| timeout | 0 | | | |scrambled38610.smt2 | 1200.160s | 1447.0MiB| timeout | 0 | | | |scrambled97138.smt2 | 1200.164s | 1439.0MiB| timeout | 0 | | | |scrambled41801.smt2 | 1200.173s | 922.0MiB| timeout | 0 | | | |scrambled27577.smt2 | 1200.174s | 1167.0MiB| timeout | 0 | | | |scrambled92133.smt2 | 1200.175s | 1839.0MiB| timeout | 0 | | | |scrambled62810.smt2 | 1200.183s | 1341.0MiB| timeout | 0 | | | |scrambled82743.smt2 | 1200.185s | 830.0MiB| timeout | 0 | | | |scrambled124624.smt2 | 1200.238s | 1468.0MiB| timeout | 0 | | | |scrambled25140.smt2 | 1201.230s | 13.872GiB| timeout | 0 | | |