# .

* 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}
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: bb9a55789061a7e3da7e3868f9e388c750e72ad9
Z3 branch: core_min
Z3 options: "-T:1200 -v:0 smt.threads=1 tactic.default_tactic=smt 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.794s | 30.5MiB| sat | 0 |  |  |
|scrambled14368.smt2                                          |    9.803s | 26.768MiB| sat | 0 |  |  |
|scrambled82241.smt2                                          | 1200.014s | 29.824MiB| timeout | 0 |  |  |
|scrambled7586.smt2                                           | 1200.014s | 28.268MiB| timeout | 0 |  |  |
|scrambled58292.smt2                                          | 1200.015s | 36.552MiB| timeout | 0 |  |  |
|scrambled54263.smt2                                          | 1200.015s | 30.884MiB| timeout | 0 |  |  |
|scrambled124828.smt2                                         | 1200.016s | 43.828MiB| timeout | 0 |  |  |
|scrambled74869.smt2                                          | 1200.016s | 29.54MiB| timeout | 0 |  |  |
|scrambled94319.smt2                                          | 1200.019s | 30.532MiB| timeout | 0 |  |  |
|scrambled28630.smt2                                          | 1200.020s | 31.32MiB| timeout | 0 |  |  |
|scrambled32269.smt2                                          | 1200.021s | 27.148MiB| timeout | 0 |  |  |
|scrambled18831.smt2                                          | 1200.022s | 31.436MiB| timeout | 0 |  |  |
|scrambled80728.smt2                                          | 1200.031s | 30.992MiB| timeout | 0 |  |  |
|scrambled7923.smt2                                           | 1200.032s | 27.9MiB| timeout | 0 |  |  |
|scrambled99534.smt2                                          | 1200.032s | 31.672MiB| timeout | 0 |  |  |
|scrambled117944.smt2                                         | 1200.032s | 29.012MiB| timeout | 0 |  |  |
|scrambled34121.smt2                                          | 1200.033s | 31.5MiB| timeout | 0 |  |  |
|scrambled14880.smt2                                          | 1200.033s | 30.436MiB| timeout | 0 |  |  |
|scrambled112083.smt2                                         | 1200.033s | 28.34MiB| timeout | 0 |  |  |
|scrambled100912.smt2                                         | 1200.034s | 30.808MiB| timeout | 0 |  |  |
|scrambled112144.smt2                                         | 1200.034s | 36.66MiB| timeout | 0 |  |  |
|scrambled117334.smt2                                         | 1200.034s | 57.172MiB| timeout | 0 |  |  |
|scrambled42946.smt2                                          | 1200.035s | 29.388MiB| timeout | 0 |  |  |
|scrambled73220.smt2                                          | 1200.035s | 33.028MiB| timeout | 0 |  |  |
|scrambled22492.smt2                                          | 1200.038s | 49.788MiB| timeout | 0 |  |  |
|scrambled21647.smt2                                          | 1200.040s | 56.296MiB| timeout | 0 |  |  |
|scrambled118224.smt2                                         | 1200.041s | 57.928MiB| timeout | 0 |  |  |
|scrambled32701.smt2                                          | 1200.043s | 128.0MiB| timeout | 0 |  |  |
|scrambled94768.smt2                                          | 1200.052s | 365.0MiB| timeout | 0 |  |  |
|scrambled27426.smt2                                          | 1200.056s | 753.0MiB| timeout | 0 |  |  |
|scrambled41575.smt2                                          | 1200.087s | 495.0MiB| timeout | 0 |  |  |
|scrambled85895.smt2                                          | 1200.091s | 410.0MiB| timeout | 0 |  |  |
|scrambled91241.smt2                                          | 1200.091s | 742.0MiB| timeout | 0 |  |  |
|scrambled70990.smt2                                          | 1200.097s | 494.0MiB| timeout | 0 |  |  |
|scrambled6476.smt2                                           | 1200.098s | 969.0MiB| timeout | 0 |  |  |
|scrambled65757.smt2                                          | 1200.103s | 707.0MiB| timeout | 0 |  |  |
|scrambled78428.smt2                                          | 1200.110s | 711.0MiB| timeout | 0 |  |  |
|scrambled121780.smt2                                         | 1200.120s | 974.0MiB| timeout | 0 |  |  |
|scrambled60239.smt2                                          | 1200.129s | 548.0MiB| timeout | 0 |  |  |
|scrambled36539.smt2                                          | 1200.151s | 681.0MiB| timeout | 0 |  |  |
|scrambled61896.smt2                                          | 1200.164s | 710.0MiB| timeout | 0 |  |  |
|scrambled14016.smt2                                          | 1200.180s | 874.0MiB| timeout | 0 |  |  |
|scrambled5797.smt2                                           | 1200.316s | 1787.0MiB| timeout | 0 |  |  |
|scrambled114923.smt2                                         | 1200.496s | 2703.0MiB| timeout | 0 |  |  |