# . * 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
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=false 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.972s | 271.0MiB| sat | 0 | | | |scrambled14368.smt2 | 1.501s | 265.0MiB| sat | 0 | | | |scrambled36539.smt2 | 1.874s | 302.0MiB| sat | 0 | | | |scrambled80728.smt2 | 1200.045s | 316.0MiB| timeout | 0 | | | |scrambled117944.smt2 | 1200.048s | 300.0MiB| timeout | 0 | | | |scrambled32269.smt2 | 1200.048s | 337.0MiB| timeout | 0 | | | |scrambled100912.smt2 | 1200.056s | 322.0MiB| timeout | 0 | | | |scrambled82241.smt2 | 1200.058s | 295.0MiB| timeout | 0 | | | |scrambled42946.smt2 | 1200.062s | 302.0MiB| timeout | 0 | | | |scrambled73220.smt2 | 1200.062s | 332.0MiB| timeout | 0 | | | |scrambled28630.smt2 | 1200.069s | 302.0MiB| timeout | 0 | | | |scrambled21647.smt2 | 1200.070s | 354.0MiB| timeout | 0 | | | |scrambled112083.smt2 | 1200.071s | 312.0MiB| timeout | 0 | | | |scrambled74869.smt2 | 1200.079s | 389.0MiB| timeout | 0 | | | |scrambled112144.smt2 | 1200.081s | 316.0MiB| timeout | 0 | | | |scrambled7923.smt2 | 1200.084s | 285.0MiB| timeout | 0 | | | |scrambled54263.smt2 | 1200.087s | 345.0MiB| timeout | 0 | | | |scrambled118224.smt2 | 1200.093s | 457.0MiB| timeout | 0 | | | |scrambled99534.smt2 | 1200.093s | 385.0MiB| timeout | 0 | | | |scrambled34121.smt2 | 1200.095s | 299.0MiB| timeout | 0 | | | |scrambled117334.smt2 | 1200.098s | 334.0MiB| timeout | 0 | | | |scrambled14880.smt2 | 1200.108s | 291.0MiB| timeout | 0 | | | |scrambled18831.smt2 | 1200.110s | 308.0MiB| timeout | 0 | | | |scrambled7586.smt2 | 1200.122s | 302.0MiB| timeout | 0 | | | |scrambled85895.smt2 | 1200.144s | 972.0MiB| timeout | 0 | | | |scrambled32701.smt2 | 1200.164s | 930.0MiB| timeout | 0 | | | |scrambled94319.smt2 | 1200.211s | 1616.0MiB| timeout | 0 | | | |scrambled94768.smt2 | 1200.244s | 1286.0MiB| timeout | 0 | | | |scrambled60239.smt2 | 1200.411s | 5432.0MiB| timeout | 0 | | | |scrambled121780.smt2 | 1200.440s | 9576.0MiB| timeout | 0 | | | |scrambled27426.smt2 | 1200.477s | 7457.0MiB| timeout | 0 | | | |scrambled14016.smt2 | 1200.499s | 4143.0MiB| timeout | 0 | | | |scrambled6476.smt2 | 1200.570s | 9534.0MiB| timeout | 0 | | | |scrambled91241.smt2 | 1200.580s | 7177.0MiB| timeout | 0 | | | |scrambled61896.smt2 | 1200.598s | 4072.0MiB| timeout | 0 | | | |scrambled58292.smt2 | 1200.605s | 4801.0MiB| timeout | 0 | | | |scrambled78428.smt2 | 1200.695s | 7130.0MiB| timeout | 0 | | | |scrambled65757.smt2 | 1200.721s | 5435.0MiB| timeout | 0 | | | |scrambled70990.smt2 | 1200.777s | 4603.0MiB| timeout | 0 | | | |scrambled41575.smt2 | 1200.855s | 4879.0MiB| timeout | 0 | | | |scrambled124828.smt2 | 1200.983s | 9155.0MiB| timeout | 0 | | | |scrambled22492.smt2 | 1201.692s | 17.874GiB| timeout | 0 | | | |scrambled114923.smt2 | 1202.001s | 18.555GiB| timeout | 0 | | | |scrambled5797.smt2 | 1203.778s | 45.166GiB| timeout | 0 | | |