# . * SAT 3 * UNSAT 0 * TIMEOUT 41 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_NRA-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_NRA
Z3 commit message: Merge branch 'master' of github.com:Z3Prover/z3 into core_min
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled14368.smt2 | 1.160s | 265.0MiB| sat | 0 | | | |scrambled36539.smt2 | 1.570s | 294.0MiB| sat | 0 | | | |scrambled29556.smt2 | 49.448s | 273.0MiB| sat | 0 | | | |scrambled117944.smt2 | 1200.051s | 327.0MiB| timeout | 0 | | | |scrambled42946.smt2 | 1200.055s | 310.0MiB| timeout | 0 | | | |scrambled34121.smt2 | 1200.055s | 297.0MiB| timeout | 0 | | | |scrambled32269.smt2 | 1200.055s | 305.0MiB| timeout | 0 | | | |scrambled80728.smt2 | 1200.057s | 448.0MiB| timeout | 0 | | | |scrambled100912.smt2 | 1200.058s | 334.0MiB| timeout | 0 | | | |scrambled112083.smt2 | 1200.058s | 349.0MiB| timeout | 0 | | | |scrambled82241.smt2 | 1200.059s | 298.0MiB| timeout | 0 | | | |scrambled7923.smt2 | 1200.062s | 290.0MiB| timeout | 0 | | | |scrambled118224.smt2 | 1200.064s | 468.0MiB| timeout | 0 | | | |scrambled28630.smt2 | 1200.065s | 309.0MiB| timeout | 0 | | | |scrambled18831.smt2 | 1200.066s | 309.0MiB| timeout | 0 | | | |scrambled112144.smt2 | 1200.073s | 325.0MiB| timeout | 0 | | | |scrambled14880.smt2 | 1200.073s | 375.0MiB| timeout | 0 | | | |scrambled7586.smt2 | 1200.073s | 291.0MiB| timeout | 0 | | | |scrambled94768.smt2 | 1200.075s | 441.0MiB| timeout | 0 | | | |scrambled73220.smt2 | 1200.077s | 562.0MiB| timeout | 0 | | | |scrambled74869.smt2 | 1200.083s | 292.0MiB| timeout | 0 | | | |scrambled21647.smt2 | 1200.083s | 347.0MiB| timeout | 0 | | | |scrambled54263.smt2 | 1200.085s | 344.0MiB| timeout | 0 | | | |scrambled117334.smt2 | 1200.087s | 357.0MiB| timeout | 0 | | | |scrambled99534.smt2 | 1200.089s | 436.0MiB| timeout | 0 | | | |scrambled32701.smt2 | 1200.140s | 881.0MiB| timeout | 0 | | | |scrambled58292.smt2 | 1200.201s | 1416.0MiB| timeout | 0 | | | |scrambled85895.smt2 | 1200.211s | 1596.0MiB| timeout | 0 | | | |scrambled94319.smt2 | 1200.225s | 2113.0MiB| timeout | 0 | | | |scrambled65757.smt2 | 1200.388s | 3719.0MiB| timeout | 0 | | | |scrambled27426.smt2 | 1200.394s | 7436.0MiB| timeout | 0 | | | |scrambled70990.smt2 | 1200.447s | 4602.0MiB| timeout | 0 | | | |scrambled41575.smt2 | 1200.462s | 4863.0MiB| timeout | 0 | | | |scrambled61896.smt2 | 1200.473s | 5023.0MiB| timeout | 0 | | | |scrambled124828.smt2 | 1200.479s | 3760.0MiB| timeout | 0 | | | |scrambled60239.smt2 | 1200.526s | 5433.0MiB| timeout | 0 | | | |scrambled121780.smt2 | 1200.573s | 9568.0MiB| timeout | 0 | | | |scrambled6476.smt2 | 1200.666s | 9527.0MiB| timeout | 0 | | | |scrambled78428.smt2 | 1200.716s | 7126.0MiB| timeout | 0 | | | |scrambled91241.smt2 | 1200.946s | 7176.0MiB| timeout | 0 | | | |scrambled114923.smt2 | 1201.643s | 17.476GiB| timeout | 0 | | | |scrambled22492.smt2 | 1201.883s | 20.329GiB| timeout | 0 | | | |scrambled14016.smt2 | 1202.609s | 25.913GiB| timeout | 0 | | | |scrambled5797.smt2 | 1207.376s | 85.716GiB| timeout | 0 | | |