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

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |auk-0041.smt2 | 0.039s | 20.168MiB| unsat | 0 | | | |auk-0161.smt2 | 0.043s | 19.448MiB| sat | 0 | | | |auk-0178.smt2 | 0.043s | 19.604MiB| sat | 0 | | | |auk-0054.smt2 | 0.045s | 18.968MiB| unsat | 0 | | | |auk-0042.smt2 | 0.046s | 20.036MiB| sat | 0 | | | |auk-0066.smt2 | 0.047s | 19.624MiB| sat | 0 | | | |auk-0069.smt2 | 0.051s | 20.088MiB| unsat | 0 | | | |auk-0046.smt2 | 0.052s | 19.708MiB| unsat | 0 | | | |auk-0160.smt2 | 0.055s | 19.996MiB| unsat | 0 | | | |auk-0179.smt2 | 0.055s | 20.08MiB| unsat | 0 | | | |auk-0060.smt2 | 0.056s | 19.96MiB| unsat | 0 | | | |auk-0138.smt2 | 0.056s | 20.252MiB| unsat | 0 | | | |auk-0170.smt2 | 0.059s | 20.484MiB| unsat | 0 | | | |auk-0012.smt2 | 0.062s | 20.508MiB| unsat | 0 | | | |auk-0168.smt2 | 0.062s | 20.236MiB| sat | 0 | | | |auk-0038.smt2 | 0.062s | 19.096MiB| unsat | 0 | | | |auk-0057.smt2 | 0.064s | 19.904MiB| unsat | 0 | | | |auk-0166.smt2 | 0.065s | 21.12MiB| sat | 0 | | | |auk-0067.smt2 | 0.066s | 20.268MiB| sat | 0 | | | |auk-0036.smt2 | 0.069s | 20.636MiB| sat | 0 | | | |auk-0031.smt2 | 0.070s | 20.252MiB| unsat | 0 | | | |auk-0059.smt2 | 0.071s | 22.844MiB| unsat | 0 | | | |auk-0068.smt2 | 0.075s | 19.664MiB| unsat | 0 | | | |auk-0051.smt2 | 0.085s | 21.024MiB| unsat | 0 | | | |auk-0136.smt2 | 0.086s | 20.772MiB| sat | 0 | | | |auk-0050.smt2 | 0.089s | 20.204MiB| unsat | 0 | | | |auk-0040.smt2 | 0.089s | 20.236MiB| unsat | 0 | | | |auk-0009.smt2 | 0.090s | 20.384MiB| sat | 0 | | | |auk-0028.smt2 | 0.091s | 22.34MiB| unsat | 0 | | | |auk-0097.smt2 | 0.094s | 22.988MiB| sat | 0 | | | |auk-0065.smt2 | 0.095s | 20.416MiB| unsat | 0 | | | |auk-0034.smt2 | 0.095s | 20.688MiB| unsat | 0 | | | |auk-0064.smt2 | 0.095s | 21.108MiB| sat | 0 | | | |auk-0044.smt2 | 0.097s | 20.688MiB| unsat | 0 | | | |auk-0159.smt2 | 0.098s | 20.348MiB| unsat | 0 | | | |auk-0063.smt2 | 0.100s | 20.676MiB| unsat | 0 | | | |auk-0035.smt2 | 0.104s | 20.228MiB| unsat | 0 | | | |auk-0032.smt2 | 0.105s | 20.416MiB| unsat | 0 | | | |auk-0055.smt2 | 0.105s | 24.812MiB| sat | 0 | | | |auk-0139.smt2 | 0.109s | 21.536MiB| unsat | 0 | | | |auk-0053.smt2 | 0.110s | 20.752MiB| sat | 0 | | | |auk-0061.smt2 | 0.113s | 20.768MiB| unsat | 0 | | | |auk-0039.smt2 | 0.118s | 20.692MiB| unsat | 0 | | | |auk-0093.smt2 | 0.126s | 24.62MiB| sat | 0 | | | |auk-0043.smt2 | 0.130s | 24.276MiB| unsat | 0 | | | |auk-0174.smt2 | 0.132s | 25.72MiB| sat | 0 | | | |auk-0037.smt2 | 0.139s | 25.484MiB| unsat | 0 | | | |auk-0104.smt2 | 0.141s | 24.136MiB| sat | 0 | | | |auk-0052.smt2 | 0.142s | 24.728MiB| unsat | 0 | | | |auk-0024.smt2 | 0.142s | 25.528MiB| unsat | 0 | | | |auk-0058.smt2 | 0.142s | 24.624MiB| sat | 0 | | | |auk-0019.smt2 | 0.147s | 26.156MiB| unsat | 0 | | | |auk-0110.smt2 | 0.148s | 24.7MiB| sat | 0 | | | |auk-0154.smt2 | 0.149s | 26.308MiB| sat | 0 | | | |auk-0165.smt2 | 0.149s | 25.256MiB| sat | 0 | | | |auk-0125.smt2 | 0.150s | 26.736MiB| sat | 0 | | | |auk-0047.smt2 | 0.152s | 24.892MiB| unsat | 0 | | | |auk-0033.smt2 | 0.152s | 25.968MiB| sat | 0 | | | |auk-0143.smt2 | 0.155s | 20.772MiB| unsat | 0 | | | |auk-0157.smt2 | 0.158s | 24.924MiB| sat | 0 | | | |auk-0020.smt2 | 0.162s | 25.536MiB| unsat | 0 | | | |auk-0021.smt2 | 0.164s | 23.328MiB| unsat | 0 | | | |auk-0129.smt2 | 0.164s | 25.012MiB| sat | 0 | | | |auk-0176.smt2 | 0.169s | 26.424MiB| sat | 0 | | | |auk-0003.smt2 | 0.172s | 27.86MiB| unsat | 0 | | | |auk-0163.smt2 | 0.174s | 25.7MiB| sat | 0 | | | |auk-0062.smt2 | 0.178s | 24.676MiB| unsat | 0 | | | |auk-0048.smt2 | 0.179s | 25.168MiB| unsat | 0 | | | |auk-0173.smt2 | 0.179s | 25.752MiB| sat | 0 | | | |auk-0045.smt2 | 0.180s | 25.148MiB| unsat | 0 | | | |auk-0172.smt2 | 0.181s | 25.784MiB| sat | 0 | | | |auk-0153.smt2 | 0.181s | 26.376MiB| sat | 0 | | | |auk-0030.smt2 | 0.181s | 24.92MiB| unsat | 0 | | | |auk-0162.smt2 | 0.181s | 24.444MiB| sat | 0 | | | |auk-0167.smt2 | 0.183s | 25.28MiB| sat | 0 | | | |auk-0175.smt2 | 0.184s | 26.2MiB| sat | 0 | | | |auk-0106.smt2 | 0.186s | 26.728MiB| sat | 0 | | | |auk-0108.smt2 | 0.187s | 28.352MiB| sat | 0 | | | |auk-0127.smt2 | 0.189s | 26.6MiB| sat | 0 | | | |auk-0100.smt2 | 0.189s | 24.488MiB| sat | 0 | | | |auk-0026.smt2 | 0.191s | 24.852MiB| unsat | 0 | | | |auk-0105.smt2 | 0.194s | 27.136MiB| sat | 0 | | | |auk-0158.smt2 | 0.195s | 25.052MiB| sat | 0 | | | |auk-0164.smt2 | 0.195s | 25.732MiB| sat | 0 | | | |auk-0118.smt2 | 0.197s | 27.012MiB| sat | 0 | | | |auk-0124.smt2 | 0.198s | 26.796MiB| sat | 0 | | | |auk-0121.smt2 | 0.199s | 26.532MiB| sat | 0 | | | |auk-0169.smt2 | 0.199s | 25.972MiB| unsat | 0 | | | |auk-0177.smt2 | 0.201s | 26.272MiB| sat | 0 | | | |auk-0014.smt2 | 0.205s | 27.828MiB| unsat | 0 | | | |auk-0107.smt2 | 0.205s | 26.648MiB| sat | 0 | | | |auk-0155.smt2 | 0.207s | 25.144MiB| sat | 0 | | | |auk-0171.smt2 | 0.210s | 25.74MiB| sat | 0 | | | |auk-0156.smt2 | 0.213s | 25.308MiB| sat | 0 | | | |auk-0008.smt2 | 0.215s | 27.976MiB| unsat | 0 | | | |auk-0150.smt2 | 0.217s | 25.672MiB| unsat | 0 | | | |auk-0112.smt2 | 0.220s | 27.192MiB| sat | 0 | | | |auk-0152.smt2 | 0.220s | 25.16MiB| sat | 0 | | | |auk-0029.smt2 | 0.224s | 25.768MiB| unsat | 0 | | | |auk-0111.smt2 | 0.239s | 28.508MiB| sat | 0 | | | |auk-0102.smt2 | 0.240s | 27.1MiB| sat | 0 | | | |auk-0013.smt2 | 0.241s | 27.932MiB| unsat | 0 | | | |auk-0016.smt2 | 0.243s | 25.524MiB| unsat | 0 | | | |auk-0114.smt2 | 0.246s | 25.74MiB| sat | 0 | | | |auk-0126.smt2 | 0.257s | 28.576MiB| sat | 0 | | | |auk-0180.smt2 | 0.267s | 27.848MiB| unsat | 0 | | | |auk-0018.smt2 | 0.274s | 27.584MiB| unsat | 0 | | | |auk-0023.smt2 | 0.279s | 27.78MiB| unsat | 0 | | | |auk-0070.smt2 | 0.284s | 31.408MiB| sat | 0 | | | |auk-0117.smt2 | 0.294s | 30.172MiB| sat | 0 | | | |auk-0103.smt2 | 0.295s | 27.544MiB| sat | 0 | | | |auk-0115.smt2 | 0.310s | 35.244MiB| sat | 0 | | | |auk-0120.smt2 | 0.320s | 30.784MiB| sat | 0 | | | |auk-0113.smt2 | 0.325s | 29.932MiB| sat | 0 | | | |auk-0049.smt2 | 0.326s | 21.332MiB| unsat | 0 | | | |auk-0134.smt2 | 0.356s | 31.832MiB| sat | 0 | | | |auk-0022.smt2 | 0.383s | 28.436MiB| sat | 0 | | | |auk-0123.smt2 | 0.385s | 31.256MiB| sat | 0 | | | |auk-0116.smt2 | 0.399s | 31.228MiB| sat | 0 | | | |auk-0130.smt2 | 0.448s | 33.492MiB| sat | 0 | | | |auk-0002.smt2 | 0.459s | 33.504MiB| unsat | 0 | | | |auk-0010.smt2 | 0.466s | 32.924MiB| unsat | 0 | | | |auk-0004.smt2 | 0.470s | 33.768MiB| unsat | 0 | | | |auk-0119.smt2 | 0.474s | 34.008MiB| sat | 0 | | | |auk-0135.smt2 | 0.476s | 28.144MiB| unsat | 0 | | | |auk-0006.smt2 | 0.525s | 33.74MiB| unsat | 0 | | | |auk-0109.smt2 | 0.544s | 44.436MiB| sat | 0 | | | |auk-0056.smt2 | 0.620s | 27.372MiB| sat | 0 | | | |auk-0128.smt2 | 0.629s | 32.804MiB| sat | 0 | | | |auk-0072.smt2 | 0.766s | 32.236MiB| sat | 0 | | | |auk-0078.smt2 | 0.769s | 32.272MiB| sat | 0 | | | |auk-0025.smt2 | 0.779s | 30.948MiB| unsat | 0 | | | |auk-0133.smt2 | 0.823s | 42.284MiB| sat | 0 | | | |auk-0096.smt2 | 0.840s | 28.5MiB| sat | 0 | | | |auk-0122.smt2 | 0.999s | 31.128MiB| sat | 0 | | | |auk-0080.smt2 | 1.032s | 34.712MiB| sat | 0 | | | |auk-0132.smt2 | 1.064s | 56.192MiB| sat | 0 | | | |auk-0151.smt2 | 1.115s | 22.992MiB| unsat | 0 | | | |auk-0071.smt2 | 1.151s | 47.248MiB| sat | 0 | | | |auk-0076.smt2 | 1.263s | 47.3MiB| sat | 0 | | | |auk-0075.smt2 | 1.280s | 47.208MiB| sat | 0 | | | |auk-0077.smt2 | 1.297s | 42.024MiB| sat | 0 | | | |auk-0073.smt2 | 1.345s | 47.036MiB| sat | 0 | | | |auk-0027.smt2 | 1.553s | 29.0MiB| unsat | 0 | | | |auk-0184.smt2 | 1.706s | 36.508MiB| unsat | 0 | | | |auk-0017.smt2 | 1.710s | 31.104MiB| unsat | 0 | | | |auk-0131.smt2 | 1.714s | 91.72MiB| sat | 0 | | | |auk-0094.smt2 | 1.881s | 32.308MiB| sat | 0 | | | |auk-0095.smt2 | 2.476s | 37.892MiB| unsat | 0 | | | |auk-0146.smt2 | 2.681s | 29.884MiB| unsat | 0 | | | |auk-0144.smt2 | 2.766s | 34.108MiB| unsat | 0 | | | |auk-0083.smt2 | 2.911s | 99.0MiB| sat | 0 | | | |auk-0082.smt2 | 2.936s | 99.0MiB| sat | 0 | | | |auk-0079.smt2 | 3.202s | 45.508MiB| sat | 0 | | | |auk-0145.smt2 | 3.862s | 31.732MiB| unsat | 0 | | | |auk-0084.smt2 | 4.086s | 53.976MiB| unsat | 0 | | | |auk-0148.smt2 | 4.442s | 38.088MiB| unsat | 0 | | | |auk-0182.smt2 | 4.757s | 63.812MiB| unsat | 0 | | | |auk-0186.smt2 | 5.700s | 66.492MiB| unsat | 0 | | | |auk-0183.smt2 | 6.946s | 70.644MiB| unsat | 0 | | | |auk-0142.smt2 | 7.821s | 36.396MiB| unsat | 0 | | | |auk-0090.smt2 | 8.435s | 59.16MiB| unsat | 0 | | | |auk-0137.smt2 | 9.089s | 30.54MiB| sat | 0 | | | |auk-0087.smt2 | 12.095s | 65.72MiB| unsat | 0 | | | |auk-0141.smt2 | 12.339s | 49.136MiB| unsat | 0 | | | |auk-0181.smt2 | 12.431s | 72.024MiB| unsat | 0 | | | |auk-0091.smt2 | 27.148s | 45.236MiB| sat | 0 | | | |auk-0074.smt2 | 30.011s | 32.908MiB| timeout | 0 | | | |auk-0081.smt2 | 30.013s | 35.376MiB| timeout | 0 | | | |auk-0147.smt2 | 30.013s | 38.904MiB| timeout | 0 | | | |auk-0187.smt2 | 30.014s | 58.98MiB| timeout | 0 | | | |auk-0007.smt2 | 30.014s | 57.148MiB| timeout | 0 | | | |auk-0188.smt2 | 30.015s | 55.492MiB| timeout | 0 | | | |auk-0101.smt2 | 30.016s | 36.528MiB| timeout | 0 | | | |auk-0088.smt2 | 30.017s | 94.616MiB| timeout | 0 | | | |auk-0001.smt2 | 30.018s | 26.692MiB| timeout | 0 | | | |auk-0189.smt2 | 30.018s | 54.852MiB| timeout | 0 | | | |auk-0149.smt2 | 30.019s | 29.32MiB| timeout | 0 | | | |auk-0185.smt2 | 30.019s | 51.268MiB| timeout | 0 | | | |auk-0005.smt2 | 30.021s | 46.3MiB| timeout | 0 | | | |auk-0140.smt2 | 30.021s | 50.764MiB| timeout | 0 | | | |auk-0086.smt2 | 30.021s | 95.136MiB| timeout | 0 | | | |auk-0092.smt2 | 30.023s | 102.0MiB| timeout | 0 | | | |auk-0085.smt2 | 30.025s | 97.148MiB| timeout | 0 | | | |auk-0015.smt2 | 30.027s | 126.0MiB| timeout | 0 | | | |auk-0099.smt2 | 30.028s | 159.0MiB| timeout | 0 | | | |auk-0089.smt2 | 30.030s | 74.364MiB| timeout | 0 | | | |auk-0098.smt2 | 30.031s | 174.0MiB| timeout | 0 | | | |auk-0011.smt2 | 30.035s | 47.316MiB| timeout | 0 | | |