# . * SAT 88 * UNSAT 78 * TIMEOUT 23 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: certora2-poly-seed-2
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: ed84b14e6c7dfaf6efd1b740119ecb1631e8bdfb
Z3 branch: arie
Z3 options: "-T:30 smt.arith.nl.nra.poly=true smt.random_seed=2"
Z3 inputs: inputs/certora2
Z3 commit message: fixing coi bug

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |auk-0060.smt2 | 0.032s | 20.028MiB| unsat | 0 | | | |auk-0179.smt2 | 0.034s | 19.912MiB| unsat | 0 | | | |auk-0066.smt2 | 0.035s | 19.716MiB| sat | 0 | | | |auk-0054.smt2 | 0.035s | 18.976MiB| unsat | 0 | | | |auk-0161.smt2 | 0.036s | 19.48MiB| sat | 0 | | | |auk-0168.smt2 | 0.037s | 20.088MiB| sat | 0 | | | |auk-0038.smt2 | 0.039s | 18.956MiB| unsat | 0 | | | |auk-0046.smt2 | 0.044s | 19.74MiB| unsat | 0 | | | |auk-0069.smt2 | 0.048s | 19.984MiB| unsat | 0 | | | |auk-0068.smt2 | 0.048s | 19.74MiB| unsat | 0 | | | |auk-0178.smt2 | 0.049s | 19.716MiB| sat | 0 | | | |auk-0057.smt2 | 0.050s | 19.992MiB| unsat | 0 | | | |auk-0009.smt2 | 0.050s | 20.276MiB| sat | 0 | | | |auk-0050.smt2 | 0.051s | 20.252MiB| unsat | 0 | | | |auk-0042.smt2 | 0.052s | 20.08MiB| sat | 0 | | | |auk-0159.smt2 | 0.053s | 20.368MiB| unsat | 0 | | | |auk-0170.smt2 | 0.054s | 20.512MiB| unsat | 0 | | | |auk-0040.smt2 | 0.054s | 20.244MiB| unsat | 0 | | | |auk-0138.smt2 | 0.059s | 20.296MiB| unsat | 0 | | | |auk-0041.smt2 | 0.062s | 20.192MiB| unsat | 0 | | | |auk-0031.smt2 | 0.062s | 20.228MiB| unsat | 0 | | | |auk-0160.smt2 | 0.065s | 19.992MiB| unsat | 0 | | | |auk-0053.smt2 | 0.066s | 21.048MiB| sat | 0 | | | |auk-0012.smt2 | 0.068s | 20.296MiB| unsat | 0 | | | |auk-0067.smt2 | 0.074s | 20.256MiB| sat | 0 | | | |auk-0035.smt2 | 0.084s | 20.128MiB| unsat | 0 | | | |auk-0097.smt2 | 0.085s | 22.884MiB| sat | 0 | | | |auk-0166.smt2 | 0.087s | 21.164MiB| sat | 0 | | | |auk-0061.smt2 | 0.093s | 20.732MiB| unsat | 0 | | | |auk-0036.smt2 | 0.094s | 20.896MiB| sat | 0 | | | |auk-0032.smt2 | 0.095s | 20.428MiB| unsat | 0 | | | |auk-0065.smt2 | 0.104s | 20.596MiB| unsat | 0 | | | |auk-0028.smt2 | 0.105s | 22.52MiB| unsat | 0 | | | |auk-0058.smt2 | 0.105s | 24.652MiB| sat | 0 | | | |auk-0093.smt2 | 0.105s | 24.452MiB| sat | 0 | | | |auk-0059.smt2 | 0.106s | 22.788MiB| unsat | 0 | | | |auk-0055.smt2 | 0.107s | 24.832MiB| sat | 0 | | | |auk-0044.smt2 | 0.108s | 20.676MiB| unsat | 0 | | | |auk-0034.smt2 | 0.109s | 20.68MiB| unsat | 0 | | | |auk-0051.smt2 | 0.112s | 20.812MiB| unsat | 0 | | | |auk-0064.smt2 | 0.112s | 21.264MiB| sat | 0 | | | |auk-0047.smt2 | 0.119s | 25.492MiB| unsat | 0 | | | |auk-0100.smt2 | 0.120s | 24.532MiB| sat | 0 | | | |auk-0157.smt2 | 0.127s | 24.968MiB| sat | 0 | | | |auk-0062.smt2 | 0.133s | 24.716MiB| unsat | 0 | | | |auk-0052.smt2 | 0.135s | 24.78MiB| unsat | 0 | | | |auk-0125.smt2 | 0.142s | 26.824MiB| sat | 0 | | | |auk-0063.smt2 | 0.145s | 20.784MiB| unsat | 0 | | | |auk-0039.smt2 | 0.146s | 20.672MiB| unsat | 0 | | | |auk-0019.smt2 | 0.148s | 25.968MiB| unsat | 0 | | | |auk-0037.smt2 | 0.150s | 25.704MiB| unsat | 0 | | | |auk-0176.smt2 | 0.150s | 26.432MiB| sat | 0 | | | |auk-0026.smt2 | 0.150s | 24.764MiB| unsat | 0 | | | |auk-0169.smt2 | 0.152s | 25.836MiB| unsat | 0 | | | |auk-0110.smt2 | 0.152s | 24.852MiB| sat | 0 | | | |auk-0172.smt2 | 0.156s | 25.668MiB| sat | 0 | | | |auk-0162.smt2 | 0.158s | 24.424MiB| sat | 0 | | | |auk-0003.smt2 | 0.159s | 27.844MiB| unsat | 0 | | | |auk-0048.smt2 | 0.161s | 25.368MiB| unsat | 0 | | | |auk-0043.smt2 | 0.165s | 24.332MiB| unsat | 0 | | | |auk-0150.smt2 | 0.165s | 25.676MiB| unsat | 0 | | | |auk-0155.smt2 | 0.166s | 25.268MiB| sat | 0 | | | |auk-0008.smt2 | 0.166s | 27.844MiB| unsat | 0 | | | |auk-0156.smt2 | 0.166s | 25.128MiB| sat | 0 | | | |auk-0163.smt2 | 0.167s | 25.7MiB| sat | 0 | | | |auk-0104.smt2 | 0.169s | 24.088MiB| sat | 0 | | | |auk-0114.smt2 | 0.169s | 25.756MiB| sat | 0 | | | |auk-0174.smt2 | 0.171s | 25.676MiB| sat | 0 | | | |auk-0030.smt2 | 0.171s | 25.008MiB| unsat | 0 | | | |auk-0045.smt2 | 0.173s | 25.28MiB| unsat | 0 | | | |auk-0049.smt2 | 0.177s | 21.144MiB| unsat | 0 | | | |auk-0102.smt2 | 0.179s | 27.136MiB| sat | 0 | | | |auk-0173.smt2 | 0.181s | 25.852MiB| sat | 0 | | | |auk-0177.smt2 | 0.182s | 26.448MiB| sat | 0 | | | |auk-0106.smt2 | 0.186s | 26.756MiB| sat | 0 | | | |auk-0171.smt2 | 0.187s | 25.624MiB| sat | 0 | | | |auk-0136.smt2 | 0.188s | 20.868MiB| sat | 0 | | | |auk-0139.smt2 | 0.188s | 21.688MiB| unsat | 0 | | | |auk-0029.smt2 | 0.191s | 25.756MiB| unsat | 0 | | | |auk-0024.smt2 | 0.193s | 25.572MiB| unsat | 0 | | | |auk-0020.smt2 | 0.195s | 25.424MiB| unsat | 0 | | | |auk-0013.smt2 | 0.195s | 27.968MiB| unsat | 0 | | | |auk-0118.smt2 | 0.197s | 27.188MiB| sat | 0 | | | |auk-0129.smt2 | 0.197s | 25.004MiB| sat | 0 | | | |auk-0107.smt2 | 0.200s | 26.708MiB| sat | 0 | | | |auk-0033.smt2 | 0.200s | 26.144MiB| sat | 0 | | | |auk-0124.smt2 | 0.202s | 26.916MiB| sat | 0 | | | |auk-0175.smt2 | 0.206s | 26.38MiB| sat | 0 | | | |auk-0165.smt2 | 0.208s | 25.304MiB| sat | 0 | | | |auk-0121.smt2 | 0.209s | 26.464MiB| sat | 0 | | | |auk-0126.smt2 | 0.212s | 28.472MiB| sat | 0 | | | |auk-0152.smt2 | 0.215s | 24.996MiB| sat | 0 | | | |auk-0021.smt2 | 0.216s | 23.26MiB| unsat | 0 | | | |auk-0167.smt2 | 0.216s | 25.284MiB| sat | 0 | | | |auk-0108.smt2 | 0.221s | 28.332MiB| sat | 0 | | | |auk-0014.smt2 | 0.228s | 28.0MiB| unsat | 0 | | | |auk-0112.smt2 | 0.231s | 27.008MiB| sat | 0 | | | |auk-0164.smt2 | 0.231s | 25.576MiB| sat | 0 | | | |auk-0154.smt2 | 0.233s | 26.324MiB| sat | 0 | | | |auk-0158.smt2 | 0.234s | 25.148MiB| sat | 0 | | | |auk-0153.smt2 | 0.234s | 26.32MiB| sat | 0 | | | |auk-0111.smt2 | 0.236s | 28.42MiB| sat | 0 | | | |auk-0127.smt2 | 0.239s | 26.544MiB| sat | 0 | | | |auk-0143.smt2 | 0.258s | 21.0MiB| unsat | 0 | | | |auk-0018.smt2 | 0.259s | 27.704MiB| unsat | 0 | | | |auk-0017.smt2 | 0.261s | 28.624MiB| unsat | 0 | | | |auk-0016.smt2 | 0.268s | 25.484MiB| unsat | 0 | | | |auk-0105.smt2 | 0.277s | 27.148MiB| sat | 0 | | | |auk-0103.smt2 | 0.289s | 27.676MiB| sat | 0 | | | |auk-0113.smt2 | 0.290s | 29.408MiB| sat | 0 | | | |auk-0180.smt2 | 0.328s | 28.82MiB| unsat | 0 | | | |auk-0122.smt2 | 0.332s | 31.064MiB| sat | 0 | | | |auk-0002.smt2 | 0.355s | 34.452MiB| unsat | 0 | | | |auk-0116.smt2 | 0.358s | 31.296MiB| sat | 0 | | | |auk-0023.smt2 | 0.379s | 27.256MiB| unsat | 0 | | | |auk-0128.smt2 | 0.381s | 32.3MiB| sat | 0 | | | |auk-0120.smt2 | 0.395s | 31.628MiB| sat | 0 | | | |auk-0123.smt2 | 0.403s | 31.304MiB| sat | 0 | | | |auk-0130.smt2 | 0.429s | 33.512MiB| sat | 0 | | | |auk-0056.smt2 | 0.436s | 26.656MiB| sat | 0 | | | |auk-0004.smt2 | 0.446s | 34.376MiB| unsat | 0 | | | |auk-0006.smt2 | 0.454s | 34.772MiB| unsat | 0 | | | |auk-0010.smt2 | 0.468s | 34.356MiB| unsat | 0 | | | |auk-0015.smt2 | 0.537s | 35.568MiB| unsat | 0 | | | |auk-0070.smt2 | 0.545s | 31.356MiB| sat | 0 | | | |auk-0022.smt2 | 0.547s | 28.212MiB| sat | 0 | | | |auk-0096.smt2 | 0.549s | 28.756MiB| sat | 0 | | | |auk-0109.smt2 | 0.577s | 44.556MiB| sat | 0 | | | |auk-0135.smt2 | 0.594s | 27.82MiB| unsat | 0 | | | |auk-0119.smt2 | 0.653s | 35.212MiB| sat | 0 | | | |auk-0025.smt2 | 0.658s | 30.644MiB| unsat | 0 | | | |auk-0078.smt2 | 0.692s | 32.2MiB| sat | 0 | | | |auk-0115.smt2 | 0.767s | 35.66MiB| sat | 0 | | | |auk-0072.smt2 | 0.810s | 32.14MiB| sat | 0 | | | |auk-0145.smt2 | 0.852s | 30.512MiB| unsat | 0 | | | |auk-0151.smt2 | 0.860s | 22.42MiB| unsat | 0 | | | |auk-0133.smt2 | 0.913s | 42.18MiB| sat | 0 | | | |auk-0149.smt2 | 0.998s | 29.304MiB| unsat | 0 | | | |auk-0132.smt2 | 1.034s | 55.092MiB| sat | 0 | | | |auk-0077.smt2 | 1.047s | 41.236MiB| sat | 0 | | | |auk-0094.smt2 | 1.065s | 31.024MiB| sat | 0 | | | |auk-0117.smt2 | 1.076s | 32.184MiB| sat | 0 | | | |auk-0091.smt2 | 1.123s | 42.92MiB| sat | 0 | | | |auk-0071.smt2 | 1.151s | 47.104MiB| sat | 0 | | | |auk-0073.smt2 | 1.239s | 47.204MiB| sat | 0 | | | |auk-0144.smt2 | 1.249s | 33.72MiB| unsat | 0 | | | |auk-0101.smt2 | 1.284s | 32.068MiB| unsat | 0 | | | |auk-0075.smt2 | 1.357s | 47.284MiB| sat | 0 | | | |auk-0076.smt2 | 1.373s | 47.244MiB| sat | 0 | | | |auk-0131.smt2 | 1.643s | 91.264MiB| sat | 0 | | | |auk-0146.smt2 | 2.338s | 29.808MiB| unsat | 0 | | | |auk-0027.smt2 | 2.359s | 29.664MiB| unsat | 0 | | | |auk-0080.smt2 | 2.378s | 34.816MiB| sat | 0 | | | |auk-0148.smt2 | 2.406s | 35.04MiB| unsat | 0 | | | |auk-0134.smt2 | 2.603s | 33.228MiB| sat | 0 | | | |auk-0083.smt2 | 2.816s | 99.0MiB| sat | 0 | | | |auk-0082.smt2 | 2.915s | 99.0MiB| sat | 0 | | | |auk-0079.smt2 | 3.120s | 45.012MiB| sat | 0 | | | |auk-0183.smt2 | 3.560s | 66.272MiB| unsat | 0 | | | |auk-0142.smt2 | 4.541s | 36.368MiB| unsat | 0 | | | |auk-0137.smt2 | 7.933s | 29.568MiB| sat | 0 | | | |auk-0074.smt2 | 12.514s | 33.196MiB| unsat | 0 | | | |auk-0084.smt2 | 14.471s | 57.444MiB| unsat | 0 | | | |auk-0141.smt2 | 14.868s | 50.416MiB| unsat | 0 | | | |auk-0187.smt2 | 20.869s | 56.776MiB| unsat | 0 | | | |auk-0182.smt2 | 29.308s | 77.108MiB| unsat | 0 | | | |auk-0147.smt2 | 30.010s | 31.792MiB| timeout | 0 | | | |auk-0184.smt2 | 30.011s | 46.932MiB| timeout | 0 | | | |auk-0095.smt2 | 30.012s | 40.92MiB| timeout | 0 | | | |auk-0188.smt2 | 30.015s | 54.04MiB| timeout | 0 | | | |auk-0001.smt2 | 30.015s | 31.432MiB| timeout | 0 | | | |auk-0087.smt2 | 30.016s | 66.348MiB| timeout | 0 | | | |auk-0140.smt2 | 30.016s | 46.752MiB| timeout | 0 | | | |auk-0005.smt2 | 30.017s | 47.564MiB| timeout | 0 | | | |auk-0189.smt2 | 30.017s | 61.96MiB| timeout | 0 | | | |auk-0007.smt2 | 30.018s | 48.884MiB| timeout | 0 | | | |auk-0081.smt2 | 30.019s | 36.088MiB| timeout | 0 | | | |auk-0181.smt2 | 30.019s | 81.664MiB| timeout | 0 | | | |auk-0090.smt2 | 30.019s | 65.788MiB| timeout | 0 | | | |auk-0092.smt2 | 30.020s | 94.472MiB| timeout | 0 | | | |auk-0085.smt2 | 30.020s | 98.596MiB| timeout | 0 | | | |auk-0185.smt2 | 30.021s | 53.244MiB| timeout | 0 | | | |auk-0089.smt2 | 30.022s | 73.532MiB| timeout | 0 | | | |auk-0086.smt2 | 30.023s | 104.0MiB| timeout | 0 | | | |auk-0099.smt2 | 30.027s | 161.0MiB| timeout | 0 | | | |auk-0186.smt2 | 30.028s | 75.72MiB| timeout | 0 | | | |auk-0088.smt2 | 30.032s | 101.0MiB| timeout | 0 | | | |auk-0011.smt2 | 30.034s | 45.904MiB| timeout | 0 | | | |auk-0098.smt2 | 30.067s | 168.0MiB| timeout | 0 | | |