# . * 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-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 tactic.default_tactic=smt 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 | 399.932s | 10.907GiB| sat | 0 | | | |scrambled88927.smt2 | 416.404s | 281.0MiB| unsat | 0 | | | |scrambled122587.smt2 | 537.268s | 542.0MiB| unsat | 0 | | | |scrambled102680.smt2 | 653.192s | 11.632GiB| sat | 0 | | | |scrambled124681.smt2 | 1200.048s | 298.0MiB| timeout | 0 | | | |scrambled92964.smt2 | 1200.054s | 377.0MiB| timeout | 0 | | | |scrambled46192.smt2 | 1200.087s | 524.0MiB| timeout | 0 | | | |scrambled103576.smt2 | 1200.091s | 304.0MiB| timeout | 0 | | | |scrambled76532.smt2 | 1200.092s | 580.0MiB| timeout | 0 | | | |scrambled115671.smt2 | 1200.095s | 550.0MiB| timeout | 0 | | | |scrambled35077.smt2 | 1200.098s | 583.0MiB| timeout | 0 | | | |scrambled31085.smt2 | 1200.100s | 446.0MiB| timeout | 0 | | | |scrambled101086.smt2 | 1200.110s | 560.0MiB| timeout | 0 | | | |scrambled104811.smt2 | 1200.113s | 408.0MiB| timeout | 0 | | | |scrambled65517.smt2 | 1200.115s | 641.0MiB| timeout | 0 | | | |scrambled77308.smt2 | 1200.122s | 405.0MiB| timeout | 0 | | | |scrambled49820.smt2 | 1200.125s | 560.0MiB| timeout | 0 | | | |scrambled71015.smt2 | 1200.171s | 1324.0MiB| timeout | 0 | | | |scrambled55845.smt2 | 1200.332s | 1518.0MiB| timeout | 0 | | | |scrambled17583.smt2 | 1200.341s | 3217.0MiB| timeout | 0 | | | |scrambled76525.smt2 | 1200.353s | 2894.0MiB| timeout | 0 | | | |scrambled59368.smt2 | 1200.418s | 2900.0MiB| timeout | 0 | | | |scrambled124455.smt2 | 1200.443s | 3675.0MiB| timeout | 0 | | | |scrambled47581.smt2 | 1200.507s | 3346.0MiB| timeout | 0 | | | |scrambled95284.smt2 | 1200.573s | 4650.0MiB| timeout | 0 | | | |scrambled37260.smt2 | 1200.583s | 5060.0MiB| timeout | 0 | | | |scrambled77008.smt2 | 1200.840s | 7601.0MiB| timeout | 0 | | | |scrambled117897.smt2 | 1200.861s | 5954.0MiB| timeout | 0 | | | |scrambled101728.smt2 | 1201.026s | 10.395GiB| timeout | 0 | | | |scrambled8163.smt2 | 1201.036s | 11.047GiB| timeout | 0 | | | |scrambled109307.smt2 | 1201.073s | 8390.0MiB| timeout | 0 | | | |scrambled102621.smt2 | 1201.164s | 12.903GiB| timeout | 0 | | | |scrambled55850.smt2 | 1201.194s | 12.304GiB| timeout | 0 | | | |scrambled13169.smt2 | 1201.227s | 10.778GiB| timeout | 0 | | | |scrambled25695.smt2 | 1201.237s | 13.412GiB| timeout | 0 | | | |scrambled111949.smt2 | 1201.514s | 16.297GiB| timeout | 0 | | | |scrambled98986.smt2 | 1201.573s | 12.377GiB| timeout | 0 | | | |scrambled13209.smt2 | 1201.886s | 20.963GiB| timeout | 0 | | |