# .

* SAT 2
* UNSAT 0
* TIMEOUT 42
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-1-sequential-smtcomp2025-QF_NRA-timeout20min-no_default_tactic}
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: bb9a55789061a7e3da7e3868f9e388c750e72ad9
Z3 branch: core_min
Z3 options: "-T:1200 -v:0 smt.threads=1 smt.auto_config=false"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_NRA
Z3 commit message: clean up code

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|scrambled29556.smt2                                          |    0.672s | 24.716MiB| sat | 0 |  |  |
|scrambled14368.smt2                                          |   51.371s | 29.288MiB| sat | 0 |  |  |
|scrambled100912.smt2                                         | 1200.012s | 35.892MiB| timeout | 0 |  |  |
|scrambled42946.smt2                                          | 1200.013s | 90.02MiB| timeout | 0 |  |  |
|scrambled94319.smt2                                          | 1200.014s | 37.088MiB| timeout | 0 |  |  |
|scrambled117944.smt2                                         | 1200.014s | 38.36MiB| timeout | 0 |  |  |
|scrambled82241.smt2                                          | 1200.016s | 67.288MiB| timeout | 0 |  |  |
|scrambled58292.smt2                                          | 1200.017s | 180.0MiB| timeout | 0 |  |  |
|scrambled112144.smt2                                         | 1200.018s | 43.236MiB| timeout | 0 |  |  |
|scrambled18831.smt2                                          | 1200.020s | 204.0MiB| timeout | 0 |  |  |
|scrambled7586.smt2                                           | 1200.020s | 159.0MiB| timeout | 0 |  |  |
|scrambled21647.smt2                                          | 1200.021s | 110.0MiB| timeout | 0 |  |  |
|scrambled74869.smt2                                          | 1200.029s | 72.484MiB| timeout | 0 |  |  |
|scrambled14880.smt2                                          | 1200.029s | 34.6MiB| timeout | 0 |  |  |
|scrambled34121.smt2                                          | 1200.030s | 30.896MiB| timeout | 0 |  |  |
|scrambled7923.smt2                                           | 1200.030s | 60.048MiB| timeout | 0 |  |  |
|scrambled36539.smt2                                          | 1200.031s | 63.38MiB| timeout | 0 |  |  |
|scrambled54263.smt2                                          | 1200.033s | 89.328MiB| timeout | 0 |  |  |
|scrambled73220.smt2                                          | 1200.033s | 40.236MiB| timeout | 0 |  |  |
|scrambled94768.smt2                                          | 1200.035s | 210.0MiB| timeout | 0 |  |  |
|scrambled80728.smt2                                          | 1200.036s | 42.056MiB| timeout | 0 |  |  |
|scrambled65757.smt2                                          | 1200.037s | 233.0MiB| timeout | 0 |  |  |
|scrambled112083.smt2                                         | 1200.037s | 34.52MiB| timeout | 0 |  |  |
|scrambled28630.smt2                                          | 1200.037s | 49.884MiB| timeout | 0 |  |  |
|scrambled99534.smt2                                          | 1200.038s | 182.0MiB| timeout | 0 |  |  |
|scrambled32269.smt2                                          | 1200.038s | 94.688MiB| timeout | 0 |  |  |
|scrambled124828.smt2                                         | 1200.039s | 102.0MiB| timeout | 0 |  |  |
|scrambled22492.smt2                                          | 1200.040s | 119.0MiB| timeout | 0 |  |  |
|scrambled118224.smt2                                         | 1200.040s | 141.0MiB| timeout | 0 |  |  |
|scrambled85895.smt2                                          | 1200.052s | 459.0MiB| timeout | 0 |  |  |
|scrambled32701.smt2                                          | 1200.053s | 125.0MiB| timeout | 0 |  |  |
|scrambled117334.smt2                                         | 1200.063s | 570.0MiB| timeout | 0 |  |  |
|scrambled27426.smt2                                          | 1200.081s | 927.0MiB| timeout | 0 |  |  |
|scrambled78428.smt2                                          | 1200.082s | 772.0MiB| timeout | 0 |  |  |
|scrambled70990.smt2                                          | 1200.086s | 656.0MiB| timeout | 0 |  |  |
|scrambled6476.smt2                                           | 1200.088s | 1023.0MiB| timeout | 0 |  |  |
|scrambled121780.smt2                                         | 1200.094s | 1051.0MiB| timeout | 0 |  |  |
|scrambled91241.smt2                                          | 1200.095s | 753.0MiB| timeout | 0 |  |  |
|scrambled60239.smt2                                          | 1200.096s | 737.0MiB| timeout | 0 |  |  |
|scrambled41575.smt2                                          | 1200.105s | 835.0MiB| timeout | 0 |  |  |
|scrambled61896.smt2                                          | 1200.108s | 711.0MiB| timeout | 0 |  |  |
|scrambled14016.smt2                                          | 1200.109s | 931.0MiB| timeout | 0 |  |  |
|scrambled5797.smt2                                           | 1200.133s | 1369.0MiB| timeout | 0 |  |  |
|scrambled114923.smt2                                         | 1200.202s | 1982.0MiB| timeout | 0 |  |  |