# . * SAT 86 * UNSAT 70 * TIMEOUT 33 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: certora2-base
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: ed84b14e6c7dfaf6efd1b740119ecb1631e8bdfb
Z3 branch: arie
Z3 options: "-T:30 tactic.default_tactic=smt"
Z3 inputs: inputs/certora2
Z3 commit message: fixing coi bug

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |auk-0067.smt2 | 0.054s | 20.256MiB| sat | 0 | | | |auk-0038.smt2 | 0.055s | 19.592MiB| unsat | 0 | | | |auk-0161.smt2 | 0.055s | 19.668MiB| sat | 0 | | | |auk-0031.smt2 | 0.057s | 20.252MiB| unsat | 0 | | | |auk-0179.smt2 | 0.060s | 20.084MiB| unsat | 0 | | | |auk-0069.smt2 | 0.065s | 20.26MiB| unsat | 0 | | | |auk-0166.smt2 | 0.066s | 21.16MiB| sat | 0 | | | |auk-0041.smt2 | 0.066s | 20.52MiB| unsat | 0 | | | |auk-0160.smt2 | 0.068s | 20.252MiB| unsat | 0 | | | |auk-0170.smt2 | 0.068s | 20.56MiB| unsat | 0 | | | |auk-0060.smt2 | 0.069s | 20.06MiB| unsat | 0 | | | |auk-0178.smt2 | 0.070s | 20.076MiB| sat | 0 | | | |auk-0068.smt2 | 0.072s | 19.48MiB| unsat | 0 | | | |auk-0061.smt2 | 0.073s | 20.716MiB| unsat | 0 | | | |auk-0042.smt2 | 0.074s | 20.256MiB| sat | 0 | | | |auk-0066.smt2 | 0.075s | 19.824MiB| sat | 0 | | | |auk-0050.smt2 | 0.075s | 20.416MiB| unsat | 0 | | | |auk-0046.smt2 | 0.075s | 20.104MiB| unsat | 0 | | | |auk-0138.smt2 | 0.083s | 20.3MiB| unsat | 0 | | | |auk-0159.smt2 | 0.085s | 20.508MiB| unsat | 0 | | | |auk-0054.smt2 | 0.087s | 19.496MiB| unsat | 0 | | | |auk-0036.smt2 | 0.087s | 21.216MiB| sat | 0 | | | |auk-0168.smt2 | 0.087s | 20.328MiB| sat | 0 | | | |auk-0035.smt2 | 0.092s | 23.388MiB| unsat | 0 | | | |auk-0057.smt2 | 0.093s | 20.224MiB| unsat | 0 | | | |auk-0059.smt2 | 0.093s | 25.088MiB| unsat | 0 | | | |auk-0043.smt2 | 0.099s | 26.328MiB| unsat | 0 | | | |auk-0064.smt2 | 0.100s | 20.892MiB| sat | 0 | | | |auk-0065.smt2 | 0.106s | 24.572MiB| unsat | 0 | | | |auk-0012.smt2 | 0.107s | 21.104MiB| unsat | 0 | | | |auk-0028.smt2 | 0.107s | 24.14MiB| unsat | 0 | | | |auk-0034.smt2 | 0.107s | 25.052MiB| unsat | 0 | | | |auk-0097.smt2 | 0.111s | 25.652MiB| sat | 0 | | | |auk-0051.smt2 | 0.139s | 21.42MiB| unsat | 0 | | | |auk-0040.smt2 | 0.139s | 20.536MiB| unsat | 0 | | | |auk-0032.smt2 | 0.145s | 26.248MiB| unsat | 0 | | | |auk-0093.smt2 | 0.150s | 27.18MiB| sat | 0 | | | |auk-0020.smt2 | 0.152s | 27.008MiB| unsat | 0 | | | |auk-0024.smt2 | 0.156s | 26.932MiB| unsat | 0 | | | |auk-0110.smt2 | 0.159s | 28.232MiB| sat | 0 | | | |auk-0052.smt2 | 0.160s | 27.072MiB| unsat | 0 | | | |auk-0172.smt2 | 0.163s | 29.76MiB| sat | 0 | | | |auk-0019.smt2 | 0.163s | 27.612MiB| unsat | 0 | | | |auk-0058.smt2 | 0.168s | 27.364MiB| sat | 0 | | | |auk-0047.smt2 | 0.171s | 27.376MiB| unsat | 0 | | | |auk-0045.smt2 | 0.174s | 27.476MiB| unsat | 0 | | | |auk-0044.smt2 | 0.175s | 26.22MiB| unsat | 0 | | | |auk-0125.smt2 | 0.178s | 31.924MiB| sat | 0 | | | |auk-0163.smt2 | 0.178s | 29.888MiB| sat | 0 | | | |auk-0016.smt2 | 0.180s | 26.772MiB| unsat | 0 | | | |auk-0129.smt2 | 0.183s | 28.576MiB| sat | 0 | | | |auk-0157.smt2 | 0.187s | 30.664MiB| sat | 0 | | | |auk-0100.smt2 | 0.190s | 28.28MiB| sat | 0 | | | |auk-0063.smt2 | 0.192s | 26.092MiB| unsat | 0 | | | |auk-0164.smt2 | 0.194s | 29.792MiB| sat | 0 | | | |auk-0021.smt2 | 0.198s | 26.096MiB| unsat | 0 | | | |auk-0158.smt2 | 0.202s | 28.184MiB| sat | 0 | | | |auk-0033.smt2 | 0.206s | 28.764MiB| sat | 0 | | | |auk-0114.smt2 | 0.206s | 30.108MiB| sat | 0 | | | |auk-0165.smt2 | 0.210s | 31.064MiB| sat | 0 | | | |auk-0055.smt2 | 0.212s | 27.712MiB| sat | 0 | | | |auk-0169.smt2 | 0.212s | 30.664MiB| unsat | 0 | | | |auk-0162.smt2 | 0.219s | 28.148MiB| sat | 0 | | | |auk-0155.smt2 | 0.220s | 31.508MiB| sat | 0 | | | |auk-0174.smt2 | 0.220s | 30.916MiB| sat | 0 | | | |auk-0026.smt2 | 0.220s | 27.276MiB| unsat | 0 | | | |auk-0017.smt2 | 0.222s | 30.1MiB| unsat | 0 | | | |auk-0037.smt2 | 0.224s | 28.144MiB| unsat | 0 | | | |auk-0029.smt2 | 0.225s | 28.232MiB| unsat | 0 | | | |auk-0048.smt2 | 0.226s | 28.212MiB| unsat | 0 | | | |auk-0039.smt2 | 0.227s | 26.872MiB| unsat | 0 | | | |auk-0018.smt2 | 0.237s | 27.384MiB| unsat | 0 | | | |auk-0107.smt2 | 0.238s | 31.624MiB| sat | 0 | | | |auk-0152.smt2 | 0.241s | 28.624MiB| sat | 0 | | | |auk-0156.smt2 | 0.241s | 31.508MiB| sat | 0 | | | |auk-0104.smt2 | 0.244s | 27.644MiB| sat | 0 | | | |auk-0124.smt2 | 0.245s | 32.2MiB| sat | 0 | | | |auk-0154.smt2 | 0.247s | 30.456MiB| sat | 0 | | | |auk-0118.smt2 | 0.248s | 32.892MiB| sat | 0 | | | |auk-0167.smt2 | 0.248s | 31.404MiB| sat | 0 | | | |auk-0177.smt2 | 0.248s | 31.356MiB| sat | 0 | | | |auk-0171.smt2 | 0.251s | 32.292MiB| sat | 0 | | | |auk-0108.smt2 | 0.256s | 34.832MiB| sat | 0 | | | |auk-0102.smt2 | 0.266s | 32.06MiB| sat | 0 | | | |auk-0173.smt2 | 0.268s | 30.32MiB| sat | 0 | | | |auk-0176.smt2 | 0.269s | 31.532MiB| sat | 0 | | | |auk-0030.smt2 | 0.277s | 27.712MiB| unsat | 0 | | | |auk-0143.smt2 | 0.281s | 21.48MiB| unsat | 0 | | | |auk-0150.smt2 | 0.292s | 28.844MiB| unsat | 0 | | | |auk-0056.smt2 | 0.293s | 29.948MiB| sat | 0 | | | |auk-0121.smt2 | 0.294s | 31.256MiB| sat | 0 | | | |auk-0112.smt2 | 0.297s | 32.916MiB| sat | 0 | | | |auk-0105.smt2 | 0.302s | 32.42MiB| sat | 0 | | | |auk-0062.smt2 | 0.320s | 30.76MiB| unsat | 0 | | | |auk-0111.smt2 | 0.322s | 32.54MiB| sat | 0 | | | |auk-0136.smt2 | 0.326s | 20.9MiB| sat | 0 | | | |auk-0122.smt2 | 0.331s | 34.82MiB| sat | 0 | | | |auk-0126.smt2 | 0.334s | 33.652MiB| sat | 0 | | | |auk-0180.smt2 | 0.358s | 30.356MiB| unsat | 0 | | | |auk-0103.smt2 | 0.361s | 32.936MiB| sat | 0 | | | |auk-0153.smt2 | 0.362s | 31.304MiB| sat | 0 | | | |auk-0175.smt2 | 0.376s | 31.852MiB| sat | 0 | | | |auk-0106.smt2 | 0.387s | 32.22MiB| sat | 0 | | | |auk-0023.smt2 | 0.409s | 29.568MiB| unsat | 0 | | | |auk-0127.smt2 | 0.421s | 32.812MiB| sat | 0 | | | |auk-0113.smt2 | 0.431s | 34.948MiB| sat | 0 | | | |auk-0117.smt2 | 0.432s | 35.64MiB| sat | 0 | | | |auk-0128.smt2 | 0.462s | 36.976MiB| sat | 0 | | | |auk-0096.smt2 | 0.507s | 32.536MiB| sat | 0 | | | |auk-0135.smt2 | 0.517s | 30.648MiB| unsat | 0 | | | |auk-0120.smt2 | 0.527s | 36.2MiB| sat | 0 | | | |auk-0115.smt2 | 0.557s | 40.276MiB| sat | 0 | | | |auk-0094.smt2 | 0.598s | 35.56MiB| sat | 0 | | | |auk-0123.smt2 | 0.604s | 35.616MiB| sat | 0 | | | |auk-0070.smt2 | 0.658s | 36.688MiB| sat | 0 | | | |auk-0009.smt2 | 0.686s | 22.736MiB| sat | 0 | | | |auk-0072.smt2 | 0.733s | 34.536MiB| sat | 0 | | | |auk-0080.smt2 | 0.753s | 40.404MiB| sat | 0 | | | |auk-0078.smt2 | 0.760s | 34.696MiB| sat | 0 | | | |auk-0049.smt2 | 0.769s | 21.94MiB| unsat | 0 | | | |auk-0116.smt2 | 0.780s | 34.156MiB| sat | 0 | | | |auk-0119.smt2 | 0.797s | 40.012MiB| sat | 0 | | | |auk-0074.smt2 | 0.803s | 36.228MiB| unsat | 0 | | | |auk-0109.smt2 | 0.897s | 98.0MiB| sat | 0 | | | |auk-0133.smt2 | 0.985s | 44.724MiB| sat | 0 | | | |auk-0027.smt2 | 1.052s | 30.068MiB| unsat | 0 | | | |auk-0071.smt2 | 1.143s | 47.116MiB| sat | 0 | | | |auk-0073.smt2 | 1.169s | 46.972MiB| sat | 0 | | | |auk-0146.smt2 | 1.217s | 32.04MiB| unsat | 0 | | | |auk-0101.smt2 | 1.288s | 36.988MiB| unsat | 0 | | | |auk-0075.smt2 | 1.361s | 47.052MiB| sat | 0 | | | |auk-0145.smt2 | 1.440s | 34.78MiB| unsat | 0 | | | |auk-0076.smt2 | 1.478s | 47.164MiB| sat | 0 | | | |auk-0130.smt2 | 1.549s | 38.42MiB| sat | 0 | | | |auk-0132.smt2 | 2.008s | 63.668MiB| sat | 0 | | | |auk-0081.smt2 | 2.387s | 42.364MiB| unsat | 0 | | | |auk-0053.smt2 | 2.629s | 22.904MiB| sat | 0 | | | |auk-0082.smt2 | 2.753s | 98.0MiB| sat | 0 | | | |auk-0083.smt2 | 2.775s | 98.0MiB| sat | 0 | | | |auk-0148.smt2 | 2.777s | 37.084MiB| unsat | 0 | | | |auk-0182.smt2 | 2.813s | 52.088MiB| unsat | 0 | | | |auk-0095.smt2 | 2.826s | 39.884MiB| unsat | 0 | | | |auk-0144.smt2 | 2.930s | 38.124MiB| unsat | 0 | | | |auk-0142.smt2 | 3.440s | 37.728MiB| unsat | 0 | | | |auk-0149.smt2 | 3.754s | 31.716MiB| unsat | 0 | | | |auk-0131.smt2 | 3.927s | 99.04MiB| sat | 0 | | | |auk-0002.smt2 | 3.967s | 43.032MiB| unsat | 0 | | | |auk-0187.smt2 | 4.449s | 47.736MiB| unsat | 0 | | | |auk-0077.smt2 | 4.472s | 54.492MiB| sat | 0 | | | |auk-0079.smt2 | 6.559s | 56.868MiB| sat | 0 | | | |auk-0183.smt2 | 7.288s | 64.332MiB| unsat | 0 | | | |auk-0134.smt2 | 7.462s | 40.82MiB| sat | 0 | | | |auk-0084.smt2 | 11.922s | 56.752MiB| unsat | 0 | | | |auk-0090.smt2 | 14.289s | 60.432MiB| unsat | 0 | | | |auk-0141.smt2 | 18.210s | 49.328MiB| unsat | 0 | | | |auk-0007.smt2 | 20.263s | 44.932MiB| sat | 0 | | | |auk-0147.smt2 | 30.011s | 33.172MiB| timeout | 0 | | | |auk-0188.smt2 | 30.012s | 45.736MiB| timeout | 0 | | | |auk-0025.smt2 | 30.013s | 36.12MiB| timeout | 0 | | | |auk-0091.smt2 | 30.015s | 48.72MiB| timeout | 0 | | | |auk-0001.smt2 | 30.015s | 23.26MiB| timeout | 0 | | | |auk-0015.smt2 | 30.015s | 55.832MiB| timeout | 0 | | | |auk-0185.smt2 | 30.016s | 49.332MiB| timeout | 0 | | | |auk-0184.smt2 | 30.016s | 55.456MiB| timeout | 0 | | | |auk-0005.smt2 | 30.017s | 53.184MiB| timeout | 0 | | | |auk-0088.smt2 | 30.017s | 80.492MiB| timeout | 0 | | | |auk-0189.smt2 | 30.017s | 56.26MiB| timeout | 0 | | | |auk-0140.smt2 | 30.018s | 58.168MiB| timeout | 0 | | | |auk-0139.smt2 | 30.018s | 31.98MiB| timeout | 0 | | | |auk-0181.smt2 | 30.019s | 64.144MiB| timeout | 0 | | | |auk-0092.smt2 | 30.019s | 85.684MiB| timeout | 0 | | | |auk-0085.smt2 | 30.019s | 88.72MiB| timeout | 0 | | | |auk-0186.smt2 | 30.019s | 63.248MiB| timeout | 0 | | | |auk-0087.smt2 | 30.020s | 72.596MiB| timeout | 0 | | | |auk-0003.smt2 | 30.020s | 55.908MiB| timeout | 0 | | | |auk-0013.smt2 | 30.023s | 53.776MiB| timeout | 0 | | | |auk-0086.smt2 | 30.023s | 89.08MiB| timeout | 0 | | | |auk-0022.smt2 | 30.024s | 32.788MiB| timeout | 0 | | | |auk-0008.smt2 | 30.024s | 53.808MiB| timeout | 0 | | | |auk-0137.smt2 | 30.025s | 39.604MiB| timeout | 0 | | | |auk-0011.smt2 | 30.025s | 47.42MiB| timeout | 0 | | | |auk-0010.smt2 | 30.026s | 52.52MiB| timeout | 0 | | | |auk-0014.smt2 | 30.026s | 55.08MiB| timeout | 0 | | | |auk-0151.smt2 | 30.026s | 58.448MiB| timeout | 0 | | | |auk-0089.smt2 | 30.030s | 99.0MiB| timeout | 0 | | | |auk-0004.smt2 | 30.032s | 44.236MiB| timeout | 0 | | | |auk-0098.smt2 | 30.043s | 146.0MiB| timeout | 0 | | | |auk-0099.smt2 | 30.045s | 143.0MiB| timeout | 0 | | | |auk-0006.smt2 | 30.048s | 317.0MiB| timeout | 0 | | |