# . * 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
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_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.659s | 24.932MiB| sat | 0 | | | |scrambled14368.smt2 | 51.295s | 265.0MiB| sat | 0 | | | |scrambled73220.smt2 | 1200.043s | 326.0MiB| timeout | 0 | | | |scrambled21647.smt2 | 1200.043s | 350.0MiB| timeout | 0 | | | |scrambled34121.smt2 | 1200.044s | 312.0MiB| timeout | 0 | | | |scrambled82241.smt2 | 1200.046s | 307.0MiB| timeout | 0 | | | |scrambled80728.smt2 | 1200.047s | 383.0MiB| timeout | 0 | | | |scrambled42946.smt2 | 1200.051s | 323.0MiB| timeout | 0 | | | |scrambled32269.smt2 | 1200.055s | 295.0MiB| timeout | 0 | | | |scrambled100912.smt2 | 1200.058s | 332.0MiB| timeout | 0 | | | |scrambled74869.smt2 | 1200.059s | 326.0MiB| timeout | 0 | | | |scrambled14880.smt2 | 1200.061s | 393.0MiB| timeout | 0 | | | |scrambled112144.smt2 | 1200.064s | 350.0MiB| timeout | 0 | | | |scrambled28630.smt2 | 1200.064s | 305.0MiB| timeout | 0 | | | |scrambled7923.smt2 | 1200.065s | 284.0MiB| timeout | 0 | | | |scrambled118224.smt2 | 1200.068s | 1050.0MiB| timeout | 0 | | | |scrambled117944.smt2 | 1200.070s | 307.0MiB| timeout | 0 | | | |scrambled112083.smt2 | 1200.070s | 291.0MiB| timeout | 0 | | | |scrambled7586.smt2 | 1200.070s | 344.0MiB| timeout | 0 | | | |scrambled18831.smt2 | 1200.083s | 417.0MiB| timeout | 0 | | | |scrambled54263.smt2 | 1200.084s | 353.0MiB| timeout | 0 | | | |scrambled99534.smt2 | 1200.090s | 394.0MiB| timeout | 0 | | | |scrambled117334.smt2 | 1200.135s | 1097.0MiB| timeout | 0 | | | |scrambled32701.smt2 | 1200.138s | 916.0MiB| timeout | 0 | | | |scrambled94768.smt2 | 1200.148s | 1132.0MiB| timeout | 0 | | | |scrambled85895.smt2 | 1200.179s | 1341.0MiB| timeout | 0 | | | |scrambled94319.smt2 | 1200.211s | 1806.0MiB| timeout | 0 | | | |scrambled36539.smt2 | 1200.229s | 2161.0MiB| timeout | 0 | | | |scrambled27426.smt2 | 1200.384s | 7717.0MiB| timeout | 0 | | | |scrambled60239.smt2 | 1200.401s | 5686.0MiB| timeout | 0 | | | |scrambled14016.smt2 | 1200.463s | 3833.0MiB| timeout | 0 | | | |scrambled41575.smt2 | 1200.487s | 5293.0MiB| timeout | 0 | | | |scrambled121780.smt2 | 1200.492s | 9643.0MiB| timeout | 0 | | | |scrambled91241.smt2 | 1200.520s | 7185.0MiB| timeout | 0 | | | |scrambled70990.smt2 | 1200.545s | 4774.0MiB| timeout | 0 | | | |scrambled78428.smt2 | 1200.630s | 7342.0MiB| timeout | 0 | | | |scrambled6476.smt2 | 1200.642s | 9574.0MiB| timeout | 0 | | | |scrambled58292.smt2 | 1200.670s | 6856.0MiB| timeout | 0 | | | |scrambled61896.smt2 | 1200.690s | 4737.0MiB| timeout | 0 | | | |scrambled124828.smt2 | 1201.245s | 14.182GiB| timeout | 0 | | | |scrambled65757.smt2 | 1201.286s | 12.829GiB| timeout | 0 | | | |scrambled114923.smt2 | 1201.414s | 16.322GiB| timeout | 0 | | | |scrambled22492.smt2 | 1201.685s | 18.575GiB| timeout | 0 | | | |scrambled5797.smt2 | 1202.044s | 24.915GiB| timeout | 0 | | |