# data

* SAT 1
* UNSAT 0
* TIMEOUT 185
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: smt-sls
Z3 repo: https://github.com/Z3Prover/z3
Z3 commit: 9770c005926e2085d4ede18f03d56cb67d762d84
Z3 branch: master
Z3 options: "-T:20 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify sls-smt)" model_validate=true"
Z3 inputs: inputs/QF_NIA_MCM
Z3 commit message: adjust heuristic in random-inc-dec for finite domains

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|107.smt2                                                     |   18.488s | 21.956MiB| sat | 0 |  |  |
|175.smt2                                                     |   19.465s | 132.0MiB| timeout | 0 |  |  |
|115.smt2                                                     |   19.490s | 23.732MiB| timeout | 0 |  |  |
|117.smt2                                                     |   19.580s | 21.948MiB| timeout | 0 |  |  |
|142.smt2                                                     |   19.588s | 35.504MiB| timeout | 0 |  |  |
|108.smt2                                                     |   19.593s | 31.904MiB| timeout | 0 |  |  |
|25.smt2                                                      |   19.618s | 21.92MiB| timeout | 0 |  |  |
|111.smt2                                                     |   19.644s | 31.588MiB| timeout | 0 |  |  |
|162.smt2                                                     |   19.653s | 25.876MiB| timeout | 0 |  |  |
|132.smt2                                                     |   19.658s | 37.768MiB| timeout | 0 |  |  |
|96.smt2                                                      |   19.688s | 23.664MiB| timeout | 0 |  |  |
|100.smt2                                                     |   19.693s | 22.78MiB| timeout | 0 |  |  |
|17.smt2                                                      |   19.725s | 22.744MiB| timeout | 0 |  |  |
|87.smt2                                                      |   19.740s | 20.836MiB| timeout | 0 |  |  |
|147.smt2                                                     |   19.747s | 33.96MiB| timeout | 0 |  |  |
|90.smt2                                                      |   19.768s | 23.656MiB| timeout | 0 |  |  |
|93.smt2                                                      |   19.769s | 21.04MiB| timeout | 0 |  |  |
|122.smt2                                                     |   19.776s | 36.2MiB| timeout | 0 |  |  |
|110.smt2                                                     |   19.785s | 33.9MiB| timeout | 0 |  |  |
|97.smt2                                                      |   19.785s | 22.78MiB| timeout | 0 |  |  |
|121.smt2                                                     |   19.802s | 38.316MiB| timeout | 0 |  |  |
|31.smt2                                                      |   19.814s | 22.608MiB| timeout | 0 |  |  |
|16.smt2                                                      |   19.817s | 23.644MiB| timeout | 0 |  |  |
|123.smt2                                                     |   19.820s | 29.896MiB| timeout | 0 |  |  |
|135.smt2                                                     |   19.825s | 38.304MiB| timeout | 0 |  |  |
|71.smt2                                                      |   19.826s | 22.636MiB| timeout | 0 |  |  |
|80.smt2                                                      |   19.828s | 23.652MiB| timeout | 0 |  |  |
|64.smt2                                                      |   19.829s | 23.656MiB| timeout | 0 |  |  |
|154.smt2                                                     |   19.853s | 36.444MiB| timeout | 0 |  |  |
|129.smt2                                                     |   19.854s | 35.868MiB| timeout | 0 |  |  |
|86.smt2                                                      |   19.864s | 21.308MiB| timeout | 0 |  |  |
|182.smt2                                                     |   19.868s | 274.0MiB| timeout | 0 |  |  |
|37.smt2                                                      |   19.870s | 22.868MiB| timeout | 0 |  |  |
|118.smt2                                                     |   19.871s | 22.168MiB| timeout | 0 |  |  |
|19.smt2                                                      |   19.872s | 21.912MiB| timeout | 0 |  |  |
|120.smt2                                                     |   19.875s | 36.372MiB| timeout | 0 |  |  |
|172.smt2                                                     |   19.879s | 144.0MiB| timeout | 0 |  |  |
|21.smt2                                                      |   19.880s | 21.928MiB| timeout | 0 |  |  |
|01.smt2                                                      |   19.884s | 22.192MiB| timeout | 0 |  |  |
|29.smt2                                                      |   19.887s | 22.372MiB| timeout | 0 |  |  |
|140.smt2                                                     |   19.897s | 34.944MiB| timeout | 0 |  |  |
|69.smt2                                                      |   19.898s | 22.64MiB| timeout | 0 |  |  |
|104.smt2                                                     |   19.901s | 23.724MiB| timeout | 0 |  |  |
|149.smt2                                                     |   19.904s | 36.66MiB| timeout | 0 |  |  |
|103.smt2                                                     |   19.904s | 22.8MiB| timeout | 0 |  |  |
|13.smt2                                                      |   19.907s | 21.784MiB| timeout | 0 |  |  |
|176.smt2                                                     |   19.909s | 143.0MiB| timeout | 0 |  |  |
|116.smt2                                                     |   19.914s | 36.06MiB| timeout | 0 |  |  |
|98.smt2                                                      |   19.922s | 22.636MiB| timeout | 0 |  |  |
|27.smt2                                                      |   19.923s | 22.744MiB| timeout | 0 |  |  |
|183.smt2                                                     |   19.929s | 273.0MiB| timeout | 0 |  |  |
|11.smt2                                                      |   19.933s | 20.812MiB| timeout | 0 |  |  |
|186.smt2                                                     |   19.939s | 245.0MiB| timeout | 0 |  |  |
|44.smt2                                                      |   19.942s | 20.592MiB| timeout | 0 |  |  |
|09.smt2                                                      |   19.942s | 20.86MiB| timeout | 0 |  |  |
|77.smt2                                                      |   19.943s | 22.78MiB| timeout | 0 |  |  |
|20.smt2                                                      |   19.949s | 22.748MiB| timeout | 0 |  |  |
|184.smt2                                                     |   19.951s | 136.0MiB| timeout | 0 |  |  |
|158.smt2                                                     |   19.951s | 60.092MiB| timeout | 0 |  |  |
|83.smt2                                                      |   19.952s | 22.352MiB| timeout | 0 |  |  |
|180.smt2                                                     |   19.952s | 146.0MiB| timeout | 0 |  |  |
|141.smt2                                                     |   19.953s | 33.744MiB| timeout | 0 |  |  |
|155.smt2                                                     |   19.953s | 31.332MiB| timeout | 0 |  |  |
|153.smt2                                                     |   19.954s | 38.312MiB| timeout | 0 |  |  |
|74.smt2                                                      |   19.956s | 23.656MiB| timeout | 0 |  |  |
|65.smt2                                                      |   19.961s | 22.784MiB| timeout | 0 |  |  |
|61.smt2                                                      |   19.965s | 22.772MiB| timeout | 0 |  |  |
|181.smt2                                                     |   19.972s | 155.0MiB| timeout | 0 |  |  |
|133.smt2                                                     |   19.975s | 35.528MiB| timeout | 0 |  |  |
|160.smt2                                                     |   19.979s | 60.948MiB| timeout | 0 |  |  |
|10.smt2                                                      |   19.981s | 21.552MiB| timeout | 0 |  |  |
|07.smt2                                                      |   19.982s | 21.488MiB| timeout | 0 |  |  |
|51.smt2                                                      |   19.983s | 21.936MiB| timeout | 0 |  |  |
|112.smt2                                                     |   19.984s | 31.596MiB| timeout | 0 |  |  |
|57.smt2                                                      |   19.984s | 23.656MiB| timeout | 0 |  |  |
|134.smt2                                                     |   19.985s | 36.136MiB| timeout | 0 |  |  |
|164.smt2                                                     |   19.987s | 25.892MiB| timeout | 0 |  |  |
|33.smt2                                                      |   19.988s | 21.48MiB| timeout | 0 |  |  |
|62.smt2                                                      |   19.988s | 23.668MiB| timeout | 0 |  |  |
|36.smt2                                                      |   19.989s | 21.656MiB| timeout | 0 |  |  |
|144.smt2                                                     |   19.989s | 38.324MiB| timeout | 0 |  |  |
|165.smt2                                                     |   19.989s | 76.476MiB| timeout | 0 |  |  |
|130.smt2                                                     |   19.990s | 33.42MiB| timeout | 0 |  |  |
|54.smt2                                                      |   19.990s | 22.784MiB| timeout | 0 |  |  |
|26.smt2                                                      |   19.990s | 21.92MiB| timeout | 0 |  |  |
|50.smt2                                                      |   19.991s | 23.028MiB| timeout | 0 |  |  |
|113.smt2                                                     |   19.991s | 21.292MiB| timeout | 0 |  |  |
|56.smt2                                                      |   19.992s | 24.68MiB| timeout | 0 |  |  |
|45.smt2                                                      |   19.992s | 20.164MiB| timeout | 0 |  |  |
|139.smt2                                                     |   19.992s | 29.568MiB| timeout | 0 |  |  |
|70.smt2                                                      |   19.993s | 23.644MiB| timeout | 0 |  |  |
|99.smt2                                                      |   19.993s | 21.752MiB| timeout | 0 |  |  |
|41.smt2                                                      |   19.994s | 21.48MiB| timeout | 0 |  |  |
|148.smt2                                                     |   19.994s | 35.532MiB| timeout | 0 |  |  |
|174.smt2                                                     |   19.994s | 132.0MiB| timeout | 0 |  |  |
|85.smt2                                                      |   19.996s | 22.088MiB| timeout | 0 |  |  |
|03.smt2                                                      |   19.996s | 21.836MiB| timeout | 0 |  |  |
|12.smt2                                                      |   19.996s | 19.916MiB| timeout | 0 |  |  |
|49.smt2                                                      |   19.996s | 21.704MiB| timeout | 0 |  |  |
|88.smt2                                                      |   19.996s | 23.668MiB| timeout | 0 |  |  |
|157.smt2                                                     |   19.997s | 33.464MiB| timeout | 0 |  |  |
|42.smt2                                                      |   19.997s | 20.656MiB| timeout | 0 |  |  |
|32.smt2                                                      |   19.997s | 21.796MiB| timeout | 0 |  |  |
|58.smt2                                                      |   19.997s | 23.664MiB| timeout | 0 |  |  |
|08.smt2                                                      |   19.998s | 20.524MiB| timeout | 0 |  |  |
|114.smt2                                                     |   19.998s | 30.168MiB| timeout | 0 |  |  |
|40.smt2                                                      |   19.998s | 22.752MiB| timeout | 0 |  |  |
|47.smt2                                                      |   19.998s | 22.632MiB| timeout | 0 |  |  |
|128.smt2                                                     |   19.998s | 34.22MiB| timeout | 0 |  |  |
|79.smt2                                                      |   19.998s | 23.72MiB| timeout | 0 |  |  |
|167.smt2                                                     |   19.998s | 58.168MiB| timeout | 0 |  |  |
|24.smt2                                                      |   19.999s | 22.744MiB| timeout | 0 |  |  |
|34.smt2                                                      |   19.999s | 21.096MiB| timeout | 0 |  |  |
|94.smt2                                                      |   19.999s | 23.916MiB| timeout | 0 |  |  |
|137.smt2                                                     |   19.999s | 36.188MiB| timeout | 0 |  |  |
|136.smt2                                                     |   19.999s | 36.188MiB| timeout | 0 |  |  |
|127.smt2                                                     |   20.000s | 36.052MiB| timeout | 0 |  |  |
|185.smt2                                                     |   20.000s | 245.0MiB| timeout | 0 |  |  |
|46.smt2                                                      |   20.000s | 23.732MiB| timeout | 0 |  |  |
|177.smt2                                                     |   20.000s | 43.864MiB| timeout | 0 |  |  |
|145.smt2                                                     |   20.000s | 36.188MiB| timeout | 0 |  |  |
|82.smt2                                                      |   20.000s | 23.352MiB| timeout | 0 |  |  |
|81.smt2                                                      |   20.001s | 22.776MiB| timeout | 0 |  |  |
|78.smt2                                                      |   20.001s | 24.532MiB| timeout | 0 |  |  |
|84.smt2                                                      |   20.001s | 21.032MiB| timeout | 0 |  |  |
|63.smt2                                                      |   20.001s | 22.78MiB| timeout | 0 |  |  |
|02.smt2                                                      |   20.001s | 21.724MiB| timeout | 0 |  |  |
|35.smt2                                                      |   20.001s | 22.592MiB| timeout | 0 |  |  |
|170.smt2                                                     |   20.001s | 25.888MiB| timeout | 0 |  |  |
|169.smt2                                                     |   20.001s | 78.576MiB| timeout | 0 |  |  |
|152.smt2                                                     |   20.001s | 27.656MiB| timeout | 0 |  |  |
|168.smt2                                                     |   20.001s | 67.428MiB| timeout | 0 |  |  |
|18.smt2                                                      |   20.001s | 22.748MiB| timeout | 0 |  |  |
|161.smt2                                                     |   20.002s | 73.5MiB| timeout | 0 |  |  |
|109.smt2                                                     |   20.002s | 22.168MiB| timeout | 0 |  |  |
|124.smt2                                                     |   20.002s | 27.564MiB| timeout | 0 |  |  |
|38.smt2                                                      |   20.002s | 21.812MiB| timeout | 0 |  |  |
|52.smt2                                                      |   20.002s | 23.912MiB| timeout | 0 |  |  |
|91.smt2                                                      |   20.002s | 22.76MiB| timeout | 0 |  |  |
|143.smt2                                                     |   20.002s | 33.5MiB| timeout | 0 |  |  |
|159.smt2                                                     |   20.002s | 57.088MiB| timeout | 0 |  |  |
|39.smt2                                                      |   20.002s | 23.636MiB| timeout | 0 |  |  |
|23.smt2                                                      |   20.002s | 21.92MiB| timeout | 0 |  |  |
|156.smt2                                                     |   20.002s | 30.396MiB| timeout | 0 |  |  |
|68.smt2                                                      |   20.003s | 23.756MiB| timeout | 0 |  |  |
|73.smt2                                                      |   20.003s | 22.192MiB| timeout | 0 |  |  |
|06.smt2                                                      |   20.003s | 19.748MiB| timeout | 0 |  |  |
|101.smt2                                                     |   20.003s | 21.968MiB| timeout | 0 |  |  |
|102.smt2                                                     |   20.003s | 23.916MiB| timeout | 0 |  |  |
|131.smt2                                                     |   20.003s | 25.176MiB| timeout | 0 |  |  |
|48.smt2                                                      |   20.003s | 22.652MiB| timeout | 0 |  |  |
|28.smt2                                                      |   20.003s | 21.916MiB| timeout | 0 |  |  |
|146.smt2                                                     |   20.003s | 36.204MiB| timeout | 0 |  |  |
|04.smt2                                                      |   20.003s | 21.036MiB| timeout | 0 |  |  |
|67.smt2                                                      |   20.003s | 23.0MiB| timeout | 0 |  |  |
|105.smt2                                                     |   20.003s | 31.816MiB| timeout | 0 |  |  |
|14.smt2                                                      |   20.004s | 21.008MiB| timeout | 0 |  |  |
|119.smt2                                                     |   20.004s | 36.408MiB| timeout | 0 |  |  |
|150.smt2                                                     |   20.004s | 34.636MiB| timeout | 0 |  |  |
|179.smt2                                                     |   20.004s | 146.0MiB| timeout | 0 |  |  |
|138.smt2                                                     |   20.004s | 35.852MiB| timeout | 0 |  |  |
|72.smt2                                                      |   20.004s | 22.768MiB| timeout | 0 |  |  |
|89.smt2                                                      |   20.004s | 22.78MiB| timeout | 0 |  |  |
|22.smt2                                                      |   20.004s | 22.988MiB| timeout | 0 |  |  |
|30.smt2                                                      |   20.004s | 21.636MiB| timeout | 0 |  |  |
|151.smt2                                                     |   20.005s | 33.964MiB| timeout | 0 |  |  |
|92.smt2                                                      |   20.005s | 21.848MiB| timeout | 0 |  |  |
|60.smt2                                                      |   20.005s | 23.668MiB| timeout | 0 |  |  |
|53.smt2                                                      |   20.005s | 23.032MiB| timeout | 0 |  |  |
|43.smt2                                                      |   20.006s | 21.188MiB| timeout | 0 |  |  |
|163.smt2                                                     |   20.006s | 73.996MiB| timeout | 0 |  |  |
|75.smt2                                                      |   20.006s | 22.772MiB| timeout | 0 |  |  |
|59.smt2                                                      |   20.006s | 22.784MiB| timeout | 0 |  |  |
|66.smt2                                                      |   20.007s | 23.864MiB| timeout | 0 |  |  |
|05.smt2                                                      |   20.007s | 22.176MiB| timeout | 0 |  |  |
|125.smt2                                                     |   20.007s | 38.288MiB| timeout | 0 |  |  |
|55.smt2                                                      |   20.007s | 21.94MiB| timeout | 0 |  |  |
|106.smt2                                                     |   20.008s | 34.152MiB| timeout | 0 |  |  |
|178.smt2                                                     |   20.010s | 152.0MiB| timeout | 0 |  |  |
|95.smt2                                                      |   20.010s | 22.776MiB| timeout | 0 |  |  |
|173.smt2                                                     |   20.010s | 138.0MiB| timeout | 0 |  |  |
|15.smt2                                                      |   20.010s | 21.268MiB| timeout | 0 |  |  |
|171.smt2                                                     |   20.010s | 61.08MiB| timeout | 0 |  |  |
|126.smt2                                                     |   20.011s | 36.096MiB| timeout | 0 |  |  |
|166.smt2                                                     |   20.012s | 25.9MiB| timeout | 0 |  |  |
|76.smt2                                                      |   20.080s | 23.864MiB| timeout | 0 |  |  |