# .

* 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-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.821s | 25.912MiB| sat | 0 |  |  |
|scrambled29556.smt2                                          |    6.278s | 28.336MiB| sat | 0 |  |  |
|scrambled7586.smt2                                           | 1200.012s | 29.192MiB| timeout | 0 |  |  |
|scrambled99534.smt2                                          | 1200.013s | 29.392MiB| timeout | 0 |  |  |
|scrambled73220.smt2                                          | 1200.013s | 33.836MiB| timeout | 0 |  |  |
|scrambled42946.smt2                                          | 1200.014s | 30.64MiB| timeout | 0 |  |  |
|scrambled58292.smt2                                          | 1200.015s | 43.212MiB| timeout | 0 |  |  |
|scrambled14880.smt2                                          | 1200.015s | 28.932MiB| timeout | 0 |  |  |
|scrambled34121.smt2                                          | 1200.016s | 28.42MiB| timeout | 0 |  |  |
|scrambled82241.smt2                                          | 1200.016s | 30.232MiB| timeout | 0 |  |  |
|scrambled117334.smt2                                         | 1200.016s | 33.848MiB| timeout | 0 |  |  |
|scrambled118224.smt2                                         | 1200.024s | 42.476MiB| timeout | 0 |  |  |
|scrambled112144.smt2                                         | 1200.025s | 33.76MiB| timeout | 0 |  |  |
|scrambled28630.smt2                                          | 1200.026s | 29.076MiB| timeout | 0 |  |  |
|scrambled74869.smt2                                          | 1200.029s | 31.244MiB| timeout | 0 |  |  |
|scrambled32269.smt2                                          | 1200.030s | 27.596MiB| timeout | 0 |  |  |
|scrambled100912.smt2                                         | 1200.032s | 33.048MiB| timeout | 0 |  |  |
|scrambled21647.smt2                                          | 1200.032s | 33.564MiB| timeout | 0 |  |  |
|scrambled36539.smt2                                          | 1200.033s | 35.864MiB| timeout | 0 |  |  |
|scrambled112083.smt2                                         | 1200.033s | 31.596MiB| timeout | 0 |  |  |
|scrambled54263.smt2                                          | 1200.034s | 29.044MiB| timeout | 0 |  |  |
|scrambled94768.smt2                                          | 1200.035s | 27.32MiB| timeout | 0 |  |  |
|scrambled7923.smt2                                           | 1200.035s | 28.464MiB| timeout | 0 |  |  |
|scrambled80728.smt2                                          | 1200.036s | 32.852MiB| timeout | 0 |  |  |
|scrambled18831.smt2                                          | 1200.037s | 32.804MiB| timeout | 0 |  |  |
|scrambled117944.smt2                                         | 1200.037s | 31.348MiB| timeout | 0 |  |  |
|scrambled27426.smt2                                          | 1200.042s | 753.0MiB| timeout | 0 |  |  |
|scrambled61896.smt2                                          | 1200.059s | 545.0MiB| timeout | 0 |  |  |
|scrambled22492.smt2                                          | 1200.063s | 549.0MiB| timeout | 0 |  |  |
|scrambled32701.smt2                                          | 1200.063s | 314.0MiB| timeout | 0 |  |  |
|scrambled41575.smt2                                          | 1200.068s | 495.0MiB| timeout | 0 |  |  |
|scrambled70990.smt2                                          | 1200.072s | 494.0MiB| timeout | 0 |  |  |
|scrambled14016.smt2                                          | 1200.073s | 339.0MiB| timeout | 0 |  |  |
|scrambled6476.smt2                                           | 1200.080s | 968.0MiB| timeout | 0 |  |  |
|scrambled121780.smt2                                         | 1200.081s | 974.0MiB| timeout | 0 |  |  |
|scrambled85895.smt2                                          | 1200.088s | 560.0MiB| timeout | 0 |  |  |
|scrambled78428.smt2                                          | 1200.089s | 711.0MiB| timeout | 0 |  |  |
|scrambled60239.smt2                                          | 1200.089s | 548.0MiB| timeout | 0 |  |  |
|scrambled91241.smt2                                          | 1200.090s | 742.0MiB| timeout | 0 |  |  |
|scrambled124828.smt2                                         | 1200.100s | 728.0MiB| timeout | 0 |  |  |
|scrambled5797.smt2                                           | 1200.187s | 1799.0MiB| timeout | 0 |  |  |
|scrambled114923.smt2                                         | 1200.210s | 1907.0MiB| timeout | 0 |  |  |
|scrambled94319.smt2                                          | 1200.260s | 2642.0MiB| timeout | 0 |  |  |
|scrambled65757.smt2                                          | 1201.731s | 21.545GiB| timeout | 0 |  |  |