# . * SAT 87 * UNSAT 78 * TIMEOUT 24 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: certora2-poly-seed-0
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: ed84b14e6c7dfaf6efd1b740119ecb1631e8bdfb
Z3 branch: arie
Z3 options: "-T:30 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.031s | 19.42MiB| sat | 0 | | | |auk-0069.smt2 | 0.034s | 20.2MiB| unsat | 0 | | | |auk-0046.smt2 | 0.036s | 19.708MiB| unsat | 0 | | | |auk-0066.smt2 | 0.037s | 19.712MiB| sat | 0 | | | |auk-0178.smt2 | 0.045s | 19.66MiB| sat | 0 | | | |auk-0166.smt2 | 0.047s | 20.728MiB| sat | 0 | | | |auk-0038.smt2 | 0.048s | 18.996MiB| unsat | 0 | | | |auk-0060.smt2 | 0.050s | 19.916MiB| unsat | 0 | | | |auk-0054.smt2 | 0.052s | 18.972MiB| unsat | 0 | | | |auk-0061.smt2 | 0.052s | 20.764MiB| unsat | 0 | | | |auk-0168.smt2 | 0.056s | 19.984MiB| sat | 0 | | | |auk-0179.smt2 | 0.060s | 20.0MiB| unsat | 0 | | | |auk-0138.smt2 | 0.061s | 20.26MiB| unsat | 0 | | | |auk-0012.smt2 | 0.065s | 20.36MiB| unsat | 0 | | | |auk-0042.smt2 | 0.065s | 20.04MiB| sat | 0 | | | |auk-0160.smt2 | 0.066s | 20.128MiB| unsat | 0 | | | |auk-0170.smt2 | 0.070s | 20.592MiB| unsat | 0 | | | |auk-0050.smt2 | 0.072s | 20.256MiB| unsat | 0 | | | |auk-0067.smt2 | 0.073s | 20.248MiB| sat | 0 | | | |auk-0039.smt2 | 0.076s | 20.588MiB| unsat | 0 | | | |auk-0035.smt2 | 0.078s | 20.196MiB| unsat | 0 | | | |auk-0057.smt2 | 0.084s | 19.74MiB| unsat | 0 | | | |auk-0068.smt2 | 0.084s | 19.488MiB| unsat | 0 | | | |auk-0036.smt2 | 0.085s | 20.892MiB| sat | 0 | | | |auk-0032.smt2 | 0.094s | 20.364MiB| unsat | 0 | | | |auk-0009.smt2 | 0.095s | 20.308MiB| sat | 0 | | | |auk-0028.smt2 | 0.096s | 22.46MiB| unsat | 0 | | | |auk-0044.smt2 | 0.097s | 20.732MiB| unsat | 0 | | | |auk-0059.smt2 | 0.097s | 22.784MiB| unsat | 0 | | | |auk-0051.smt2 | 0.099s | 20.956MiB| unsat | 0 | | | |auk-0040.smt2 | 0.101s | 20.196MiB| unsat | 0 | | | |auk-0031.smt2 | 0.103s | 20.28MiB| unsat | 0 | | | |auk-0034.smt2 | 0.104s | 20.672MiB| unsat | 0 | | | |auk-0041.smt2 | 0.107s | 20.212MiB| unsat | 0 | | | |auk-0065.smt2 | 0.110s | 20.568MiB| unsat | 0 | | | |auk-0159.smt2 | 0.112s | 20.308MiB| unsat | 0 | | | |auk-0053.smt2 | 0.116s | 21.124MiB| sat | 0 | | | |auk-0163.smt2 | 0.124s | 25.712MiB| sat | 0 | | | |auk-0174.smt2 | 0.125s | 25.72MiB| sat | 0 | | | |auk-0063.smt2 | 0.126s | 20.864MiB| unsat | 0 | | | |auk-0172.smt2 | 0.131s | 25.808MiB| sat | 0 | | | |auk-0062.smt2 | 0.132s | 24.744MiB| unsat | 0 | | | |auk-0097.smt2 | 0.136s | 22.86MiB| sat | 0 | | | |auk-0110.smt2 | 0.136s | 24.796MiB| sat | 0 | | | |auk-0136.smt2 | 0.138s | 20.696MiB| sat | 0 | | | |auk-0155.smt2 | 0.139s | 25.14MiB| sat | 0 | | | |auk-0055.smt2 | 0.140s | 24.624MiB| sat | 0 | | | |auk-0043.smt2 | 0.141s | 24.204MiB| unsat | 0 | | | |auk-0064.smt2 | 0.143s | 20.744MiB| sat | 0 | | | |auk-0047.smt2 | 0.145s | 25.084MiB| unsat | 0 | | | |auk-0052.smt2 | 0.146s | 24.672MiB| unsat | 0 | | | |auk-0024.smt2 | 0.148s | 25.544MiB| unsat | 0 | | | |auk-0030.smt2 | 0.149s | 24.896MiB| unsat | 0 | | | |auk-0049.smt2 | 0.154s | 21.064MiB| unsat | 0 | | | |auk-0104.smt2 | 0.156s | 24.216MiB| sat | 0 | | | |auk-0020.smt2 | 0.158s | 25.42MiB| unsat | 0 | | | |auk-0129.smt2 | 0.158s | 25.008MiB| sat | 0 | | | |auk-0058.smt2 | 0.161s | 24.704MiB| sat | 0 | | | |auk-0108.smt2 | 0.164s | 28.296MiB| sat | 0 | | | |auk-0157.smt2 | 0.164s | 24.84MiB| sat | 0 | | | |auk-0003.smt2 | 0.164s | 28.076MiB| unsat | 0 | | | |auk-0158.smt2 | 0.165s | 25.144MiB| sat | 0 | | | |auk-0033.smt2 | 0.166s | 26.052MiB| sat | 0 | | | |auk-0173.smt2 | 0.172s | 25.772MiB| sat | 0 | | | |auk-0100.smt2 | 0.172s | 24.428MiB| sat | 0 | | | |auk-0107.smt2 | 0.174s | 26.54MiB| sat | 0 | | | |auk-0162.smt2 | 0.175s | 24.48MiB| sat | 0 | | | |auk-0045.smt2 | 0.182s | 25.28MiB| unsat | 0 | | | |auk-0153.smt2 | 0.186s | 26.38MiB| sat | 0 | | | |auk-0176.smt2 | 0.186s | 26.432MiB| sat | 0 | | | |auk-0026.smt2 | 0.188s | 24.788MiB| unsat | 0 | | | |auk-0164.smt2 | 0.189s | 25.704MiB| sat | 0 | | | |auk-0167.smt2 | 0.190s | 25.332MiB| sat | 0 | | | |auk-0124.smt2 | 0.192s | 26.98MiB| sat | 0 | | | |auk-0029.smt2 | 0.193s | 25.872MiB| unsat | 0 | | | |auk-0152.smt2 | 0.195s | 24.948MiB| sat | 0 | | | |auk-0016.smt2 | 0.197s | 25.064MiB| unsat | 0 | | | |auk-0037.smt2 | 0.199s | 25.728MiB| unsat | 0 | | | |auk-0150.smt2 | 0.200s | 25.792MiB| unsat | 0 | | | |auk-0014.smt2 | 0.202s | 27.976MiB| unsat | 0 | | | |auk-0156.smt2 | 0.202s | 25.24MiB| sat | 0 | | | |auk-0177.smt2 | 0.202s | 26.44MiB| sat | 0 | | | |auk-0127.smt2 | 0.205s | 26.396MiB| sat | 0 | | | |auk-0171.smt2 | 0.209s | 25.616MiB| sat | 0 | | | |auk-0175.smt2 | 0.215s | 26.416MiB| sat | 0 | | | |auk-0165.smt2 | 0.218s | 25.308MiB| sat | 0 | | | |auk-0105.smt2 | 0.220s | 27.068MiB| sat | 0 | | | |auk-0102.smt2 | 0.221s | 26.976MiB| sat | 0 | | | |auk-0169.smt2 | 0.221s | 25.916MiB| unsat | 0 | | | |auk-0126.smt2 | 0.221s | 28.464MiB| sat | 0 | | | |auk-0008.smt2 | 0.223s | 27.912MiB| unsat | 0 | | | |auk-0112.smt2 | 0.224s | 27.248MiB| sat | 0 | | | |auk-0118.smt2 | 0.224s | 26.98MiB| sat | 0 | | | |auk-0125.smt2 | 0.225s | 26.936MiB| sat | 0 | | | |auk-0023.smt2 | 0.228s | 27.408MiB| unsat | 0 | | | |auk-0021.smt2 | 0.228s | 23.424MiB| unsat | 0 | | | |auk-0114.smt2 | 0.229s | 25.844MiB| sat | 0 | | | |auk-0121.smt2 | 0.238s | 26.64MiB| sat | 0 | | | |auk-0106.smt2 | 0.244s | 26.86MiB| sat | 0 | | | |auk-0013.smt2 | 0.247s | 28.008MiB| unsat | 0 | | | |auk-0139.smt2 | 0.252s | 21.72MiB| unsat | 0 | | | |auk-0048.smt2 | 0.253s | 25.784MiB| unsat | 0 | | | |auk-0154.smt2 | 0.254s | 26.22MiB| sat | 0 | | | |auk-0117.smt2 | 0.260s | 30.6MiB| sat | 0 | | | |auk-0111.smt2 | 0.262s | 28.672MiB| sat | 0 | | | |auk-0180.smt2 | 0.279s | 27.8MiB| unsat | 0 | | | |auk-0018.smt2 | 0.282s | 27.156MiB| unsat | 0 | | | |auk-0143.smt2 | 0.285s | 21.22MiB| unsat | 0 | | | |auk-0019.smt2 | 0.299s | 27.22MiB| unsat | 0 | | | |auk-0115.smt2 | 0.330s | 34.144MiB| sat | 0 | | | |auk-0103.smt2 | 0.343s | 27.528MiB| sat | 0 | | | |auk-0002.smt2 | 0.358s | 33.86MiB| unsat | 0 | | | |auk-0128.smt2 | 0.382s | 31.948MiB| sat | 0 | | | |auk-0116.smt2 | 0.385s | 31.144MiB| sat | 0 | | | |auk-0123.smt2 | 0.392s | 31.452MiB| sat | 0 | | | |auk-0010.smt2 | 0.408s | 33.208MiB| unsat | 0 | | | |auk-0017.smt2 | 0.417s | 29.836MiB| unsat | 0 | | | |auk-0113.smt2 | 0.421s | 31.064MiB| sat | 0 | | | |auk-0120.smt2 | 0.451s | 31.368MiB| sat | 0 | | | |auk-0135.smt2 | 0.469s | 28.196MiB| unsat | 0 | | | |auk-0130.smt2 | 0.497s | 33.664MiB| sat | 0 | | | |auk-0093.smt2 | 0.502s | 25.056MiB| sat | 0 | | | |auk-0119.smt2 | 0.539s | 35.376MiB| sat | 0 | | | |auk-0109.smt2 | 0.546s | 44.432MiB| sat | 0 | | | |auk-0122.smt2 | 0.562s | 31.32MiB| sat | 0 | | | |auk-0094.smt2 | 0.650s | 31.008MiB| sat | 0 | | | |auk-0078.smt2 | 0.658s | 32.14MiB| sat | 0 | | | |auk-0025.smt2 | 0.713s | 30.692MiB| unsat | 0 | | | |auk-0072.smt2 | 0.733s | 32.064MiB| sat | 0 | | | |auk-0080.smt2 | 0.747s | 34.544MiB| sat | 0 | | | |auk-0096.smt2 | 0.753s | 29.012MiB| sat | 0 | | | |auk-0056.smt2 | 0.803s | 27.16MiB| sat | 0 | | | |auk-0133.smt2 | 0.818s | 42.076MiB| sat | 0 | | | |auk-0004.smt2 | 0.908s | 35.58MiB| unsat | 0 | | | |auk-0022.smt2 | 0.995s | 28.52MiB| sat | 0 | | | |auk-0151.smt2 | 1.003s | 23.084MiB| unsat | 0 | | | |auk-0091.smt2 | 1.016s | 42.688MiB| sat | 0 | | | |auk-0132.smt2 | 1.131s | 56.188MiB| sat | 0 | | | |auk-0071.smt2 | 1.136s | 47.34MiB| sat | 0 | | | |auk-0077.smt2 | 1.154s | 41.56MiB| sat | 0 | | | |auk-0073.smt2 | 1.190s | 47.144MiB| sat | 0 | | | |auk-0149.smt2 | 1.236s | 28.752MiB| unsat | 0 | | | |auk-0076.smt2 | 1.273s | 47.428MiB| sat | 0 | | | |auk-0146.smt2 | 1.345s | 29.084MiB| unsat | 0 | | | |auk-0006.smt2 | 1.420s | 37.748MiB| unsat | 0 | | | |auk-0079.smt2 | 1.456s | 45.532MiB| sat | 0 | | | |auk-0101.smt2 | 1.498s | 35.86MiB| unsat | 0 | | | |auk-0075.smt2 | 1.499s | 47.172MiB| sat | 0 | | | |auk-0131.smt2 | 1.524s | 90.288MiB| sat | 0 | | | |auk-0145.smt2 | 1.545s | 30.864MiB| unsat | 0 | | | |auk-0184.smt2 | 1.599s | 37.5MiB| unsat | 0 | | | |auk-0015.smt2 | 1.609s | 36.568MiB| unsat | 0 | | | |auk-0083.smt2 | 2.841s | 99.0MiB| sat | 0 | | | |auk-0082.smt2 | 2.879s | 99.0MiB| sat | 0 | | | |auk-0144.smt2 | 3.101s | 35.212MiB| unsat | 0 | | | |auk-0095.smt2 | 3.412s | 38.696MiB| unsat | 0 | | | |auk-0134.smt2 | 3.876s | 33.288MiB| sat | 0 | | | |auk-0148.smt2 | 3.916s | 35.344MiB| unsat | 0 | | | |auk-0142.smt2 | 4.701s | 36.344MiB| unsat | 0 | | | |auk-0070.smt2 | 6.701s | 33.228MiB| sat | 0 | | | |auk-0183.smt2 | 7.580s | 71.576MiB| unsat | 0 | | | |auk-0182.smt2 | 9.250s | 70.144MiB| unsat | 0 | | | |auk-0140.smt2 | 9.517s | 41.712MiB| unsat | 0 | | | |auk-0141.smt2 | 11.485s | 47.796MiB| unsat | 0 | | | |auk-0087.smt2 | 19.111s | 70.596MiB| unsat | 0 | | | |auk-0188.smt2 | 30.012s | 55.064MiB| timeout | 0 | | | |auk-0074.smt2 | 30.013s | 33.524MiB| timeout | 0 | | | |auk-0147.smt2 | 30.014s | 38.768MiB| timeout | 0 | | | |auk-0189.smt2 | 30.014s | 60.108MiB| timeout | 0 | | | |auk-0007.smt2 | 30.016s | 52.436MiB| timeout | 0 | | | |auk-0085.smt2 | 30.018s | 107.0MiB| timeout | 0 | | | |auk-0089.smt2 | 30.018s | 70.512MiB| timeout | 0 | | | |auk-0186.smt2 | 30.019s | 77.504MiB| timeout | 0 | | | |auk-0092.smt2 | 30.020s | 88.268MiB| timeout | 0 | | | |auk-0181.smt2 | 30.024s | 77.196MiB| timeout | 0 | | | |auk-0090.smt2 | 30.024s | 62.572MiB| timeout | 0 | | | |auk-0187.smt2 | 30.025s | 57.212MiB| timeout | 0 | | | |auk-0099.smt2 | 30.025s | 160.0MiB| timeout | 0 | | | |auk-0081.smt2 | 30.026s | 35.736MiB| timeout | 0 | | | |auk-0185.smt2 | 30.028s | 50.86MiB| timeout | 0 | | | |auk-0001.smt2 | 30.028s | 31.496MiB| timeout | 0 | | | |auk-0088.smt2 | 30.029s | 82.388MiB| timeout | 0 | | | |auk-0005.smt2 | 30.030s | 110.0MiB| timeout | 0 | | | |auk-0084.smt2 | 30.031s | 67.76MiB| timeout | 0 | | | |auk-0011.smt2 | 30.032s | 52.816MiB| timeout | 0 | | | |auk-0086.smt2 | 30.032s | 105.0MiB| timeout | 0 | | | |auk-0098.smt2 | 30.034s | 173.0MiB| timeout | 0 | | | |auk-0137.smt2 | 30.039s | 30.808MiB| timeout | 0 | | | |auk-0027.smt2 | 30.046s | 37.556MiB| timeout | 0 | | |