# . * SAT 87 * UNSAT 74 * TIMEOUT 28 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: certora2-poly
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"
Z3 inputs: inputs/certora2
Z3 commit message: fixing coi bug

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |auk-0161.smt2 | 0.042s | 19.5MiB| sat | 0 | | | |auk-0069.smt2 | 0.045s | 20.16MiB| unsat | 0 | | | |auk-0138.smt2 | 0.047s | 20.264MiB| unsat | 0 | | | |auk-0057.smt2 | 0.048s | 20.264MiB| unsat | 0 | | | |auk-0054.smt2 | 0.055s | 19.548MiB| unsat | 0 | | | |auk-0068.smt2 | 0.059s | 19.484MiB| unsat | 0 | | | |auk-0046.smt2 | 0.059s | 20.204MiB| unsat | 0 | | | |auk-0041.smt2 | 0.063s | 20.436MiB| unsat | 0 | | | |auk-0067.smt2 | 0.064s | 20.28MiB| sat | 0 | | | |auk-0042.smt2 | 0.067s | 20.112MiB| sat | 0 | | | |auk-0038.smt2 | 0.071s | 19.736MiB| unsat | 0 | | | |auk-0031.smt2 | 0.073s | 20.104MiB| unsat | 0 | | | |auk-0179.smt2 | 0.074s | 20.084MiB| unsat | 0 | | | |auk-0178.smt2 | 0.074s | 19.956MiB| sat | 0 | | | |auk-0066.smt2 | 0.076s | 19.968MiB| sat | 0 | | | |auk-0064.smt2 | 0.078s | 20.784MiB| sat | 0 | | | |auk-0060.smt2 | 0.079s | 20.1MiB| unsat | 0 | | | |auk-0160.smt2 | 0.081s | 20.252MiB| unsat | 0 | | | |auk-0168.smt2 | 0.081s | 20.368MiB| sat | 0 | | | |auk-0061.smt2 | 0.087s | 20.476MiB| unsat | 0 | | | |auk-0050.smt2 | 0.094s | 20.384MiB| unsat | 0 | | | |auk-0012.smt2 | 0.102s | 21.136MiB| unsat | 0 | | | |auk-0052.smt2 | 0.102s | 27.212MiB| unsat | 0 | | | |auk-0044.smt2 | 0.102s | 26.172MiB| unsat | 0 | | | |auk-0065.smt2 | 0.105s | 24.56MiB| unsat | 0 | | | |auk-0032.smt2 | 0.106s | 26.176MiB| unsat | 0 | | | |auk-0170.smt2 | 0.106s | 20.484MiB| unsat | 0 | | | |auk-0166.smt2 | 0.107s | 21.316MiB| sat | 0 | | | |auk-0036.smt2 | 0.109s | 21.392MiB| sat | 0 | | | |auk-0159.smt2 | 0.110s | 20.516MiB| unsat | 0 | | | |auk-0043.smt2 | 0.114s | 26.46MiB| unsat | 0 | | | |auk-0051.smt2 | 0.116s | 21.276MiB| unsat | 0 | | | |auk-0019.smt2 | 0.120s | 27.552MiB| unsat | 0 | | | |auk-0035.smt2 | 0.120s | 23.404MiB| unsat | 0 | | | |auk-0024.smt2 | 0.126s | 26.856MiB| unsat | 0 | | | |auk-0040.smt2 | 0.127s | 20.792MiB| unsat | 0 | | | |auk-0063.smt2 | 0.129s | 26.212MiB| unsat | 0 | | | |auk-0028.smt2 | 0.130s | 24.16MiB| unsat | 0 | | | |auk-0059.smt2 | 0.130s | 25.188MiB| unsat | 0 | | | |auk-0034.smt2 | 0.137s | 25.016MiB| unsat | 0 | | | |auk-0100.smt2 | 0.142s | 28.172MiB| sat | 0 | | | |auk-0055.smt2 | 0.144s | 27.852MiB| sat | 0 | | | |auk-0026.smt2 | 0.150s | 27.22MiB| unsat | 0 | | | |auk-0016.smt2 | 0.155s | 26.78MiB| unsat | 0 | | | |auk-0018.smt2 | 0.155s | 27.424MiB| unsat | 0 | | | |auk-0157.smt2 | 0.167s | 30.748MiB| sat | 0 | | | |auk-0158.smt2 | 0.168s | 28.156MiB| sat | 0 | | | |auk-0125.smt2 | 0.170s | 31.944MiB| sat | 0 | | | |auk-0039.smt2 | 0.171s | 26.888MiB| unsat | 0 | | | |auk-0021.smt2 | 0.172s | 26.224MiB| unsat | 0 | | | |auk-0049.smt2 | 0.175s | 21.124MiB| unsat | 0 | | | |auk-0045.smt2 | 0.175s | 27.516MiB| unsat | 0 | | | |auk-0177.smt2 | 0.177s | 31.596MiB| sat | 0 | | | |auk-0172.smt2 | 0.180s | 30.208MiB| sat | 0 | | | |auk-0093.smt2 | 0.180s | 26.956MiB| sat | 0 | | | |auk-0020.smt2 | 0.181s | 27.088MiB| unsat | 0 | | | |auk-0163.smt2 | 0.183s | 29.776MiB| sat | 0 | | | |auk-0037.smt2 | 0.186s | 28.144MiB| unsat | 0 | | | |auk-0165.smt2 | 0.186s | 30.964MiB| sat | 0 | | | |auk-0047.smt2 | 0.188s | 27.436MiB| unsat | 0 | | | |auk-0155.smt2 | 0.189s | 31.692MiB| sat | 0 | | | |auk-0169.smt2 | 0.191s | 30.844MiB| unsat | 0 | | | |auk-0058.smt2 | 0.194s | 27.384MiB| sat | 0 | | | |auk-0023.smt2 | 0.198s | 29.516MiB| unsat | 0 | | | |auk-0097.smt2 | 0.203s | 25.648MiB| sat | 0 | | | |auk-0152.smt2 | 0.208s | 28.54MiB| sat | 0 | | | |auk-0114.smt2 | 0.208s | 30.08MiB| sat | 0 | | | |auk-0129.smt2 | 0.211s | 28.62MiB| sat | 0 | | | |auk-0030.smt2 | 0.213s | 27.56MiB| unsat | 0 | | | |auk-0174.smt2 | 0.218s | 30.896MiB| sat | 0 | | | |auk-0104.smt2 | 0.219s | 27.488MiB| sat | 0 | | | |auk-0048.smt2 | 0.221s | 28.412MiB| unsat | 0 | | | |auk-0118.smt2 | 0.226s | 32.908MiB| sat | 0 | | | |auk-0164.smt2 | 0.231s | 29.764MiB| sat | 0 | | | |auk-0108.smt2 | 0.233s | 34.656MiB| sat | 0 | | | |auk-0173.smt2 | 0.237s | 30.172MiB| sat | 0 | | | |auk-0150.smt2 | 0.238s | 28.916MiB| unsat | 0 | | | |auk-0156.smt2 | 0.239s | 31.624MiB| sat | 0 | | | |auk-0033.smt2 | 0.240s | 28.98MiB| sat | 0 | | | |auk-0171.smt2 | 0.245s | 32.22MiB| sat | 0 | | | |auk-0017.smt2 | 0.246s | 30.024MiB| unsat | 0 | | | |auk-0162.smt2 | 0.248s | 28.036MiB| sat | 0 | | | |auk-0029.smt2 | 0.252s | 28.416MiB| unsat | 0 | | | |auk-0105.smt2 | 0.257s | 32.384MiB| sat | 0 | | | |auk-0110.smt2 | 0.258s | 28.128MiB| sat | 0 | | | |auk-0176.smt2 | 0.263s | 31.476MiB| sat | 0 | | | |auk-0154.smt2 | 0.265s | 30.496MiB| sat | 0 | | | |auk-0121.smt2 | 0.269s | 31.152MiB| sat | 0 | | | |auk-0180.smt2 | 0.269s | 30.084MiB| unsat | 0 | | | |auk-0102.smt2 | 0.274s | 32.196MiB| sat | 0 | | | |auk-0122.smt2 | 0.289s | 34.832MiB| sat | 0 | | | |auk-0107.smt2 | 0.291s | 31.6MiB| sat | 0 | | | |auk-0103.smt2 | 0.293s | 33.032MiB| sat | 0 | | | |auk-0175.smt2 | 0.293s | 31.856MiB| sat | 0 | | | |auk-0112.smt2 | 0.296s | 32.988MiB| sat | 0 | | | |auk-0167.smt2 | 0.300s | 31.372MiB| sat | 0 | | | |auk-0009.smt2 | 0.303s | 21.88MiB| sat | 0 | | | |auk-0127.smt2 | 0.304s | 32.616MiB| sat | 0 | | | |auk-0126.smt2 | 0.305s | 33.688MiB| sat | 0 | | | |auk-0062.smt2 | 0.310s | 30.74MiB| unsat | 0 | | | |auk-0136.smt2 | 0.310s | 21.008MiB| sat | 0 | | | |auk-0124.smt2 | 0.312s | 32.44MiB| sat | 0 | | | |auk-0106.smt2 | 0.322s | 32.28MiB| sat | 0 | | | |auk-0111.smt2 | 0.329s | 32.576MiB| sat | 0 | | | |auk-0153.smt2 | 0.336s | 31.564MiB| sat | 0 | | | |auk-0117.smt2 | 0.371s | 35.604MiB| sat | 0 | | | |auk-0120.smt2 | 0.420s | 35.656MiB| sat | 0 | | | |auk-0113.smt2 | 0.420s | 35.148MiB| sat | 0 | | | |auk-0135.smt2 | 0.451s | 30.868MiB| unsat | 0 | | | |auk-0128.smt2 | 0.472s | 36.968MiB| sat | 0 | | | |auk-0080.smt2 | 0.540s | 40.424MiB| sat | 0 | | | |auk-0056.smt2 | 0.546s | 29.78MiB| sat | 0 | | | |auk-0123.smt2 | 0.568s | 35.7MiB| sat | 0 | | | |auk-0115.smt2 | 0.592s | 40.432MiB| sat | 0 | | | |auk-0078.smt2 | 0.622s | 34.588MiB| sat | 0 | | | |auk-0070.smt2 | 0.624s | 36.668MiB| sat | 0 | | | |auk-0094.smt2 | 0.651s | 35.528MiB| sat | 0 | | | |auk-0053.smt2 | 0.661s | 21.904MiB| sat | 0 | | | |auk-0133.smt2 | 0.723s | 44.172MiB| sat | 0 | | | |auk-0143.smt2 | 0.817s | 22.028MiB| unsat | 0 | | | |auk-0072.smt2 | 0.827s | 34.624MiB| sat | 0 | | | |auk-0074.smt2 | 0.899s | 36.292MiB| unsat | 0 | | | |auk-0096.smt2 | 0.910s | 33.356MiB| sat | 0 | | | |auk-0116.smt2 | 0.924s | 34.188MiB| sat | 0 | | | |auk-0109.smt2 | 0.962s | 98.0MiB| sat | 0 | | | |auk-0146.smt2 | 1.136s | 32.036MiB| unsat | 0 | | | |auk-0071.smt2 | 1.141s | 47.052MiB| sat | 0 | | | |auk-0022.smt2 | 1.148s | 30.576MiB| sat | 0 | | | |auk-0187.smt2 | 1.177s | 46.184MiB| unsat | 0 | | | |auk-0145.smt2 | 1.259s | 34.116MiB| unsat | 0 | | | |auk-0130.smt2 | 1.262s | 38.56MiB| sat | 0 | | | |auk-0076.smt2 | 1.302s | 47.056MiB| sat | 0 | | | |auk-0073.smt2 | 1.372s | 47.008MiB| sat | 0 | | | |auk-0075.smt2 | 1.403s | 47.016MiB| sat | 0 | | | |auk-0119.smt2 | 1.469s | 41.064MiB| sat | 0 | | | |auk-0132.smt2 | 1.917s | 63.608MiB| sat | 0 | | | |auk-0185.smt2 | 1.984s | 46.348MiB| unsat | 0 | | | |auk-0027.smt2 | 2.201s | 30.888MiB| unsat | 0 | | | |auk-0149.smt2 | 2.370s | 31.348MiB| unsat | 0 | | | |auk-0081.smt2 | 2.421s | 42.2MiB| unsat | 0 | | | |auk-0095.smt2 | 2.456s | 38.904MiB| unsat | 0 | | | |auk-0182.smt2 | 2.655s | 51.848MiB| unsat | 0 | | | |auk-0083.smt2 | 2.748s | 98.0MiB| sat | 0 | | | |auk-0148.smt2 | 2.791s | 37.26MiB| unsat | 0 | | | |auk-0082.smt2 | 2.928s | 99.0MiB| sat | 0 | | | |auk-0101.smt2 | 3.069s | 39.78MiB| unsat | 0 | | | |auk-0144.smt2 | 3.125s | 37.82MiB| unsat | 0 | | | |auk-0142.smt2 | 3.265s | 37.772MiB| unsat | 0 | | | |auk-0006.smt2 | 3.518s | 41.996MiB| unsat | 0 | | | |auk-0131.smt2 | 3.554s | 99.048MiB| sat | 0 | | | |auk-0077.smt2 | 4.362s | 54.26MiB| sat | 0 | | | |auk-0079.smt2 | 6.698s | 56.704MiB| sat | 0 | | | |auk-0183.smt2 | 7.000s | 64.188MiB| unsat | 0 | | | |auk-0010.smt2 | 7.309s | 46.9MiB| unsat | 0 | | | |auk-0134.smt2 | 8.026s | 40.716MiB| sat | 0 | | | |auk-0025.smt2 | 11.410s | 36.636MiB| unsat | 0 | | | |auk-0084.smt2 | 11.481s | 56.608MiB| unsat | 0 | | | |auk-0090.smt2 | 14.138s | 60.42MiB| unsat | 0 | | | |auk-0151.smt2 | 14.585s | 29.028MiB| unsat | 0 | | | |auk-0141.smt2 | 15.197s | 47.776MiB| unsat | 0 | | | |auk-0137.smt2 | 21.142s | 37.5MiB| sat | 0 | | | |auk-0001.smt2 | 30.012s | 25.16MiB| timeout | 0 | | | |auk-0140.smt2 | 30.014s | 44.024MiB| timeout | 0 | | | |auk-0147.smt2 | 30.014s | 31.924MiB| timeout | 0 | | | |auk-0189.smt2 | 30.014s | 54.708MiB| timeout | 0 | | | |auk-0004.smt2 | 30.016s | 44.16MiB| timeout | 0 | | | |auk-0013.smt2 | 30.017s | 53.916MiB| timeout | 0 | | | |auk-0085.smt2 | 30.017s | 74.248MiB| timeout | 0 | | | |auk-0003.smt2 | 30.017s | 54.44MiB| timeout | 0 | | | |auk-0005.smt2 | 30.018s | 51.02MiB| timeout | 0 | | | |auk-0002.smt2 | 30.019s | 46.868MiB| timeout | 0 | | | |auk-0007.smt2 | 30.019s | 39.248MiB| timeout | 0 | | | |auk-0184.smt2 | 30.020s | 54.292MiB| timeout | 0 | | | |auk-0188.smt2 | 30.021s | 53.304MiB| timeout | 0 | | | |auk-0087.smt2 | 30.021s | 72.944MiB| timeout | 0 | | | |auk-0091.smt2 | 30.021s | 49.928MiB| timeout | 0 | | | |auk-0008.smt2 | 30.021s | 53.784MiB| timeout | 0 | | | |auk-0181.smt2 | 30.022s | 65.656MiB| timeout | 0 | | | |auk-0099.smt2 | 30.023s | 145.0MiB| timeout | 0 | | | |auk-0015.smt2 | 30.023s | 56.476MiB| timeout | 0 | | | |auk-0011.smt2 | 30.024s | 46.756MiB| timeout | 0 | | | |auk-0089.smt2 | 30.024s | 72.54MiB| timeout | 0 | | | |auk-0086.smt2 | 30.024s | 92.652MiB| timeout | 0 | | | |auk-0088.smt2 | 30.029s | 80.012MiB| timeout | 0 | | | |auk-0139.smt2 | 30.029s | 33.052MiB| timeout | 0 | | | |auk-0186.smt2 | 30.035s | 67.732MiB| timeout | 0 | | | |auk-0098.smt2 | 30.037s | 147.0MiB| timeout | 0 | | | |auk-0092.smt2 | 30.038s | 82.664MiB| timeout | 0 | | | |auk-0014.smt2 | 30.090s | 55.668MiB| timeout | 0 | | |