# . * SAT 2 * UNSAT 2 * TIMEOUT 34 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_LRA-timeout20min-bb2-no_default_tactic-auto_config
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=true smt_parallel.num_global_bb_batch_threads=2"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_LRA
Z3 commit message: Merge branch 'master' of github.com:Z3Prover/z3 into core_min
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled44527.smt2 | 388.855s | 10.907GiB| sat | 0 | | | |scrambled122587.smt2 | 441.330s | 527.0MiB| unsat | 0 | | | |scrambled88927.smt2 | 602.302s | 283.0MiB| unsat | 0 | | | |scrambled102680.smt2 | 795.836s | 12.397GiB| sat | 0 | | | |scrambled124681.smt2 | 1200.045s | 299.0MiB| timeout | 0 | | | |scrambled92964.smt2 | 1200.061s | 376.0MiB| timeout | 0 | | | |scrambled104811.smt2 | 1200.082s | 409.0MiB| timeout | 0 | | | |scrambled103576.smt2 | 1200.085s | 312.0MiB| timeout | 0 | | | |scrambled46192.smt2 | 1200.094s | 549.0MiB| timeout | 0 | | | |scrambled115671.smt2 | 1200.103s | 553.0MiB| timeout | 0 | | | |scrambled65517.smt2 | 1200.110s | 630.0MiB| timeout | 0 | | | |scrambled101086.smt2 | 1200.115s | 563.0MiB| timeout | 0 | | | |scrambled35077.smt2 | 1200.115s | 583.0MiB| timeout | 0 | | | |scrambled49820.smt2 | 1200.118s | 546.0MiB| timeout | 0 | | | |scrambled77308.smt2 | 1200.122s | 407.0MiB| timeout | 0 | | | |scrambled31085.smt2 | 1200.137s | 454.0MiB| timeout | 0 | | | |scrambled76532.smt2 | 1200.166s | 582.0MiB| timeout | 0 | | | |scrambled71015.smt2 | 1200.190s | 1347.0MiB| timeout | 0 | | | |scrambled55845.smt2 | 1200.264s | 1565.0MiB| timeout | 0 | | | |scrambled59368.smt2 | 1200.377s | 2896.0MiB| timeout | 0 | | | |scrambled76525.smt2 | 1200.396s | 2955.0MiB| timeout | 0 | | | |scrambled124455.smt2 | 1200.443s | 3731.0MiB| timeout | 0 | | | |scrambled17583.smt2 | 1200.463s | 3407.0MiB| timeout | 0 | | | |scrambled95284.smt2 | 1200.522s | 4782.0MiB| timeout | 0 | | | |scrambled47581.smt2 | 1200.541s | 3327.0MiB| timeout | 0 | | | |scrambled37260.smt2 | 1200.685s | 5018.0MiB| timeout | 0 | | | |scrambled117897.smt2 | 1200.761s | 5729.0MiB| timeout | 0 | | | |scrambled77008.smt2 | 1200.914s | 7636.0MiB| timeout | 0 | | | |scrambled109307.smt2 | 1200.990s | 8324.0MiB| timeout | 0 | | | |scrambled8163.smt2 | 1201.020s | 10.965GiB| timeout | 0 | | | |scrambled101728.smt2 | 1201.112s | 10.615GiB| timeout | 0 | | | |scrambled13169.smt2 | 1201.142s | 10.667GiB| timeout | 0 | | | |scrambled55850.smt2 | 1201.251s | 12.277GiB| timeout | 0 | | | |scrambled102621.smt2 | 1201.310s | 12.884GiB| timeout | 0 | | | |scrambled98986.smt2 | 1201.383s | 12.488GiB| timeout | 0 | | | |scrambled111949.smt2 | 1201.579s | 15.821GiB| timeout | 0 | | | |scrambled25695.smt2 | 1201.848s | 13.282GiB| timeout | 0 | | | |scrambled13209.smt2 | 1202.460s | 21.463GiB| timeout | 0 | | |