# . * SAT 2 * UNSAT 0 * TIMEOUT 42 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_NRA-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_NRA
Z3 commit message: Merge branch 'master' of github.com:Z3Prover/z3 into core_min
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled29556.smt2 | 0.658s | 24.812MiB| sat | 0 | | | |scrambled14368.smt2 | 51.481s | 263.0MiB| sat | 0 | | | |scrambled112083.smt2 | 1200.042s | 298.0MiB| timeout | 0 | | | |scrambled73220.smt2 | 1200.046s | 332.0MiB| timeout | 0 | | | |scrambled21647.smt2 | 1200.046s | 355.0MiB| timeout | 0 | | | |scrambled80728.smt2 | 1200.051s | 392.0MiB| timeout | 0 | | | |scrambled28630.smt2 | 1200.059s | 323.0MiB| timeout | 0 | | | |scrambled42946.smt2 | 1200.065s | 306.0MiB| timeout | 0 | | | |scrambled100912.smt2 | 1200.065s | 436.0MiB| timeout | 0 | | | |scrambled82241.smt2 | 1200.067s | 309.0MiB| timeout | 0 | | | |scrambled32269.smt2 | 1200.068s | 301.0MiB| timeout | 0 | | | |scrambled14880.smt2 | 1200.070s | 289.0MiB| timeout | 0 | | | |scrambled74869.smt2 | 1200.072s | 313.0MiB| timeout | 0 | | | |scrambled34121.smt2 | 1200.074s | 379.0MiB| timeout | 0 | | | |scrambled112144.smt2 | 1200.074s | 330.0MiB| timeout | 0 | | | |scrambled117944.smt2 | 1200.078s | 742.0MiB| timeout | 0 | | | |scrambled94768.smt2 | 1200.080s | 447.0MiB| timeout | 0 | | | |scrambled7923.smt2 | 1200.080s | 284.0MiB| timeout | 0 | | | |scrambled54263.smt2 | 1200.081s | 357.0MiB| timeout | 0 | | | |scrambled7586.smt2 | 1200.089s | 297.0MiB| timeout | 0 | | | |scrambled18831.smt2 | 1200.090s | 399.0MiB| timeout | 0 | | | |scrambled99534.smt2 | 1200.109s | 422.0MiB| timeout | 0 | | | |scrambled32701.smt2 | 1200.127s | 868.0MiB| timeout | 0 | | | |scrambled117334.smt2 | 1200.183s | 1192.0MiB| timeout | 0 | | | |scrambled85895.smt2 | 1200.194s | 1550.0MiB| timeout | 0 | | | |scrambled94319.smt2 | 1200.227s | 1829.0MiB| timeout | 0 | | | |scrambled36539.smt2 | 1200.289s | 2131.0MiB| timeout | 0 | | | |scrambled58292.smt2 | 1200.384s | 4173.0MiB| timeout | 0 | | | |scrambled61896.smt2 | 1200.391s | 4362.0MiB| timeout | 0 | | | |scrambled118224.smt2 | 1200.416s | 3368.0MiB| timeout | 0 | | | |scrambled60239.smt2 | 1200.428s | 5684.0MiB| timeout | 0 | | | |scrambled27426.smt2 | 1200.428s | 7711.0MiB| timeout | 0 | | | |scrambled65757.smt2 | 1200.435s | 3643.0MiB| timeout | 0 | | | |scrambled121780.smt2 | 1200.457s | 9619.0MiB| timeout | 0 | | | |scrambled41575.smt2 | 1200.472s | 5273.0MiB| timeout | 0 | | | |scrambled6476.smt2 | 1200.516s | 9580.0MiB| timeout | 0 | | | |scrambled78428.smt2 | 1200.558s | 7341.0MiB| timeout | 0 | | | |scrambled91241.smt2 | 1200.582s | 7185.0MiB| timeout | 0 | | | |scrambled70990.smt2 | 1200.687s | 4772.0MiB| timeout | 0 | | | |scrambled124828.smt2 | 1201.528s | 18.252GiB| timeout | 0 | | | |scrambled114923.smt2 | 1201.619s | 15.167GiB| timeout | 0 | | | |scrambled22492.smt2 | 1202.807s | 33.879GiB| timeout | 0 | | | |scrambled5797.smt2 | 1203.092s | 38.124GiB| timeout | 0 | | | |scrambled14016.smt2 | 1222.154s | 262.0GiB| timeout | 0 | | |