# . * SAT 5 * UNSAT 11 * TIMEOUT 28 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_NIA-timeout20min-bb2-partial_share
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 6045ce393fc70dffef4ebb7a9ce331b9ce5095c6
Z3 branch: 6045ce393fc70dffef4ebb7a9ce331b9ce5095c6
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_NIA
Z3 commit message: change share units ordering
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled50258.smt2 | 0.912s | 262.0MiB| unsat | 0 | | | |scrambled30073.smt2 | 4.293s | 244.0MiB| unsat | 0 | | | |scrambled9548.smt2 | 4.962s | 312.0MiB| unsat | 0 | | | |scrambled48569.smt2 | 5.730s | 1395.0MiB| sat | 0 | | | |scrambled82407.smt2 | 6.129s | 273.0MiB| unsat | 0 | | | |scrambled129467.smt2 | 10.439s | 438.0MiB| unsat | 0 | | | |scrambled17293.smt2 | 16.384s | 1072.0MiB| sat | 0 | | | |scrambled12959.smt2 | 17.588s | 440.0MiB| unsat | 0 | | | |scrambled29780.smt2 | 20.712s | 286.0MiB| unsat | 0 | | | |scrambled103775.smt2 | 26.619s | 348.0MiB| unsat | 0 | | | |scrambled31071.smt2 | 56.776s | 553.0MiB| sat | 0 | | | |scrambled61060.smt2 | 204.036s | 1680.0MiB| unsat | 0 | | | |scrambled80288.smt2 | 220.871s | 1074.0MiB| unsat | 0 | | | |scrambled28176.smt2 | 259.225s | 1347.0MiB| sat | 0 | | | |scrambled14845.smt2 | 615.201s | 6659.0MiB| unsat | 0 | | | |scrambled96401.smt2 | 694.701s | 2425.0MiB| sat | 0 | | | |scrambled31575.smt2 | 1200.106s | 585.0MiB| timeout | 0 | | | |scrambled58311.smt2 | 1200.126s | 1063.0MiB| timeout | 0 | | | |scrambled38587.smt2 | 1200.143s | 1304.0MiB| timeout | 0 | | | |scrambled35280.smt2 | 1200.146s | 979.0MiB| timeout | 0 | | | |scrambled8852.smt2 | 1200.158s | 1977.0MiB| timeout | 0 | | | |scrambled100714.smt2 | 1200.158s | 1252.0MiB| timeout | 0 | | | |scrambled119582.smt2 | 1200.158s | 1439.0MiB| timeout | 0 | | | |scrambled101716.smt2 | 1200.174s | 1492.0MiB| timeout | 0 | | | |scrambled98111.smt2 | 1200.177s | 1582.0MiB| timeout | 0 | | | |scrambled41135.smt2 | 1200.180s | 1872.0MiB| timeout | 0 | | | |scrambled9883.smt2 | 1200.201s | 1311.0MiB| timeout | 0 | | | |scrambled36790.smt2 | 1200.214s | 1758.0MiB| timeout | 0 | | | |scrambled97386.smt2 | 1200.240s | 1590.0MiB| timeout | 0 | | | |scrambled39467.smt2 | 1200.241s | 2283.0MiB| timeout | 0 | | | |scrambled73281.smt2 | 1200.268s | 2212.0MiB| timeout | 0 | | | |scrambled62032.smt2 | 1200.275s | 2908.0MiB| timeout | 0 | | | |scrambled91750.smt2 | 1200.284s | 2729.0MiB| timeout | 0 | | | |scrambled12033.smt2 | 1200.301s | 2952.0MiB| timeout | 0 | | | |scrambled108406.smt2 | 1200.327s | 2479.0MiB| timeout | 0 | | | |scrambled82760.smt2 | 1200.336s | 3291.0MiB| timeout | 0 | | | |scrambled79354.smt2 | 1200.345s | 1807.0MiB| timeout | 0 | | | |scrambled108663.smt2 | 1200.361s | 3017.0MiB| timeout | 0 | | | |scrambled130111.smt2 | 1200.369s | 2193.0MiB| timeout | 0 | | | |scrambled122926.smt2 | 1200.387s | 3668.0MiB| timeout | 0 | | | |scrambled87588.smt2 | 1200.449s | 3146.0MiB| timeout | 0 | | | |scrambled47700.smt2 | 1200.549s | 5463.0MiB| timeout | 0 | | | |scrambled73755.smt2 | 1200.592s | 5096.0MiB| timeout | 0 | | | |scrambled85357.smt2 | 1202.818s | 33.043GiB| timeout | 0 | | |