# . * SAT 4 * UNSAT 10 * TIMEOUT 30 * UNKNOWN 0 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-4-smtcomp2025-QF_NIA-timeout20min
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 2cea893814fb3b4fe45426654eccafd40abe1b9e
Z3 branch: smt_parallel_comp_2026
Z3 options: "-T:1200 -v:0 smt.threads=4"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_NIA
Z3 commit message: rename
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled50258.smt2 | 0.863s | 176.0MiB| unsat | 0 | | | |scrambled9548.smt2 | 5.076s | 181.0MiB| unsat | 0 | | | |scrambled30073.smt2 | 5.283s | 159.0MiB| unsat | 0 | | | |scrambled82407.smt2 | 6.740s | 176.0MiB| unsat | 0 | | | |scrambled48569.smt2 | 8.438s | 917.0MiB| sat | 0 | | | |scrambled129467.smt2 | 9.316s | 289.0MiB| unsat | 0 | | | |scrambled29780.smt2 | 33.142s | 200.0MiB| unsat | 0 | | | |scrambled17293.smt2 | 39.058s | 755.0MiB| sat | 0 | | | |scrambled12959.smt2 | 41.015s | 432.0MiB| unsat | 0 | | | |scrambled28176.smt2 | 57.432s | 563.0MiB| sat | 0 | | | |scrambled103775.smt2 | 71.823s | 374.0MiB| unsat | 0 | | | |scrambled96401.smt2 | 210.940s | 535.0MiB| sat | 0 | | | |scrambled61060.smt2 | 251.421s | 1152.0MiB| unsat | 0 | | | |scrambled14845.smt2 | 653.818s | 4775.0MiB| unsat | 0 | | | |scrambled31575.smt2 | 1200.026s | 144.0MiB| timeout | 0 | | | |scrambled58311.smt2 | 1200.079s | 535.0MiB| timeout | 0 | | | |scrambled101716.smt2 | 1200.085s | 763.0MiB| timeout | 0 | | | |scrambled38587.smt2 | 1200.088s | 660.0MiB| timeout | 0 | | | |scrambled119582.smt2 | 1200.092s | 794.0MiB| timeout | 0 | | | |scrambled35280.smt2 | 1200.103s | 654.0MiB| timeout | 0 | | | |scrambled87588.smt2 | 1200.109s | 875.0MiB| timeout | 0 | | | |scrambled100714.smt2 | 1200.109s | 815.0MiB| timeout | 0 | | | |scrambled97386.smt2 | 1200.109s | 951.0MiB| timeout | 0 | | | |scrambled41135.smt2 | 1200.113s | 1055.0MiB| timeout | 0 | | | |scrambled8852.smt2 | 1200.119s | 910.0MiB| timeout | 0 | | | |scrambled80288.smt2 | 1200.124s | 742.0MiB| timeout | 0 | | | |scrambled73281.smt2 | 1200.124s | 1046.0MiB| timeout | 0 | | | |scrambled79354.smt2 | 1200.129s | 808.0MiB| timeout | 0 | | | |scrambled9883.smt2 | 1200.135s | 932.0MiB| timeout | 0 | | | |scrambled31071.smt2 | 1200.153s | 1036.0MiB| timeout | 0 | | | |scrambled62032.smt2 | 1200.159s | 967.0MiB| timeout | 0 | | | |scrambled82760.smt2 | 1200.167s | 922.0MiB| timeout | 0 | | | |scrambled36790.smt2 | 1200.172s | 1024.0MiB| timeout | 0 | | | |scrambled98111.smt2 | 1200.181s | 956.0MiB| timeout | 0 | | | |scrambled47700.smt2 | 1200.202s | 1912.0MiB| timeout | 0 | | | |scrambled39467.smt2 | 1200.215s | 2306.0MiB| timeout | 0 | | | |scrambled130111.smt2 | 1200.220s | 1203.0MiB| timeout | 0 | | | |scrambled108406.smt2 | 1200.241s | 1627.0MiB| timeout | 0 | | | |scrambled12033.smt2 | 1200.253s | 1814.0MiB| timeout | 0 | | | |scrambled122926.smt2 | 1200.254s | 2078.0MiB| timeout | 0 | | | |scrambled91750.smt2 | 1200.304s | 1836.0MiB| timeout | 0 | | | |scrambled108663.smt2 | 1200.320s | 2326.0MiB| timeout | 0 | | | |scrambled73755.smt2 | 1200.403s | 3179.0MiB| timeout | 0 | | | |scrambled85357.smt2 | 1201.488s | 15.837GiB| timeout | 0 | | |