# . * SAT 89 * UNSAT 77 * TIMEOUT 22 * 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 tactic.default_tactic=smt 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-0068.smt2 | 0.065s | 90.1MiB| unsat | 0 | | | |auk-0038.smt2 | 0.068s | 91.164MiB| unsat | 0 | | | |auk-0031.smt2 | 0.075s | 92.7MiB| unsat | 0 | | | |auk-0160.smt2 | 0.079s | 93.172MiB| unsat | 0 | | | |auk-0040.smt2 | 0.080s | 94.62MiB| unsat | 0 | | | |auk-0054.smt2 | 0.082s | 89.632MiB| unsat | 0 | | | |auk-0161.smt2 | 0.085s | 89.864MiB| sat | 0 | | | |auk-0138.smt2 | 0.090s | 92.952MiB| unsat | 0 | | | |auk-0066.smt2 | 0.091s | 91.416MiB| sat | 0 | | | |auk-0069.smt2 | 0.091s | 92.708MiB| unsat | 0 | | | |auk-0067.smt2 | 0.091s | 92.992MiB| sat | 0 | | | |auk-0057.smt2 | 0.092s | 92.116MiB| unsat | 0 | | | |auk-0042.smt2 | 0.092s | 92.196MiB| sat | 0 | | | |auk-0178.smt2 | 0.092s | 92.44MiB| sat | 0 | | | |auk-0060.smt2 | 0.094s | 92.076MiB| unsat | 0 | | | |auk-0050.smt2 | 0.096s | 93.216MiB| unsat | 0 | | | |auk-0046.smt2 | 0.096s | 92.124MiB| unsat | 0 | | | |auk-0168.smt2 | 0.097s | 93.472MiB| sat | 0 | | | |auk-0179.smt2 | 0.097s | 92.444MiB| unsat | 0 | | | |auk-0041.smt2 | 0.100s | 93.728MiB| unsat | 0 | | | |auk-0159.smt2 | 0.101s | 94.664MiB| unsat | 0 | | | |auk-0061.smt2 | 0.102s | 94.772MiB| unsat | 0 | | | |auk-0170.smt2 | 0.107s | 94.24MiB| unsat | 0 | | | |auk-0064.smt2 | 0.108s | 94.744MiB| sat | 0 | | | |auk-0036.smt2 | 0.113s | 96.28MiB| sat | 0 | | | |auk-0166.smt2 | 0.113s | 96.728MiB| sat | 0 | | | |auk-0049.smt2 | 0.113s | 96.828MiB| unsat | 0 | | | |auk-0035.smt2 | 0.113s | 101.0MiB| unsat | 0 | | | |auk-0012.smt2 | 0.117s | 96.96MiB| unsat | 0 | | | |auk-0053.smt2 | 0.122s | 96.628MiB| sat | 0 | | | |auk-0009.smt2 | 0.127s | 96.28MiB| sat | 0 | | | |auk-0028.smt2 | 0.145s | 104.0MiB| unsat | 0 | | | |auk-0143.smt2 | 0.155s | 96.536MiB| unsat | 0 | | | |auk-0097.smt2 | 0.156s | 111.0MiB| sat | 0 | | | |auk-0032.smt2 | 0.157s | 112.0MiB| unsat | 0 | | | |auk-0059.smt2 | 0.162s | 108.0MiB| unsat | 0 | | | |auk-0162.smt2 | 0.162s | 118.0MiB| sat | 0 | | | |auk-0055.smt2 | 0.163s | 118.0MiB| sat | 0 | | | |auk-0051.smt2 | 0.164s | 97.684MiB| unsat | 0 | | | |auk-0065.smt2 | 0.164s | 105.0MiB| unsat | 0 | | | |auk-0058.smt2 | 0.167s | 117.0MiB| sat | 0 | | | |auk-0034.smt2 | 0.168s | 108.0MiB| unsat | 0 | | | |auk-0024.smt2 | 0.172s | 115.0MiB| unsat | 0 | | | |auk-0063.smt2 | 0.173s | 112.0MiB| unsat | 0 | | | |auk-0030.smt2 | 0.183s | 117.0MiB| unsat | 0 | | | |auk-0037.smt2 | 0.184s | 119.0MiB| unsat | 0 | | | |auk-0020.smt2 | 0.185s | 118.0MiB| unsat | 0 | | | |auk-0045.smt2 | 0.186s | 116.0MiB| unsat | 0 | | | |auk-0039.smt2 | 0.190s | 115.0MiB| unsat | 0 | | | |auk-0021.smt2 | 0.190s | 116.0MiB| unsat | 0 | | | |auk-0016.smt2 | 0.192s | 114.0MiB| unsat | 0 | | | |auk-0043.smt2 | 0.192s | 115.0MiB| unsat | 0 | | | |auk-0033.smt2 | 0.192s | 120.0MiB| sat | 0 | | | |auk-0018.smt2 | 0.192s | 122.0MiB| unsat | 0 | | | |auk-0104.smt2 | 0.193s | 118.0MiB| sat | 0 | | | |auk-0047.smt2 | 0.195s | 116.0MiB| unsat | 0 | | | |auk-0029.smt2 | 0.196s | 120.0MiB| unsat | 0 | | | |auk-0052.smt2 | 0.197s | 116.0MiB| unsat | 0 | | | |auk-0044.smt2 | 0.197s | 112.0MiB| unsat | 0 | | | |auk-0019.smt2 | 0.198s | 120.0MiB| unsat | 0 | | | |auk-0022.smt2 | 0.203s | 121.0MiB| sat | 0 | | | |auk-0152.smt2 | 0.203s | 120.0MiB| sat | 0 | | | |auk-0100.smt2 | 0.204s | 119.0MiB| sat | 0 | | | |auk-0164.smt2 | 0.205s | 127.0MiB| sat | 0 | | | |auk-0180.smt2 | 0.208s | 126.0MiB| unsat | 0 | | | |auk-0158.smt2 | 0.209s | 120.0MiB| sat | 0 | | | |auk-0048.smt2 | 0.209s | 118.0MiB| unsat | 0 | | | |auk-0110.smt2 | 0.210s | 120.0MiB| sat | 0 | | | |auk-0114.smt2 | 0.212s | 129.0MiB| sat | 0 | | | |auk-0129.smt2 | 0.216s | 124.0MiB| sat | 0 | | | |auk-0093.smt2 | 0.227s | 119.0MiB| sat | 0 | | | |auk-0124.smt2 | 0.227s | 134.0MiB| sat | 0 | | | |auk-0155.smt2 | 0.229s | 133.0MiB| sat | 0 | | | |auk-0026.smt2 | 0.231s | 121.0MiB| unsat | 0 | | | |auk-0169.smt2 | 0.232s | 129.0MiB| unsat | 0 | | | |auk-0106.smt2 | 0.232s | 133.0MiB| sat | 0 | | | |auk-0023.smt2 | 0.235s | 125.0MiB| unsat | 0 | | | |auk-0173.smt2 | 0.237s | 129.0MiB| sat | 0 | | | |auk-0172.smt2 | 0.238s | 128.0MiB| sat | 0 | | | |auk-0176.smt2 | 0.238s | 133.0MiB| sat | 0 | | | |auk-0163.smt2 | 0.239s | 128.0MiB| sat | 0 | | | |auk-0167.smt2 | 0.240s | 134.0MiB| sat | 0 | | | |auk-0174.smt2 | 0.242s | 129.0MiB| sat | 0 | | | |auk-0136.smt2 | 0.242s | 95.516MiB| sat | 0 | | | |auk-0157.smt2 | 0.245s | 131.0MiB| sat | 0 | | | |auk-0062.smt2 | 0.246s | 129.0MiB| unsat | 0 | | | |auk-0103.smt2 | 0.248s | 137.0MiB| sat | 0 | | | |auk-0017.smt2 | 0.249s | 129.0MiB| unsat | 0 | | | |auk-0127.smt2 | 0.251s | 131.0MiB| sat | 0 | | | |auk-0154.smt2 | 0.252s | 131.0MiB| sat | 0 | | | |auk-0107.smt2 | 0.257s | 134.0MiB| sat | 0 | | | |auk-0171.smt2 | 0.258s | 135.0MiB| sat | 0 | | | |auk-0165.smt2 | 0.260s | 131.0MiB| sat | 0 | | | |auk-0121.smt2 | 0.262s | 134.0MiB| sat | 0 | | | |auk-0153.smt2 | 0.263s | 134.0MiB| sat | 0 | | | |auk-0175.smt2 | 0.263s | 132.0MiB| sat | 0 | | | |auk-0126.smt2 | 0.264s | 139.0MiB| sat | 0 | | | |auk-0177.smt2 | 0.268s | 135.0MiB| sat | 0 | | | |auk-0125.smt2 | 0.269s | 134.0MiB| sat | 0 | | | |auk-0156.smt2 | 0.272s | 134.0MiB| sat | 0 | | | |auk-0111.smt2 | 0.277s | 134.0MiB| sat | 0 | | | |auk-0105.smt2 | 0.282s | 135.0MiB| sat | 0 | | | |auk-0102.smt2 | 0.288s | 134.0MiB| sat | 0 | | | |auk-0150.smt2 | 0.289s | 124.0MiB| unsat | 0 | | | |auk-0112.smt2 | 0.291s | 136.0MiB| sat | 0 | | | |auk-0118.smt2 | 0.303s | 138.0MiB| sat | 0 | | | |auk-0117.smt2 | 0.304s | 139.0MiB| sat | 0 | | | |auk-0113.smt2 | 0.310s | 140.0MiB| sat | 0 | | | |auk-0108.smt2 | 0.312s | 147.0MiB| sat | 0 | | | |auk-0130.smt2 | 0.329s | 149.0MiB| sat | 0 | | | |auk-0027.smt2 | 0.339s | 124.0MiB| unsat | 0 | | | |auk-0025.smt2 | 0.340s | 137.0MiB| unsat | 0 | | | |auk-0122.smt2 | 0.342s | 143.0MiB| sat | 0 | | | |auk-0116.smt2 | 0.349s | 142.0MiB| sat | 0 | | | |auk-0128.smt2 | 0.354s | 151.0MiB| sat | 0 | | | |auk-0096.smt2 | 0.376s | 134.0MiB| sat | 0 | | | |auk-0135.smt2 | 0.376s | 129.0MiB| unsat | 0 | | | |auk-0070.smt2 | 0.381s | 148.0MiB| sat | 0 | | | |auk-0119.smt2 | 0.394s | 159.0MiB| sat | 0 | | | |auk-0123.smt2 | 0.402s | 149.0MiB| sat | 0 | | | |auk-0120.smt2 | 0.423s | 145.0MiB| sat | 0 | | | |auk-0001.smt2 | 0.429s | 97.236MiB| sat | 0 | | | |auk-0115.smt2 | 0.465s | 158.0MiB| sat | 0 | | | |auk-0134.smt2 | 0.488s | 152.0MiB| sat | 0 | | | |auk-0074.smt2 | 0.502s | 149.0MiB| unsat | 0 | | | |auk-0056.smt2 | 0.511s | 124.0MiB| sat | 0 | | | |auk-0081.smt2 | 0.522s | 160.0MiB| unsat | 0 | | | |auk-0080.smt2 | 0.547s | 162.0MiB| sat | 0 | | | |auk-0072.smt2 | 0.548s | 149.0MiB| sat | 0 | | | |auk-0094.smt2 | 0.565s | 149.0MiB| sat | 0 | | | |auk-0078.smt2 | 0.613s | 149.0MiB| sat | 0 | | | |auk-0091.smt2 | 0.665s | 183.0MiB| sat | 0 | | | |auk-0101.smt2 | 0.755s | 149.0MiB| unsat | 0 | | | |auk-0146.smt2 | 0.760s | 131.0MiB| unsat | 0 | | | |auk-0149.smt2 | 0.833s | 130.0MiB| unsat | 0 | | | |auk-0133.smt2 | 0.917s | 190.0MiB| sat | 0 | | | |auk-0145.smt2 | 0.986s | 140.0MiB| unsat | 0 | | | |auk-0006.smt2 | 1.141s | 170.0MiB| unsat | 0 | | | |auk-0109.smt2 | 1.206s | 380.0MiB| sat | 0 | | | |auk-0075.smt2 | 1.308s | 198.0MiB| sat | 0 | | | |auk-0076.smt2 | 1.352s | 198.0MiB| sat | 0 | | | |auk-0071.smt2 | 1.358s | 197.0MiB| sat | 0 | | | |auk-0073.smt2 | 1.363s | 197.0MiB| sat | 0 | | | |auk-0144.smt2 | 1.398s | 151.0MiB| unsat | 0 | | | |auk-0077.smt2 | 1.424s | 188.0MiB| sat | 0 | | | |auk-0079.smt2 | 1.469s | 201.0MiB| unset | 139 | | | |auk-0142.smt2 | 1.479s | 156.0MiB| unsat | 0 | | | |auk-0095.smt2 | 1.626s | 160.0MiB| unsat | 0 | | | |auk-0183.smt2 | 1.965s | 226.0MiB| unsat | 0 | | | |auk-0148.smt2 | 2.020s | 154.0MiB| unsat | 0 | | | |auk-0004.smt2 | 2.165s | 175.0MiB| unsat | 0 | | | |auk-0132.smt2 | 2.219s | 209.0MiB| sat | 0 | | | |auk-0082.smt2 | 2.930s | 329.0MiB| sat | 0 | | | |auk-0083.smt2 | 3.072s | 329.0MiB| sat | 0 | | | |auk-0131.smt2 | 4.067s | 330.0MiB| sat | 0 | | | |auk-0002.smt2 | 4.365s | 216.0MiB| unsat | 0 | | | |auk-0087.smt2 | 5.183s | 245.0MiB| unsat | 0 | | | |auk-0084.smt2 | 5.507s | 225.0MiB| unsat | 0 | | | |auk-0090.smt2 | 6.290s | 220.0MiB| unsat | 0 | | | |auk-0007.smt2 | 6.732s | 176.0MiB| sat | 0 | | | |auk-0141.smt2 | 7.130s | 188.0MiB| unsat | 0 | | | |auk-0182.smt2 | 7.389s | 241.0MiB| unsat | 0 | | | |auk-0140.smt2 | 7.909s | 173.0MiB| unsat | 0 | | | |auk-0185.smt2 | 8.165s | 202.0MiB| unsat | 0 | | | |auk-0137.smt2 | 14.776s | 139.0MiB| sat | 0 | | | |auk-0089.smt2 | 18.619s | 262.0MiB| unsat | 0 | | | |auk-0151.smt2 | 20.051s | 134.0MiB| unsat | 0 | | | |auk-0010.smt2 | 30.027s | 199.0MiB| timeout | 0 | | | |auk-0187.smt2 | 30.035s | 211.0MiB| timeout | 0 | | | |auk-0005.smt2 | 30.038s | 217.0MiB| timeout | 0 | | | |auk-0092.smt2 | 30.041s | 365.0MiB| timeout | 0 | | | |auk-0189.smt2 | 30.044s | 208.0MiB| timeout | 0 | | | |auk-0139.smt2 | 30.045s | 129.0MiB| timeout | 0 | | | |auk-0008.smt2 | 30.046s | 222.0MiB| timeout | 0 | | | |auk-0003.smt2 | 30.046s | 208.0MiB| timeout | 0 | | | |auk-0147.smt2 | 30.046s | 176.0MiB| timeout | 0 | | | |auk-0184.smt2 | 30.046s | 214.0MiB| timeout | 0 | | | |auk-0014.smt2 | 30.048s | 220.0MiB| timeout | 0 | | | |auk-0015.smt2 | 30.050s | 228.0MiB| timeout | 0 | | | |auk-0086.smt2 | 30.052s | 355.0MiB| timeout | 0 | | | |auk-0013.smt2 | 30.055s | 218.0MiB| timeout | 0 | | | |auk-0011.smt2 | 30.055s | 210.0MiB| timeout | 0 | | | |auk-0085.smt2 | 30.056s | 315.0MiB| timeout | 0 | | | |auk-0088.smt2 | 30.056s | 320.0MiB| timeout | 0 | | | |auk-0181.smt2 | 30.061s | 268.0MiB| timeout | 0 | | | |auk-0186.smt2 | 30.062s | 282.0MiB| timeout | 0 | | | |auk-0188.smt2 | 30.078s | 477.0MiB| timeout | 0 | | | |auk-0099.smt2 | 30.102s | 781.0MiB| timeout | 0 | | | |auk-0098.smt2 | 30.133s | 907.0MiB| timeout | 0 | | |