# . * SAT 66 * UNSAT 69 * TIMEOUT 32 * UNKNOWN 0 * UNSET 22 * ERROR 22 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: certora2-model-bounds
Runner: lev-ripper
Z3 repo: Z3Prover/z3
Z3 commit: ee63585581cf7bd23fdb34821d6b055bdb582b20
Z3 branch: arie
Z3 options: "-T:30 smt.arith.nl.nra.model_bounds=true"
Z3 inputs: inputs/certora2
Z3 commit message: update model-guide heuristic

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |auk-0066.smt2 | 0.108s | 19.74MiB| sat | 0 | | | |auk-0064.smt2 | 0.150s | 20.764MiB| unset | 114 | | | |auk-0057.smt2 | 0.154s | 19.956MiB| unsat | 0 | | | |auk-0012.smt2 | 0.155s | 20.44MiB| unsat | 0 | | | |auk-0060.smt2 | 0.169s | 20.14MiB| unsat | 0 | | | |auk-0036.smt2 | 0.184s | 21.084MiB| unset | 114 | | | |auk-0061.smt2 | 0.202s | 21.016MiB| unsat | 0 | | | |auk-0054.smt2 | 0.205s | 18.936MiB| unsat | 0 | | | |auk-0159.smt2 | 0.230s | 20.512MiB| unsat | 0 | | | |auk-0136.smt2 | 0.230s | 20.848MiB| unset | 114 | | | |auk-0067.smt2 | 0.234s | 20.252MiB| unset | 114 | | | |auk-0028.smt2 | 0.238s | 22.384MiB| unsat | 0 | | | |auk-0032.smt2 | 0.243s | 20.592MiB| unsat | 0 | | | |auk-0059.smt2 | 0.263s | 22.788MiB| unsat | 0 | | | |auk-0179.smt2 | 0.275s | 19.94MiB| unsat | 0 | | | |auk-0038.smt2 | 0.300s | 18.932MiB| unsat | 0 | | | |auk-0043.smt2 | 0.304s | 24.24MiB| unsat | 0 | | | |auk-0063.smt2 | 0.318s | 20.752MiB| unsat | 0 | | | |auk-0125.smt2 | 0.327s | 26.42MiB| unset | 114 | | | |auk-0172.smt2 | 0.329s | 25.824MiB| sat | 0 | | | |auk-0058.smt2 | 0.330s | 24.74MiB| sat | 0 | | | |auk-0040.smt2 | 0.334s | 20.252MiB| unsat | 0 | | | |auk-0161.smt2 | 0.334s | 19.44MiB| sat | 0 | | | |auk-0093.smt2 | 0.336s | 24.184MiB| unset | 114 | | | |auk-0138.smt2 | 0.340s | 20.252MiB| unsat | 0 | | | |auk-0031.smt2 | 0.344s | 20.348MiB| unsat | 0 | | | |auk-0173.smt2 | 0.357s | 25.764MiB| sat | 0 | | | |auk-0069.smt2 | 0.358s | 20.256MiB| unsat | 0 | | | |auk-0039.smt2 | 0.366s | 20.652MiB| unsat | 0 | | | |auk-0170.smt2 | 0.367s | 20.764MiB| unsat | 0 | | | |auk-0068.smt2 | 0.372s | 19.848MiB| unsat | 0 | | | |auk-0044.smt2 | 0.373s | 20.752MiB| unsat | 0 | | | |auk-0169.smt2 | 0.389s | 26.208MiB| unsat | 0 | | | |auk-0121.smt2 | 0.391s | 26.668MiB| sat | 0 | | | |auk-0174.smt2 | 0.393s | 25.756MiB| sat | 0 | | | |auk-0100.smt2 | 0.398s | 24.408MiB| sat | 0 | | | |auk-0062.smt2 | 0.404s | 24.768MiB| unsat | 0 | | | |auk-0050.smt2 | 0.408s | 20.356MiB| unsat | 0 | | | |auk-0155.smt2 | 0.410s | 25.312MiB| sat | 0 | | | |auk-0156.smt2 | 0.415s | 25.288MiB| sat | 0 | | | |auk-0042.smt2 | 0.430s | 20.208MiB| unset | 114 | | | |auk-0065.smt2 | 0.434s | 20.572MiB| unsat | 0 | | | |auk-0166.smt2 | 0.448s | 20.912MiB| sat | 0 | | | |auk-0008.smt2 | 0.451s | 27.932MiB| unsat | 0 | | | |auk-0163.smt2 | 0.453s | 25.692MiB| sat | 0 | | | |auk-0124.smt2 | 0.455s | 26.932MiB| sat | 0 | | | |auk-0046.smt2 | 0.457s | 19.864MiB| unsat | 0 | | | |auk-0105.smt2 | 0.473s | 27.228MiB| sat | 0 | | | |auk-0035.smt2 | 0.492s | 20.256MiB| unsat | 0 | | | |auk-0041.smt2 | 0.495s | 20.256MiB| unsat | 0 | | | |auk-0102.smt2 | 0.508s | 26.916MiB| sat | 0 | | | |auk-0152.smt2 | 0.508s | 25.092MiB| sat | 0 | | | |auk-0026.smt2 | 0.510s | 24.968MiB| unsat | 0 | | | |auk-0019.smt2 | 0.511s | 27.152MiB| unsat | 0 | | | |auk-0178.smt2 | 0.515s | 19.808MiB| sat | 0 | | | |auk-0047.smt2 | 0.520s | 25.436MiB| unsat | 0 | | | |auk-0024.smt2 | 0.522s | 25.548MiB| unsat | 0 | | | |auk-0052.smt2 | 0.524s | 25.044MiB| unsat | 0 | | | |auk-0118.smt2 | 0.535s | 26.968MiB| sat | 0 | | | |auk-0168.smt2 | 0.549s | 20.196MiB| unset | 114 | | | |auk-0160.smt2 | 0.556s | 20.032MiB| unsat | 0 | | | |auk-0051.smt2 | 0.560s | 21.176MiB| unsat | 0 | | | |auk-0126.smt2 | 0.562s | 28.352MiB| sat | 0 | | | |auk-0055.smt2 | 0.595s | 24.652MiB| sat | 0 | | | |auk-0033.smt2 | 0.613s | 26.036MiB| sat | 0 | | | |auk-0162.smt2 | 0.615s | 24.532MiB| sat | 0 | | | |auk-0158.smt2 | 0.661s | 25.124MiB| sat | 0 | | | |auk-0154.smt2 | 0.668s | 26.256MiB| sat | 0 | | | |auk-0112.smt2 | 0.670s | 27.096MiB| sat | 0 | | | |auk-0111.smt2 | 0.707s | 28.528MiB| sat | 0 | | | |auk-0029.smt2 | 0.753s | 26.164MiB| unsat | 0 | | | |auk-0016.smt2 | 0.786s | 25.144MiB| unsat | 0 | | | |auk-0143.smt2 | 0.787s | 21.316MiB| unsat | 0 | | | |auk-0177.smt2 | 0.804s | 26.384MiB| sat | 0 | | | |auk-0175.smt2 | 0.809s | 26.468MiB| sat | 0 | | | |auk-0007.smt2 | 0.810s | 31.244MiB| unset | 114 | | | |auk-0048.smt2 | 0.814s | 25.592MiB| unsat | 0 | | | |auk-0165.smt2 | 0.834s | 25.264MiB| sat | 0 | | | |auk-0167.smt2 | 0.835s | 25.28MiB| sat | 0 | | | |auk-0030.smt2 | 0.836s | 25.348MiB| unsat | 0 | | | |auk-0056.smt2 | 0.837s | 25.616MiB| unset | 114 | | | |auk-0171.smt2 | 0.846s | 25.62MiB| sat | 0 | | | |auk-0034.smt2 | 0.903s | 20.656MiB| unsat | 0 | | | |auk-0151.smt2 | 0.909s | 21.92MiB| unsat | 0 | | | |auk-0176.smt2 | 0.916s | 26.408MiB| sat | 0 | | | |auk-0110.smt2 | 0.932s | 24.8MiB| sat | 0 | | | |auk-0107.smt2 | 0.956s | 26.736MiB| sat | 0 | | | |auk-0106.smt2 | 0.957s | 26.796MiB| sat | 0 | | | |auk-0003.smt2 | 0.963s | 27.944MiB| unsat | 0 | | | |auk-0097.smt2 | 1.007s | 22.836MiB| sat | 0 | | | |auk-0002.smt2 | 1.017s | 33.952MiB| unsat | 0 | | | |auk-0021.smt2 | 1.045s | 23.46MiB| unsat | 0 | | | |auk-0150.smt2 | 1.051s | 25.784MiB| unsat | 0 | | | |auk-0157.smt2 | 1.092s | 24.988MiB| sat | 0 | | | |auk-0020.smt2 | 1.108s | 25.4MiB| unsat | 0 | | | |auk-0013.smt2 | 1.139s | 27.988MiB| unsat | 0 | | | |auk-0104.smt2 | 1.139s | 23.996MiB| sat | 0 | | | |auk-0014.smt2 | 1.156s | 27.944MiB| unsat | 0 | | | |auk-0115.smt2 | 1.190s | 34.344MiB| sat | 0 | | | |auk-0117.smt2 | 1.195s | 29.976MiB| unset | 114 | | | |auk-0129.smt2 | 1.211s | 25.012MiB| sat | 0 | | | |auk-0018.smt2 | 1.213s | 27.224MiB| unset | 114 | | | |auk-0153.smt2 | 1.225s | 26.496MiB| sat | 0 | | | |auk-0096.smt2 | 1.228s | 26.484MiB| unset | 114 | | | |auk-0049.smt2 | 1.238s | 21.816MiB| unsat | 0 | | | |auk-0010.smt2 | 1.322s | 33.928MiB| unsat | 0 | | | |auk-0037.smt2 | 1.336s | 25.924MiB| unsat | 0 | | | |auk-0127.smt2 | 1.389s | 26.56MiB| sat | 0 | | | |auk-0139.smt2 | 1.405s | 21.536MiB| unsat | 0 | | | |auk-0045.smt2 | 1.407s | 25.728MiB| unsat | 0 | | | |auk-0080.smt2 | 1.408s | 34.656MiB| sat | 0 | | | |auk-0027.smt2 | 1.446s | 26.324MiB| unset | 114 | | | |auk-0022.smt2 | 1.449s | 27.008MiB| unset | 114 | | | |auk-0006.smt2 | 1.458s | 34.332MiB| unsat | 0 | | | |auk-0108.smt2 | 1.512s | 28.444MiB| sat | 0 | | | |auk-0123.smt2 | 1.565s | 31.396MiB| sat | 0 | | | |auk-0130.smt2 | 1.574s | 33.72MiB| unset | 114 | | | |auk-0180.smt2 | 1.599s | 28.404MiB| unsat | 0 | | | |auk-0023.smt2 | 1.659s | 28.904MiB| unsat | 0 | | | |auk-0017.smt2 | 1.670s | 30.204MiB| unset | 114 | | | |auk-0091.smt2 | 1.752s | 43.176MiB| sat | 0 | | | |auk-0109.smt2 | 1.843s | 44.636MiB| sat | 0 | | | |auk-0114.smt2 | 1.867s | 25.74MiB| sat | 0 | | | |auk-0122.smt2 | 1.876s | 29.84MiB| unset | 114 | | | |auk-0116.smt2 | 1.924s | 31.308MiB| sat | 0 | | | |auk-0164.smt2 | 1.939s | 25.552MiB| sat | 0 | | | |auk-0072.smt2 | 1.953s | 32.056MiB| sat | 0 | | | |auk-0103.smt2 | 1.967s | 27.136MiB| unset | 114 | | | |auk-0113.smt2 | 2.029s | 31.008MiB| sat | 0 | | | |auk-0094.smt2 | 2.197s | 31.512MiB| sat | 0 | | | |auk-0128.smt2 | 2.238s | 32.06MiB| sat | 0 | | | |auk-0120.smt2 | 2.263s | 32.296MiB| unset | 114 | | | |auk-0146.smt2 | 2.364s | 28.976MiB| unsat | 0 | | | |auk-0119.smt2 | 2.449s | 35.68MiB| sat | 0 | | | |auk-0145.smt2 | 2.525s | 31.14MiB| unsat | 0 | | | |auk-0004.smt2 | 2.594s | 36.404MiB| unsat | 0 | | | |auk-0076.smt2 | 2.843s | 47.252MiB| sat | 0 | | | |auk-0135.smt2 | 3.163s | 28.192MiB| unsat | 0 | | | |auk-0149.smt2 | 3.699s | 29.28MiB| unsat | 0 | | | |auk-0101.smt2 | 4.157s | 33.832MiB| unsat | 0 | | | |auk-0132.smt2 | 4.281s | 56.224MiB| sat | 0 | | | |auk-0025.smt2 | 4.571s | 31.908MiB| unsat | 0 | | | |auk-0071.smt2 | 5.536s | 47.272MiB| sat | 0 | | | |auk-0075.smt2 | 5.746s | 47.192MiB| sat | 0 | | | |auk-0078.smt2 | 6.531s | 32.188MiB| sat | 0 | | | |auk-0053.smt2 | 6.617s | 23.68MiB| unset | 114 | | | |auk-0073.smt2 | 6.759s | 47.208MiB| sat | 0 | | | |auk-0133.smt2 | 7.063s | 41.928MiB| sat | 0 | | | |auk-0131.smt2 | 7.719s | 90.156MiB| sat | 0 | | | |auk-0077.smt2 | 10.744s | 42.408MiB| sat | 0 | | | |auk-0009.smt2 | 14.986s | 22.164MiB| unset | 114 | | | |auk-0070.smt2 | 15.232s | 33.144MiB| sat | 0 | | | |auk-0148.smt2 | 16.072s | 35.22MiB| unsat | 0 | | | |auk-0079.smt2 | 16.799s | 45.624MiB| sat | 0 | | | |auk-0144.smt2 | 21.484s | 35.02MiB| unsat | 0 | | | |auk-0095.smt2 | 22.048s | 38.76MiB| unsat | 0 | | | |auk-0142.smt2 | 27.121s | 36.384MiB| unsat | 0 | | | |auk-0011.smt2 | 30.063s | 40.58MiB| timeout | 0 | | | |auk-0147.smt2 | 30.074s | 25.848MiB| timeout | 0 | | | |auk-0181.smt2 | 30.078s | 65.18MiB| timeout | 0 | | | |auk-0137.smt2 | 30.079s | 28.304MiB| timeout | 0 | | | |auk-0089.smt2 | 30.101s | 60.428MiB| timeout | 0 | | | |auk-0187.smt2 | 30.121s | 48.808MiB| timeout | 0 | | | |auk-0005.smt2 | 30.128s | 38.804MiB| timeout | 0 | | | |auk-0087.smt2 | 30.132s | 61.972MiB| timeout | 0 | | | |auk-0188.smt2 | 30.135s | 51.076MiB| timeout | 0 | | | |auk-0182.smt2 | 30.138s | 68.54MiB| timeout | 0 | | | |auk-0001.smt2 | 30.140s | 22.7MiB| timeout | 0 | | | |auk-0141.smt2 | 30.142s | 46.048MiB| timeout | 0 | | | |auk-0099.smt2 | 30.164s | 118.0MiB| timeout | 0 | | | |auk-0015.smt2 | 30.171s | 38.36MiB| timeout | 0 | | | |auk-0085.smt2 | 30.173s | 76.156MiB| timeout | 0 | | | |auk-0082.smt2 | 30.173s | 77.988MiB| timeout | 0 | | | |auk-0088.smt2 | 30.184s | 59.696MiB| timeout | 0 | | | |auk-0086.smt2 | 30.185s | 55.128MiB| timeout | 0 | | | |auk-0189.smt2 | 30.187s | 49.036MiB| timeout | 0 | | | |auk-0134.smt2 | 30.194s | 33.568MiB| timeout | 0 | | | |auk-0140.smt2 | 30.199s | 35.22MiB| timeout | 0 | | | |auk-0184.smt2 | 30.203s | 38.512MiB| timeout | 0 | | | |auk-0083.smt2 | 30.235s | 74.796MiB| timeout | 0 | | | |auk-0185.smt2 | 30.238s | 49.012MiB| timeout | 0 | | | |auk-0183.smt2 | 30.247s | 55.684MiB| timeout | 0 | | | |auk-0074.smt2 | 30.249s | 32.236MiB| timeout | 0 | | | |auk-0092.smt2 | 30.253s | 54.84MiB| timeout | 0 | | | |auk-0084.smt2 | 30.267s | 54.784MiB| timeout | 0 | | | |auk-0186.smt2 | 30.377s | 55.776MiB| timeout | 0 | | | |auk-0090.smt2 | 30.386s | 54.408MiB| timeout | 0 | | | |auk-0098.smt2 | 30.443s | 115.0MiB| timeout | 0 | | | |auk-0081.smt2 | 30.451s | 34.556MiB| timeout | 0 | | |