# .

* SAT 3
* UNSAT 0
* TIMEOUT 41
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-1-sequential-smtcomp2025-QF_LIA-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_LIA
Z3 commit message: clean up code

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|scrambled118793.smt2                                         |  158.233s | 104.0MiB| sat | 0 |  |  |
|scrambled25238.smt2                                          |  836.220s | 639.0MiB| sat | 0 |  |  |
|scrambled125888.smt2                                         |  882.210s | 177.0MiB| sat | 0 |  |  |
|scrambled79766.smt2                                          | 1200.015s | 42.304MiB| timeout | 0 |  |  |
|scrambled3854.smt2                                           | 1200.016s | 42.512MiB| timeout | 0 |  |  |
|scrambled1417.smt2                                           | 1200.018s | 67.732MiB| timeout | 0 |  |  |
|scrambled45952.smt2                                          | 1200.020s | 41.54MiB| timeout | 0 |  |  |
|scrambled125827.smt2                                         | 1200.028s | 100.0MiB| timeout | 0 |  |  |
|scrambled103783.smt2                                         | 1200.033s | 42.836MiB| timeout | 0 |  |  |
|scrambled65181.smt2                                          | 1200.034s | 42.308MiB| timeout | 0 |  |  |
|scrambled59713.smt2                                          | 1200.034s | 41.584MiB| timeout | 0 |  |  |
|scrambled79867.smt2                                          | 1200.035s | 41.984MiB| timeout | 0 |  |  |
|scrambled95803.smt2                                          | 1200.036s | 234.0MiB| timeout | 0 |  |  |
|scrambled39514.smt2                                          | 1200.040s | 74.912MiB| timeout | 0 |  |  |
|scrambled32836.smt2                                          | 1200.049s | 223.0MiB| timeout | 0 |  |  |
|scrambled20101.smt2                                          | 1200.055s | 171.0MiB| timeout | 0 |  |  |
|scrambled128128.smt2                                         | 1200.061s | 426.0MiB| timeout | 0 |  |  |
|scrambled128874.smt2                                         | 1200.070s | 454.0MiB| timeout | 0 |  |  |
|scrambled55777.smt2                                          | 1200.082s | 299.0MiB| timeout | 0 |  |  |
|scrambled44911.smt2                                          | 1200.088s | 448.0MiB| timeout | 0 |  |  |
|scrambled51053.smt2                                          | 1200.090s | 342.0MiB| timeout | 0 |  |  |
|scrambled72668.smt2                                          | 1200.093s | 485.0MiB| timeout | 0 |  |  |
|scrambled131241.smt2                                         | 1200.094s | 511.0MiB| timeout | 0 |  |  |
|scrambled128732.smt2                                         | 1200.114s | 475.0MiB| timeout | 0 |  |  |
|scrambled7741.smt2                                           | 1200.123s | 524.0MiB| timeout | 0 |  |  |
|scrambled40621.smt2                                          | 1200.132s | 938.0MiB| timeout | 0 |  |  |
|scrambled119331.smt2                                         | 1200.134s | 595.0MiB| timeout | 0 |  |  |
|scrambled61922.smt2                                          | 1200.212s | 1246.0MiB| timeout | 0 |  |  |
|scrambled107115.smt2                                         | 1200.285s | 1924.0MiB| timeout | 0 |  |  |
|scrambled27843.smt2                                          | 1200.323s | 2300.0MiB| timeout | 0 |  |  |
|scrambled107826.smt2                                         | 1200.388s | 3473.0MiB| timeout | 0 |  |  |
|scrambled19335.smt2                                          | 1200.420s | 3326.0MiB| timeout | 0 |  |  |
|scrambled43577.smt2                                          | 1200.475s | 4155.0MiB| timeout | 0 |  |  |
|scrambled68944.smt2                                          | 1200.485s | 4711.0MiB| timeout | 0 |  |  |
|scrambled75189.smt2                                          | 1200.495s | 4292.0MiB| timeout | 0 |  |  |
|scrambled111627.smt2                                         | 1200.580s | 5771.0MiB| timeout | 0 |  |  |
|scrambled108840.smt2                                         | 1200.596s | 5487.0MiB| timeout | 0 |  |  |
|scrambled79760.smt2                                          | 1200.606s | 5912.0MiB| timeout | 0 |  |  |
|scrambled55680.smt2                                          | 1200.641s | 6012.0MiB| timeout | 0 |  |  |
|scrambled12042.smt2                                          | 1200.654s | 6117.0MiB| timeout | 0 |  |  |
|scrambled4299.smt2                                           | 1200.664s | 6773.0MiB| timeout | 0 |  |  |
|scrambled94658.smt2                                          | 1200.705s | 6749.0MiB| timeout | 0 |  |  |
|scrambled102166.smt2                                         | 1200.722s | 7338.0MiB| timeout | 0 |  |  |
|scrambled4198.smt2                                           | 1200.738s | 7116.0MiB| timeout | 0 |  |  |