# . * SAT 89 * UNSAT 86 * TIMEOUT 13 * UNKNOWN 0 * UNSET 1 * ERROR 1 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: certora2-parallel
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: ed84b14e6c7dfaf6efd1b740119ecb1631e8bdfb
Z3 branch: arie
Z3 options: "-T:30 smt.arith.nl.nra.poly=true smt.threads=4"
Z3 inputs: inputs/certora2
Z3 commit message: fixing coi bug

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |auk-0038.smt2 | 0.017s | 19.1MiB| unsat | 0 | | | |auk-0054.smt2 | 0.018s | 18.972MiB| unsat | 0 | | | |auk-0035.smt2 | 0.030s | 20.18MiB| unsat | 0 | | | |auk-0068.smt2 | 0.063s | 90.068MiB| unsat | 0 | | | |auk-0066.smt2 | 0.066s | 90.096MiB| sat | 0 | | | |auk-0160.smt2 | 0.069s | 91.536MiB| unsat | 0 | | | |auk-0065.smt2 | 0.071s | 20.848MiB| unsat | 0 | | | |auk-0057.smt2 | 0.072s | 90.904MiB| unsat | 0 | | | |auk-0046.smt2 | 0.072s | 91.42MiB| unsat | 0 | | | |auk-0159.smt2 | 0.073s | 92.484MiB| unsat | 0 | | | |auk-0032.smt2 | 0.075s | 21.072MiB| unsat | 0 | | | |auk-0034.smt2 | 0.075s | 20.972MiB| unsat | 0 | | | |auk-0170.smt2 | 0.079s | 92.956MiB| unsat | 0 | | | |auk-0039.smt2 | 0.083s | 21.004MiB| unsat | 0 | | | |auk-0040.smt2 | 0.084s | 91.936MiB| unsat | 0 | | | |auk-0178.smt2 | 0.085s | 90.396MiB| sat | 0 | | | |auk-0161.smt2 | 0.086s | 89.624MiB| sat | 0 | | | |auk-0050.smt2 | 0.087s | 91.944MiB| unsat | 0 | | | |auk-0060.smt2 | 0.087s | 91.68MiB| unsat | 0 | | | |auk-0179.smt2 | 0.087s | 91.672MiB| unsat | 0 | | | |auk-0069.smt2 | 0.087s | 92.412MiB| unsat | 0 | | | |auk-0166.smt2 | 0.088s | 94.484MiB| sat | 0 | | | |auk-0168.smt2 | 0.090s | 90.908MiB| sat | 0 | | | |auk-0067.smt2 | 0.093s | 92.544MiB| sat | 0 | | | |auk-0042.smt2 | 0.094s | 91.928MiB| sat | 0 | | | |auk-0138.smt2 | 0.094s | 92.764MiB| unsat | 0 | | | |auk-0041.smt2 | 0.095s | 92.188MiB| unsat | 0 | | | |auk-0009.smt2 | 0.097s | 93.988MiB| sat | 0 | | | |auk-0031.smt2 | 0.099s | 92.432MiB| unsat | 0 | | | |auk-0012.smt2 | 0.110s | 94.748MiB| unsat | 0 | | | |auk-0061.smt2 | 0.110s | 94.508MiB| unsat | 0 | | | |auk-0051.smt2 | 0.117s | 94.876MiB| unsat | 0 | | | |auk-0064.smt2 | 0.118s | 94.744MiB| sat | 0 | | | |auk-0036.smt2 | 0.121s | 96.136MiB| sat | 0 | | | |auk-0143.smt2 | 0.124s | 95.0MiB| unsat | 0 | | | |auk-0059.smt2 | 0.125s | 100.0MiB| unsat | 0 | | | |auk-0097.smt2 | 0.134s | 97.0MiB| sat | 0 | | | |auk-0028.smt2 | 0.137s | 98.676MiB| unsat | 0 | | | |auk-0139.smt2 | 0.144s | 99.308MiB| unsat | 0 | | | |auk-0055.smt2 | 0.147s | 106.0MiB| sat | 0 | | | |auk-0136.smt2 | 0.149s | 94.232MiB| sat | 0 | | | |auk-0093.smt2 | 0.152s | 103.0MiB| sat | 0 | | | |auk-0043.smt2 | 0.153s | 103.0MiB| unsat | 0 | | | |auk-0162.smt2 | 0.154s | 105.0MiB| sat | 0 | | | |auk-0053.smt2 | 0.156s | 96.176MiB| sat | 0 | | | |auk-0037.smt2 | 0.159s | 108.0MiB| unsat | 0 | | | |auk-0152.smt2 | 0.160s | 106.0MiB| sat | 0 | | | |auk-0044.smt2 | 0.162s | 101.0MiB| unsat | 0 | | | |auk-0058.smt2 | 0.167s | 106.0MiB| sat | 0 | | | |auk-0063.smt2 | 0.171s | 101.0MiB| unsat | 0 | | | |auk-0110.smt2 | 0.172s | 106.0MiB| sat | 0 | | | |auk-0047.smt2 | 0.173s | 106.0MiB| unsat | 0 | | | |auk-0029.smt2 | 0.174s | 109.0MiB| unsat | 0 | | | |auk-0052.smt2 | 0.175s | 105.0MiB| unsat | 0 | | | |auk-0030.smt2 | 0.176s | 107.0MiB| unsat | 0 | | | |auk-0129.smt2 | 0.177s | 106.0MiB| sat | 0 | | | |auk-0167.smt2 | 0.179s | 110.0MiB| sat | 0 | | | |auk-0104.smt2 | 0.179s | 103.0MiB| sat | 0 | | | |auk-0155.smt2 | 0.180s | 110.0MiB| sat | 0 | | | |auk-0164.smt2 | 0.180s | 110.0MiB| sat | 0 | | | |auk-0062.smt2 | 0.181s | 104.0MiB| unsat | 0 | | | |auk-0127.smt2 | 0.181s | 114.0MiB| sat | 0 | | | |auk-0114.smt2 | 0.181s | 110.0MiB| sat | 0 | | | |auk-0045.smt2 | 0.182s | 105.0MiB| unsat | 0 | | | |auk-0020.smt2 | 0.183s | 109.0MiB| unsat | 0 | | | |auk-0157.smt2 | 0.184s | 107.0MiB| sat | 0 | | | |auk-0022.smt2 | 0.186s | 111.0MiB| sat | 0 | | | |auk-0018.smt2 | 0.186s | 110.0MiB| unsat | 0 | | | |auk-0033.smt2 | 0.189s | 109.0MiB| sat | 0 | | | |auk-0100.smt2 | 0.192s | 105.0MiB| sat | 0 | | | |auk-0021.smt2 | 0.193s | 100.0MiB| unsat | 0 | | | |auk-0165.smt2 | 0.193s | 109.0MiB| sat | 0 | | | |auk-0106.smt2 | 0.193s | 115.0MiB| sat | 0 | | | |auk-0049.smt2 | 0.197s | 99.624MiB| unsat | 0 | | | |auk-0124.smt2 | 0.197s | 116.0MiB| sat | 0 | | | |auk-0048.smt2 | 0.198s | 107.0MiB| unsat | 0 | | | |auk-0026.smt2 | 0.198s | 106.0MiB| unsat | 0 | | | |auk-0171.smt2 | 0.199s | 110.0MiB| sat | 0 | | | |auk-0158.smt2 | 0.203s | 106.0MiB| sat | 0 | | | |auk-0103.smt2 | 0.206s | 119.0MiB| sat | 0 | | | |auk-0121.smt2 | 0.209s | 113.0MiB| sat | 0 | | | |auk-0107.smt2 | 0.211s | 115.0MiB| sat | 0 | | | |auk-0016.smt2 | 0.216s | 106.0MiB| unsat | 0 | | | |auk-0176.smt2 | 0.216s | 113.0MiB| sat | 0 | | | |auk-0013.smt2 | 0.219s | 116.0MiB| unsat | 0 | | | |auk-0024.smt2 | 0.220s | 109.0MiB| unsat | 0 | | | |auk-0180.smt2 | 0.220s | 116.0MiB| unsat | 0 | | | |auk-0154.smt2 | 0.221s | 112.0MiB| sat | 0 | | | |auk-0174.smt2 | 0.221s | 110.0MiB| sat | 0 | | | |auk-0163.smt2 | 0.221s | 110.0MiB| sat | 0 | | | |auk-0172.smt2 | 0.222s | 110.0MiB| sat | 0 | | | |auk-0153.smt2 | 0.222s | 113.0MiB| sat | 0 | | | |auk-0173.smt2 | 0.223s | 110.0MiB| sat | 0 | | | |auk-0019.smt2 | 0.224s | 110.0MiB| unsat | 0 | | | |auk-0175.smt2 | 0.228s | 113.0MiB| sat | 0 | | | |auk-0177.smt2 | 0.230s | 113.0MiB| sat | 0 | | | |auk-0126.smt2 | 0.231s | 120.0MiB| sat | 0 | | | |auk-0156.smt2 | 0.233s | 110.0MiB| sat | 0 | | | |auk-0169.smt2 | 0.240s | 112.0MiB| unsat | 0 | | | |auk-0102.smt2 | 0.241s | 116.0MiB| sat | 0 | | | |auk-0001.smt2 | 0.244s | 96.996MiB| sat | 0 | | | |auk-0105.smt2 | 0.245s | 116.0MiB| sat | 0 | | | |auk-0125.smt2 | 0.246s | 115.0MiB| sat | 0 | | | |auk-0003.smt2 | 0.248s | 116.0MiB| unsat | 0 | | | |auk-0008.smt2 | 0.249s | 116.0MiB| unsat | 0 | | | |auk-0112.smt2 | 0.253s | 117.0MiB| sat | 0 | | | |auk-0118.smt2 | 0.254s | 116.0MiB| sat | 0 | | | |auk-0014.smt2 | 0.259s | 116.0MiB| unsat | 0 | | | |auk-0017.smt2 | 0.264s | 118.0MiB| unsat | 0 | | | |auk-0111.smt2 | 0.275s | 120.0MiB| sat | 0 | | | |auk-0150.smt2 | 0.276s | 110.0MiB| unsat | 0 | | | |auk-0108.smt2 | 0.299s | 124.0MiB| sat | 0 | | | |auk-0117.smt2 | 0.301s | 128.0MiB| sat | 0 | | | |auk-0002.smt2 | 0.311s | 130.0MiB| unsat | 0 | | | |auk-0122.smt2 | 0.313s | 126.0MiB| sat | 0 | | | |auk-0113.smt2 | 0.314s | 124.0MiB| sat | 0 | | | |auk-0151.smt2 | 0.338s | 99.796MiB| unsat | 0 | | | |auk-0120.smt2 | 0.341s | 129.0MiB| sat | 0 | | | |auk-0023.smt2 | 0.342s | 117.0MiB| unsat | 0 | | | |auk-0134.smt2 | 0.343s | 131.0MiB| sat | 0 | | | |auk-0116.smt2 | 0.349s | 128.0MiB| sat | 0 | | | |auk-0010.smt2 | 0.351s | 137.0MiB| unsat | 0 | | | |auk-0135.smt2 | 0.353s | 116.0MiB| unsat | 0 | | | |auk-0123.smt2 | 0.356s | 127.0MiB| sat | 0 | | | |auk-0070.smt2 | 0.365s | 132.0MiB| sat | 0 | | | |auk-0128.smt2 | 0.366s | 135.0MiB| sat | 0 | | | |auk-0130.smt2 | 0.381s | 133.0MiB| sat | 0 | | | |auk-0119.smt2 | 0.424s | 136.0MiB| sat | 0 | | | |auk-0006.smt2 | 0.503s | 142.0MiB| unsat | 0 | | | |auk-0115.smt2 | 0.520s | 143.0MiB| sat | 0 | | | |auk-0096.smt2 | 0.552s | 119.0MiB| sat | 0 | | | |auk-0025.smt2 | 0.553s | 128.0MiB| unsat | 0 | | | |auk-0080.smt2 | 0.557s | 138.0MiB| sat | 0 | | | |auk-0072.smt2 | 0.583s | 139.0MiB| sat | 0 | | | |auk-0078.smt2 | 0.661s | 139.0MiB| sat | 0 | | | |auk-0109.smt2 | 0.704s | 128.0MiB| sat | 0 | | | |auk-0094.smt2 | 0.750s | 134.0MiB| sat | 0 | | | |auk-0091.smt2 | 0.795s | 165.0MiB| sat | 0 | | | |auk-0056.smt2 | 0.863s | 116.0MiB| sat | 0 | | | |auk-0145.smt2 | 0.871s | 125.0MiB| unsat | 0 | | | |auk-0004.smt2 | 0.931s | 148.0MiB| unsat | 0 | | | |auk-0133.smt2 | 1.026s | 177.0MiB| sat | 0 | | | |auk-0101.smt2 | 1.094s | 137.0MiB| unsat | 0 | | | |auk-0077.smt2 | 1.195s | 163.0MiB| sat | 0 | | | |auk-0184.smt2 | 1.227s | 147.0MiB| unsat | 0 | | | |auk-0132.smt2 | 1.265s | 201.0MiB| sat | 0 | | | |auk-0073.smt2 | 1.320s | 186.0MiB| sat | 0 | | | |auk-0071.smt2 | 1.332s | 186.0MiB| sat | 0 | | | |auk-0076.smt2 | 1.348s | 187.0MiB| sat | 0 | | | |auk-0075.smt2 | 1.350s | 187.0MiB| sat | 0 | | | |auk-0146.smt2 | 1.374s | 124.0MiB| unsat | 0 | | | |auk-0144.smt2 | 1.395s | 139.0MiB| unsat | 0 | | | |auk-0149.smt2 | 1.861s | 125.0MiB| unsat | 0 | | | |auk-0095.smt2 | 2.251s | 153.0MiB| unsat | 0 | | | |auk-0131.smt2 | 2.536s | 315.0MiB| sat | 0 | | | |auk-0148.smt2 | 2.608s | 145.0MiB| unsat | 0 | | | |auk-0082.smt2 | 3.137s | 318.0MiB| sat | 0 | | | |auk-0083.smt2 | 3.192s | 318.0MiB| sat | 0 | | | |auk-0181.smt2 | 3.498s | 241.0MiB| unsat | 0 | | | |auk-0027.smt2 | 4.049s | 193.0MiB| unsat | 0 | | | |auk-0084.smt2 | 4.218s | 214.0MiB| unsat | 0 | | | |auk-0142.smt2 | 4.262s | 150.0MiB| unsat | 0 | | | |auk-0079.smt2 | 4.659s | 195.0MiB| sat | 0 | | | |auk-0186.smt2 | 4.748s | 251.0MiB| unsat | 0 | | | |auk-0182.smt2 | 4.786s | 248.0MiB| unsat | 0 | | | |auk-0089.smt2 | 5.500s | 240.0MiB| unsat | 0 | | | |auk-0183.smt2 | 5.942s | 257.0MiB| unsat | 0 | | | |auk-0087.smt2 | 9.118s | 247.0MiB| unsat | 0 | | | |auk-0090.smt2 | 11.420s | 231.0MiB| unsat | 0 | | | |auk-0140.smt2 | 12.758s | 162.0MiB| unsat | 0 | | | |auk-0137.smt2 | 15.124s | 146.0MiB| sat | 0 | | | |auk-0185.smt2 | 17.988s | 193.0MiB| unsat | 0 | | | |auk-0189.smt2 | 19.091s | 214.0MiB| unsat | 0 | | | |auk-0015.smt2 | 22.537s | 179.0MiB| unset | 139 | | | |auk-0141.smt2 | 24.617s | 213.0MiB| unsat | 0 | | | |auk-0081.smt2 | 28.294s | 145.0MiB| unsat | 0 | | | |auk-0074.smt2 | 30.031s | 135.0MiB| timeout | 0 | | | |auk-0187.smt2 | 30.034s | 220.0MiB| timeout | 0 | | | |auk-0005.smt2 | 30.036s | 182.0MiB| timeout | 0 | | | |auk-0011.smt2 | 30.042s | 210.0MiB| timeout | 0 | | | |auk-0147.smt2 | 30.045s | 153.0MiB| timeout | 0 | | | |auk-0188.smt2 | 30.046s | 201.0MiB| timeout | 0 | | | |auk-0092.smt2 | 30.050s | 345.0MiB| timeout | 0 | | | |auk-0086.smt2 | 30.054s | 361.0MiB| timeout | 0 | | | |auk-0085.smt2 | 30.057s | 348.0MiB| timeout | 0 | | | |auk-0088.smt2 | 30.062s | 337.0MiB| timeout | 0 | | | |auk-0098.smt2 | 30.118s | 845.0MiB| timeout | 0 | | | |auk-0007.smt2 | 30.123s | 862.0MiB| timeout | 0 | | | |auk-0099.smt2 | 30.127s | 932.0MiB| timeout | 0 | | |