# .

* 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-auto_config}
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=true"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_NRA
Z3 commit message: clean up code

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|scrambled14368.smt2                                          |    5.838s | 25.904MiB| sat | 0 |  |  |
|scrambled29556.smt2                                          |    6.158s | 28.352MiB| sat | 0 |  |  |
|scrambled18831.smt2                                          | 1200.012s | 33.1MiB| timeout | 0 |  |  |
|scrambled82241.smt2                                          | 1200.012s | 29.824MiB| timeout | 0 |  |  |
|scrambled7586.smt2                                           | 1200.012s | 29.272MiB| timeout | 0 |  |  |
|scrambled99534.smt2                                          | 1200.013s | 29.092MiB| timeout | 0 |  |  |
|scrambled34121.smt2                                          | 1200.015s | 28.656MiB| timeout | 0 |  |  |
|scrambled112144.smt2                                         | 1200.015s | 33.652MiB| timeout | 0 |  |  |
|scrambled118224.smt2                                         | 1200.015s | 42.504MiB| timeout | 0 |  |  |
|scrambled32269.smt2                                          | 1200.015s | 27.788MiB| timeout | 0 |  |  |
|scrambled100912.smt2                                         | 1200.016s | 33.128MiB| timeout | 0 |  |  |
|scrambled7923.smt2                                           | 1200.017s | 28.464MiB| timeout | 0 |  |  |
|scrambled28630.smt2                                          | 1200.017s | 29.148MiB| timeout | 0 |  |  |
|scrambled58292.smt2                                          | 1200.018s | 43.344MiB| timeout | 0 |  |  |
|scrambled74869.smt2                                          | 1200.033s | 31.512MiB| timeout | 0 |  |  |
|scrambled42946.smt2                                          | 1200.034s | 30.572MiB| timeout | 0 |  |  |
|scrambled54263.smt2                                          | 1200.034s | 29.016MiB| timeout | 0 |  |  |
|scrambled112083.smt2                                         | 1200.034s | 31.636MiB| timeout | 0 |  |  |
|scrambled36539.smt2                                          | 1200.035s | 35.904MiB| timeout | 0 |  |  |
|scrambled14880.smt2                                          | 1200.035s | 28.832MiB| timeout | 0 |  |  |
|scrambled117944.smt2                                         | 1200.035s | 31.38MiB| timeout | 0 |  |  |
|scrambled80728.smt2                                          | 1200.036s | 32.928MiB| timeout | 0 |  |  |
|scrambled117334.smt2                                         | 1200.036s | 34.06MiB| timeout | 0 |  |  |
|scrambled73220.smt2                                          | 1200.037s | 33.696MiB| timeout | 0 |  |  |
|scrambled21647.smt2                                          | 1200.037s | 33.368MiB| timeout | 0 |  |  |
|scrambled14016.smt2                                          | 1200.045s | 338.0MiB| timeout | 0 |  |  |
|scrambled94768.smt2                                          | 1200.045s | 27.292MiB| timeout | 0 |  |  |
|scrambled60239.smt2                                          | 1200.051s | 548.0MiB| timeout | 0 |  |  |
|scrambled27426.smt2                                          | 1200.055s | 753.0MiB| timeout | 0 |  |  |
|scrambled41575.smt2                                          | 1200.075s | 495.0MiB| timeout | 0 |  |  |
|scrambled70990.smt2                                          | 1200.076s | 494.0MiB| timeout | 0 |  |  |
|scrambled32701.smt2                                          | 1200.077s | 321.0MiB| timeout | 0 |  |  |
|scrambled121780.smt2                                         | 1200.080s | 974.0MiB| timeout | 0 |  |  |
|scrambled124828.smt2                                         | 1200.082s | 725.0MiB| timeout | 0 |  |  |
|scrambled91241.smt2                                          | 1200.086s | 742.0MiB| timeout | 0 |  |  |
|scrambled22492.smt2                                          | 1200.087s | 549.0MiB| timeout | 0 |  |  |
|scrambled6476.smt2                                           | 1200.088s | 969.0MiB| timeout | 0 |  |  |
|scrambled85895.smt2                                          | 1200.101s | 559.0MiB| timeout | 0 |  |  |
|scrambled61896.smt2                                          | 1200.106s | 709.0MiB| timeout | 0 |  |  |
|scrambled78428.smt2                                          | 1200.110s | 711.0MiB| timeout | 0 |  |  |
|scrambled5797.smt2                                           | 1200.173s | 1799.0MiB| timeout | 0 |  |  |
|scrambled114923.smt2                                         | 1200.186s | 1907.0MiB| timeout | 0 |  |  |
|scrambled94319.smt2                                          | 1200.267s | 2643.0MiB| timeout | 0 |  |  |
|scrambled65757.smt2                                          | 1201.842s | 21.546GiB| timeout | 0 |  |  |