# . * SAT 5 * UNSAT 11 * TIMEOUT 28 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-4-smtcomp2025-QF_NIA-timeout_20min_bb2
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 6b8cb1099d311aac105cfc6fa658466f4ef6af67
Z3 branch: backbones
Z3 options: "-T:1260 -v:0 smt.threads=4 tactic.default_tactic=smt smt.auto_config=false smt_parallel.num_global_bb_threads=2"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_NIA
Z3 commit message: restore unrelated code to master
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled50258.smt2 | 0.864s | 158.0MiB| unsat | 0 | | | |scrambled30073.smt2 | 5.000s | 206.0MiB| unsat | 0 | | | |scrambled9548.smt2 | 7.006s | 193.0MiB| unsat | 0 | | | |scrambled82407.smt2 | 8.273s | 160.0MiB| unsat | 0 | | | |scrambled48569.smt2 | 9.115s | 812.0MiB| sat | 0 | | | |scrambled129467.smt2 | 12.053s | 256.0MiB| unsat | 0 | | | |scrambled12959.smt2 | 19.679s | 253.0MiB| unsat | 0 | | | |scrambled17293.smt2 | 22.023s | 647.0MiB| sat | 0 | | | |scrambled29780.smt2 | 39.354s | 225.0MiB| unsat | 0 | | | |scrambled103775.smt2 | 141.347s | 270.0MiB| unsat | 0 | | | |scrambled61060.smt2 | 168.198s | 942.0MiB| unsat | 0 | | | |scrambled80288.smt2 | 233.020s | 580.0MiB| unsat | 0 | | | |scrambled96401.smt2 | 239.827s | 613.0MiB| sat | 0 | | | |scrambled28176.smt2 | 346.287s | 899.0MiB| sat | 0 | | | |scrambled31071.smt2 | 444.917s | 690.0MiB| sat | 0 | | | |scrambled14845.smt2 | 719.274s | 4362.0MiB| unsat | 0 | | | |scrambled31575.smt2 | 1260.040s | 127.0MiB| timeout | 0 | | | |scrambled35280.smt2 | 1260.090s | 592.0MiB| timeout | 0 | | | |scrambled101716.smt2 | 1260.095s | 856.0MiB| timeout | 0 | | | |scrambled8852.smt2 | 1260.108s | 872.0MiB| timeout | 0 | | | |scrambled73281.smt2 | 1260.119s | 982.0MiB| timeout | 0 | | | |scrambled9883.smt2 | 1260.120s | 832.0MiB| timeout | 0 | | | |scrambled119582.smt2 | 1260.121s | 812.0MiB| timeout | 0 | | | |scrambled100714.smt2 | 1260.122s | 787.0MiB| timeout | 0 | | | |scrambled98111.smt2 | 1260.122s | 1044.0MiB| timeout | 0 | | | |scrambled38587.smt2 | 1260.134s | 954.0MiB| timeout | 0 | | | |scrambled87588.smt2 | 1260.139s | 1033.0MiB| timeout | 0 | | | |scrambled41135.smt2 | 1260.159s | 1013.0MiB| timeout | 0 | | | |scrambled79354.smt2 | 1260.166s | 881.0MiB| timeout | 0 | | | |scrambled36790.smt2 | 1260.175s | 1769.0MiB| timeout | 0 | | | |scrambled62032.smt2 | 1260.180s | 1324.0MiB| timeout | 0 | | | |scrambled58311.smt2 | 1260.196s | 1420.0MiB| timeout | 0 | | | |scrambled97386.smt2 | 1260.198s | 1155.0MiB| timeout | 0 | | | |scrambled12033.smt2 | 1260.208s | 1683.0MiB| timeout | 0 | | | |scrambled47700.smt2 | 1260.237s | 1791.0MiB| timeout | 0 | | | |scrambled122926.smt2 | 1260.239s | 2326.0MiB| timeout | 0 | | | |scrambled91750.smt2 | 1260.252s | 1614.0MiB| timeout | 0 | | | |scrambled73755.smt2 | 1260.306s | 2159.0MiB| timeout | 0 | | | |scrambled39467.smt2 | 1260.315s | 2286.0MiB| timeout | 0 | | | |scrambled130111.smt2 | 1260.347s | 1737.0MiB| timeout | 0 | | | |scrambled108663.smt2 | 1260.439s | 3128.0MiB| timeout | 0 | | | |scrambled82760.smt2 | 1260.546s | 4638.0MiB| timeout | 0 | | | |scrambled108406.smt2 | 1260.918s | 4998.0MiB| timeout | 0 | | | |scrambled85357.smt2 | 1261.777s | 18.459GiB| timeout | 0 | | |