# . * SAT 1 * UNSAT 2 * TIMEOUT 35 * 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
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_LRA
Z3 commit message: Merge branch 'master' of github.com:Z3Prover/z3 into core_min
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled122587.smt2 | 104.693s | 509.0MiB| unsat | 0 | | | |scrambled44527.smt2 | 422.766s | 12.532GiB| sat | 0 | | | |scrambled117897.smt2 | 1079.224s | 6854.0MiB| unsat | 0 | | | |scrambled103576.smt2 | 1200.053s | 296.0MiB| timeout | 0 | | | |scrambled65517.smt2 | 1200.065s | 446.0MiB| timeout | 0 | | | |scrambled104811.smt2 | 1200.066s | 376.0MiB| timeout | 0 | | | |scrambled77308.smt2 | 1200.068s | 376.0MiB| timeout | 0 | | | |scrambled124681.smt2 | 1200.069s | 305.0MiB| timeout | 0 | | | |scrambled92964.smt2 | 1200.069s | 381.0MiB| timeout | 0 | | | |scrambled46192.smt2 | 1200.079s | 588.0MiB| timeout | 0 | | | |scrambled88927.smt2 | 1200.086s | 299.0MiB| timeout | 0 | | | |scrambled49820.smt2 | 1200.088s | 556.0MiB| timeout | 0 | | | |scrambled35077.smt2 | 1200.090s | 605.0MiB| timeout | 0 | | | |scrambled101086.smt2 | 1200.096s | 574.0MiB| timeout | 0 | | | |scrambled31085.smt2 | 1200.101s | 479.0MiB| timeout | 0 | | | |scrambled115671.smt2 | 1200.111s | 586.0MiB| timeout | 0 | | | |scrambled76532.smt2 | 1200.147s | 600.0MiB| timeout | 0 | | | |scrambled71015.smt2 | 1200.164s | 1060.0MiB| timeout | 0 | | | |scrambled55845.smt2 | 1200.218s | 1632.0MiB| timeout | 0 | | | |scrambled17583.smt2 | 1200.319s | 2959.0MiB| timeout | 0 | | | |scrambled76525.smt2 | 1200.412s | 3092.0MiB| timeout | 0 | | | |scrambled47581.smt2 | 1200.423s | 3158.0MiB| timeout | 0 | | | |scrambled95284.smt2 | 1200.443s | 3580.0MiB| timeout | 0 | | | |scrambled59368.smt2 | 1200.517s | 2863.0MiB| timeout | 0 | | | |scrambled124455.smt2 | 1200.539s | 4175.0MiB| timeout | 0 | | | |scrambled109307.smt2 | 1200.620s | 6013.0MiB| timeout | 0 | | | |scrambled77008.smt2 | 1200.729s | 6275.0MiB| timeout | 0 | | | |scrambled37260.smt2 | 1200.780s | 6465.0MiB| timeout | 0 | | | |scrambled55850.smt2 | 1201.012s | 10.455GiB| timeout | 0 | | | |scrambled13169.smt2 | 1201.051s | 11.659GiB| timeout | 0 | | | |scrambled8163.smt2 | 1201.088s | 11.264GiB| timeout | 0 | | | |scrambled25695.smt2 | 1201.136s | 11.231GiB| timeout | 0 | | | |scrambled102680.smt2 | 1201.333s | 13.256GiB| timeout | 0 | | | |scrambled101728.smt2 | 1201.504s | 10.054GiB| timeout | 0 | | | |scrambled102621.smt2 | 1201.506s | 11.457GiB| timeout | 0 | | | |scrambled98986.smt2 | 1201.687s | 10.876GiB| timeout | 0 | | | |scrambled13209.smt2 | 1202.041s | 21.067GiB| timeout | 0 | | | |scrambled111949.smt2 | 1202.383s | 16.061GiB| timeout | 0 | | |