# data * SAT 0 * UNSAT 0 * TIMEOUT 2 * UNKNOWN 0 * UNSET 184 * ERROR 184 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: smt-sls
Z3 repo: https://github.com/Z3Prover/z3
Z3 commit: fa22b646aa5965a8e4d79eef54e26707fe9931fc
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: address some build warnings.
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |06.smt2 | 0.014s | 19.54MiB| unset | 139 | | | |12.smt2 | 0.014s | 19.644MiB| unset | 139 | | | |42.smt2 | 0.017s | 20.476MiB| unset | 139 | | | |45.smt2 | 0.017s | 20.048MiB| unset | 139 | | | |44.smt2 | 0.018s | 20.3MiB| unset | 139 | | | |34.smt2 | 0.018s | 20.564MiB| unset | 139 | | | |08.smt2 | 0.019s | 20.244MiB| unset | 139 | | | |09.smt2 | 0.019s | 20.712MiB| unset | 139 | | | |41.smt2 | 0.020s | 20.912MiB| unset | 139 | | | |11.smt2 | 0.020s | 20.628MiB| unset | 139 | | | |15.smt2 | 0.021s | 20.932MiB| unset | 139 | | | |04.smt2 | 0.022s | 20.912MiB| unset | 139 | | | |14.smt2 | 0.023s | 20.816MiB| unset | 139 | | | |07.smt2 | 0.023s | 21.004MiB| unset | 139 | | | |87.smt2 | 0.023s | 20.556MiB| unset | 139 | | | |33.smt2 | 0.024s | 21.168MiB| unset | 139 | | | |02.smt2 | 0.024s | 21.232MiB| unset | 139 | | | |49.smt2 | 0.024s | 21.376MiB| unset | 139 | | | |13.smt2 | 0.024s | 21.452MiB| unset | 139 | | | |73.smt2 | 0.025s | 21.752MiB| unset | 139 | | | |36.smt2 | 0.025s | 21.504MiB| unset | 139 | | | |101.smt2 | 0.025s | 21.616MiB| unset | 139 | | | |21.smt2 | 0.025s | 21.756MiB| unset | 139 | | | |99.smt2 | 0.025s | 21.524MiB| unset | 139 | | | |26.smt2 | 0.025s | 21.796MiB| unset | 139 | | | |28.smt2 | 0.025s | 21.564MiB| unset | 139 | | | |23.smt2 | 0.025s | 21.588MiB| unset | 139 | | | |05.smt2 | 0.026s | 21.612MiB| unset | 139 | | | |19.smt2 | 0.026s | 21.616MiB| unset | 139 | | | |10.smt2 | 0.026s | 21.436MiB| unset | 139 | | | |38.smt2 | 0.026s | 21.624MiB| unset | 139 | | | |51.smt2 | 0.026s | 21.792MiB| unset | 139 | | | |30.smt2 | 0.027s | 21.532MiB| unset | 139 | | | |69.smt2 | 0.028s | 22.48MiB| unset | 139 | | | |86.smt2 | 0.028s | 21.028MiB| unset | 139 | | | |84.smt2 | 0.029s | 20.688MiB| unset | 139 | | | |03.smt2 | 0.029s | 21.552MiB| unset | 139 | | | |98.smt2 | 0.029s | 22.484MiB| unset | 139 | | | |103.smt2 | 0.029s | 22.436MiB| unset | 139 | | | |83.smt2 | 0.030s | 22.168MiB| unset | 139 | | | |25.smt2 | 0.030s | 21.772MiB| unset | 139 | | | |85.smt2 | 0.030s | 21.804MiB| unset | 139 | | | |93.smt2 | 0.030s | 20.772MiB| unset | 139 | | | |72.smt2 | 0.030s | 22.448MiB| unset | 139 | | | |29.smt2 | 0.030s | 22.12MiB| unset | 139 | | | |53.smt2 | 0.030s | 22.524MiB| unset | 139 | | | |17.smt2 | 0.031s | 22.408MiB| unset | 139 | | | |40.smt2 | 0.031s | 22.532MiB| unset | 139 | | | |20.smt2 | 0.031s | 22.432MiB| unset | 139 | | | |47.smt2 | 0.031s | 22.492MiB| unset | 139 | | | |61.smt2 | 0.031s | 22.48MiB| unset | 139 | | | |95.smt2 | 0.031s | 22.552MiB| unset | 139 | | | |65.smt2 | 0.031s | 22.584MiB| unset | 139 | | | |90.smt2 | 0.031s | 23.368MiB| unset | 139 | | | |27.smt2 | 0.031s | 22.564MiB| unset | 139 | | | |100.smt2 | 0.031s | 22.488MiB| unset | 139 | | | |97.smt2 | 0.031s | 22.488MiB| unset | 139 | | | |24.smt2 | 0.032s | 22.44MiB| unset | 139 | | | |77.smt2 | 0.032s | 22.632MiB| unset | 139 | | | |81.smt2 | 0.032s | 22.544MiB| unset | 139 | | | |32.smt2 | 0.032s | 21.56MiB| unset | 139 | | | |75.smt2 | 0.032s | 22.556MiB| unset | 139 | | | |91.smt2 | 0.032s | 22.508MiB| unset | 139 | | | |35.smt2 | 0.032s | 22.036MiB| unset | 139 | | | |59.smt2 | 0.032s | 22.432MiB| unset | 139 | | | |18.smt2 | 0.032s | 22.528MiB| unset | 139 | | | |50.smt2 | 0.033s | 22.516MiB| unset | 139 | | | |63.smt2 | 0.033s | 22.604MiB| unset | 139 | | | |48.smt2 | 0.033s | 22.096MiB| unset | 139 | | | |113.smt2 | 0.033s | 21.032MiB| unset | 139 | | | |55.smt2 | 0.033s | 21.636MiB| unset | 139 | | | |01.smt2 | 0.033s | 22.04MiB| unset | 139 | | | |43.smt2 | 0.034s | 21.02MiB| unset | 139 | | | |71.smt2 | 0.035s | 22.472MiB| unset | 139 | | | |57.smt2 | 0.035s | 23.44MiB| unset | 139 | | | |79.smt2 | 0.036s | 23.312MiB| unset | 139 | | | |92.smt2 | 0.036s | 21.676MiB| unset | 139 | | | |67.smt2 | 0.036s | 22.552MiB| unset | 139 | | | |76.smt2 | 0.037s | 23.336MiB| unset | 139 | | | |16.smt2 | 0.037s | 23.352MiB| unset | 139 | | | |68.smt2 | 0.038s | 23.188MiB| unset | 139 | | | |94.smt2 | 0.038s | 23.384MiB| unset | 139 | | | |31.smt2 | 0.038s | 22.372MiB| unset | 139 | | | |89.smt2 | 0.038s | 22.424MiB| unset | 139 | | | |22.smt2 | 0.038s | 22.36MiB| unset | 139 | | | |66.smt2 | 0.039s | 23.468MiB| unset | 139 | | | |52.smt2 | 0.039s | 23.348MiB| unset | 139 | | | |96.smt2 | 0.039s | 23.416MiB| unset | 139 | | | |37.smt2 | 0.039s | 22.392MiB| unset | 139 | | | |82.smt2 | 0.039s | 23.188MiB| unset | 139 | | | |74.smt2 | 0.039s | 23.52MiB| unset | 139 | | | |54.smt2 | 0.040s | 22.424MiB| unset | 139 | | | |64.smt2 | 0.040s | 23.384MiB| unset | 139 | | | |62.smt2 | 0.040s | 23.48MiB| unset | 139 | | | |80.smt2 | 0.041s | 23.552MiB| unset | 139 | | | |102.smt2 | 0.041s | 23.44MiB| unset | 139 | | | |70.smt2 | 0.041s | 23.264MiB| unset | 139 | | | |58.smt2 | 0.041s | 23.444MiB| unset | 139 | | | |88.smt2 | 0.041s | 23.436MiB| unset | 139 | | | |39.smt2 | 0.042s | 23.436MiB| unset | 139 | | | |60.smt2 | 0.042s | 23.54MiB| unset | 139 | | | |46.smt2 | 0.046s | 23.156MiB| unset | 139 | | | |117.smt2 | 0.047s | 21.772MiB| unset | 139 | | | |107.smt2 | 0.048s | 21.9MiB| unset | 139 | | | |56.smt2 | 0.050s | 24.536MiB| unset | 139 | | | |78.smt2 | 0.050s | 24.232MiB| unset | 139 | | | |118.smt2 | 0.053s | 21.956MiB| unset | 139 | | | |109.smt2 | 0.057s | 22.108MiB| unset | 139 | | | |115.smt2 | 0.093s | 23.556MiB| unset | 139 | | | |104.smt2 | 0.097s | 23.428MiB| unset | 139 | | | |114.smt2 | 0.115s | 29.984MiB| unset | 139 | | | |131.smt2 | 0.118s | 24.908MiB| unset | 139 | | | |111.smt2 | 0.138s | 31.34MiB| unset | 139 | | | |112.smt2 | 0.142s | 31.28MiB| unset | 139 | | | |108.smt2 | 0.145s | 31.4MiB| unset | 139 | | | |124.smt2 | 0.146s | 27.336MiB| unset | 139 | | | |105.smt2 | 0.146s | 31.464MiB| unset | 139 | | | |152.smt2 | 0.150s | 27.44MiB| unset | 139 | | | |164.smt2 | 0.156s | 25.72MiB| unset | 139 | | | |139.smt2 | 0.156s | 29.284MiB| unset | 139 | | | |166.smt2 | 0.159s | 25.712MiB| unset | 139 | | | |162.smt2 | 0.163s | 25.652MiB| unset | 139 | | | |141.smt2 | 0.164s | 33.492MiB| unset | 139 | | | |170.smt2 | 0.164s | 25.66MiB| unset | 139 | | | |157.smt2 | 0.165s | 33.232MiB| unset | 139 | | | |143.smt2 | 0.167s | 33.316MiB| unset | 139 | | | |147.smt2 | 0.174s | 33.608MiB| unset | 139 | | | |110.smt2 | 0.177s | 33.724MiB| unset | 139 | | | |130.smt2 | 0.178s | 33.02MiB| unset | 139 | | | |155.smt2 | 0.178s | 30.976MiB| unset | 139 | | | |156.smt2 | 0.180s | 30.2MiB| unset | 139 | | | |106.smt2 | 0.182s | 33.692MiB| unset | 139 | | | |151.smt2 | 0.183s | 33.604MiB| unset | 139 | | | |136.smt2 | 0.193s | 35.796MiB| unset | 139 | | | |154.smt2 | 0.197s | 35.912MiB| unset | 139 | | | |123.smt2 | 0.198s | 29.516MiB| unset | 139 | | | |122.smt2 | 0.198s | 35.9MiB| unset | 139 | | | |145.smt2 | 0.200s | 35.92MiB| unset | 139 | | | |148.smt2 | 0.201s | 35.16MiB| unset | 139 | | | |150.smt2 | 0.202s | 34.088MiB| unset | 139 | | | |137.smt2 | 0.202s | 35.732MiB| unset | 139 | | | |129.smt2 | 0.202s | 35.472MiB| unset | 139 | | | |140.smt2 | 0.203s | 34.716MiB| unset | 139 | | | |116.smt2 | 0.204s | 35.708MiB| unset | 139 | | | |142.smt2 | 0.205s | 35.124MiB| unset | 139 | | | |133.smt2 | 0.206s | 35.004MiB| unset | 139 | | | |146.smt2 | 0.207s | 35.704MiB| unset | 139 | | | |119.smt2 | 0.208s | 35.768MiB| unset | 139 | | | |127.smt2 | 0.208s | 35.948MiB| unset | 139 | | | |134.smt2 | 0.209s | 35.9MiB| unset | 139 | | | |128.smt2 | 0.212s | 34.048MiB| unset | 139 | | | |126.smt2 | 0.213s | 35.684MiB| unset | 139 | | | |120.smt2 | 0.223s | 35.9MiB| unset | 139 | | | |138.smt2 | 0.223s | 35.428MiB| unset | 139 | | | |153.smt2 | 0.239s | 38.0MiB| unset | 139 | | | |149.smt2 | 0.240s | 36.268MiB| unset | 139 | | | |144.smt2 | 0.242s | 37.96MiB| unset | 139 | | | |135.smt2 | 0.245s | 37.94MiB| unset | 139 | | | |132.smt2 | 0.248s | 37.272MiB| unset | 139 | | | |125.smt2 | 0.252s | 37.916MiB| unset | 139 | | | |121.smt2 | 0.264s | 37.908MiB| unset | 139 | | | |159.smt2 | 0.668s | 56.72MiB| unset | 139 | | | |177.smt2 | 0.669s | 43.62MiB| unset | 139 | | | |160.smt2 | 0.696s | 60.492MiB| unset | 139 | | | |158.smt2 | 0.745s | 59.636MiB| unset | 139 | | | |171.smt2 | 0.800s | 60.4MiB| unset | 139 | | | |165.smt2 | 0.807s | 75.944MiB| unset | 139 | | | |161.smt2 | 0.828s | 72.86MiB| unset | 139 | | | |167.smt2 | 0.865s | 57.948MiB| unset | 139 | | | |168.smt2 | 0.934s | 67.068MiB| unset | 139 | | | |163.smt2 | 0.942s | 73.648MiB| unset | 139 | | | |169.smt2 | 0.975s | 77.932MiB| unset | 139 | | | |174.smt2 | 1.816s | 131.0MiB| unset | 139 | | | |175.smt2 | 1.930s | 131.0MiB| unset | 139 | | | |173.smt2 | 2.032s | 137.0MiB| unset | 139 | | | |179.smt2 | 2.074s | 146.0MiB| unset | 139 | | | |180.smt2 | 2.276s | 146.0MiB| unset | 139 | | | |172.smt2 | 2.440s | 143.0MiB| unset | 139 | | | |176.smt2 | 2.485s | 142.0MiB| unset | 139 | | | |181.smt2 | 2.609s | 153.0MiB| unset | 139 | | | |178.smt2 | 2.839s | 150.0MiB| unset | 139 | | | |183.smt2 | 5.456s | 271.0MiB| unset | 139 | | | |182.smt2 | 5.678s | 271.0MiB| unset | 139 | | | |184.smt2 | 13.012s | 408.0MiB| unset | 139 | | | |185.smt2 | 20.004s | 245.0MiB| timeout | 0 | | | |186.smt2 | 20.006s | 245.0MiB| timeout | 0 | | |