# .

* SAT 14
* UNSAT 0
* TIMEOUT 30
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for SMTS
-
Job description: 
Job tag: SMTS_opensmt-threads-8-smtcomp2025-QF_LIA-timeout_20min
Runner: rise-runner-2
SMTS repo: ilanashapiro/SMTS
SMTS commit: 6fbca23b525b880620030507e997cbbe14ae1a90
SMTS branch: master
SMTS options: "-o 8 -p -l"
SMTS solver mode: opensmt
SMTS timeout: 1200
SMTS inputs: inputs/smt_comp_2025_parallel/QF_LIA
SMTS commit message: fix more semantic bugs between SMTS+Z3 and the original SMTS+OpenSMT2

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|scrambled125827.smt2                                         |    1.808s | 238.0MiB| sat | 0 |  |  |
|scrambled118793.smt2                                         |    4.500s | 241.0MiB| sat | 0 |  |  |
|scrambled125888.smt2                                         |    6.000s | 328.0MiB| sat | 0 |  |  |
|scrambled131241.smt2                                         |   44.312s | 1322.0MiB| sat | 0 |  |  |
|scrambled25238.smt2                                          |   45.626s | 1410.0MiB| sat | 0 |  |  |
|scrambled72668.smt2                                          |   66.485s | 1071.0MiB| sat | 0 |  |  |
|scrambled44911.smt2                                          |   79.269s | 1120.0MiB| sat | 0 |  |  |
|scrambled20101.smt2                                          |   86.563s | 678.0MiB| sat | 0 |  |  |
|scrambled128874.smt2                                         |  152.492s | 988.0MiB| sat | 0 |  |  |
|scrambled128128.smt2                                         |  234.501s | 1722.0MiB| sat | 0 |  |  |
|scrambled7741.smt2                                           |  257.212s | 1882.0MiB| sat | 0 |  |  |
|scrambled32836.smt2                                          |  313.768s | 1252.0MiB| sat | 0 |  |  |
|scrambled95803.smt2                                          |  327.807s | 1147.0MiB| sat | 0 |  |  |
|scrambled119331.smt2                                         |  809.427s | 2341.0MiB| sat | 0 |  |  |
|scrambled55777.smt2                                          | 1200.044s | 2289.0MiB| timeout | 0 |  |  |
|scrambled1417.smt2                                           | 1200.045s | 3671.0MiB| timeout | 0 |  |  |
|scrambled111627.smt2                                         | 1200.046s | 16.313GiB| timeout | 0 |  |  |
|scrambled39514.smt2                                          | 1200.055s | 47.367GiB| timeout | 0 |  |  |
|scrambled79766.smt2                                          | 1200.055s | 45.12GiB| timeout | 0 |  |  |
|scrambled68944.smt2                                          | 1200.056s | 10.413GiB| timeout | 0 |  |  |
|scrambled102166.smt2                                         | 1200.057s | 14.652GiB| timeout | 0 |  |  |
|scrambled40621.smt2                                          | 1200.058s | 2544.0MiB| timeout | 0 |  |  |
|scrambled55680.smt2                                          | 1200.058s | 21.426GiB| timeout | 0 |  |  |
|scrambled61922.smt2                                          | 1200.060s | 11.723GiB| timeout | 0 |  |  |
|scrambled107826.smt2                                         | 1200.061s | 14.153GiB| timeout | 0 |  |  |
|scrambled12042.smt2                                          | 1200.063s | 21.698GiB| timeout | 0 |  |  |
|scrambled108840.smt2                                         | 1200.067s | 14.578GiB| timeout | 0 |  |  |
|scrambled51053.smt2                                          | 1200.068s | 4843.0MiB| timeout | 0 |  |  |
|scrambled43577.smt2                                          | 1200.068s | 12.49GiB| timeout | 0 |  |  |
|scrambled27843.smt2                                          | 1200.070s | 9421.0MiB| timeout | 0 |  |  |
|scrambled79760.smt2                                          | 1200.073s | 10.472GiB| timeout | 0 |  |  |
|scrambled59713.smt2                                          | 1200.078s | 45.778GiB| timeout | 0 |  |  |
|scrambled4198.smt2                                           | 1200.078s | 23.985GiB| timeout | 0 |  |  |
|scrambled75189.smt2                                          | 1200.080s | 11.496GiB| timeout | 0 |  |  |
|scrambled19335.smt2                                          | 1200.085s | 16.324GiB| timeout | 0 |  |  |
|scrambled4299.smt2                                           | 1200.087s | 11.362GiB| timeout | 0 |  |  |
|scrambled79867.smt2                                          | 1200.092s | 54.193GiB| timeout | 0 |  |  |
|scrambled65181.smt2                                          | 1200.101s | 48.493GiB| timeout | 0 |  |  |
|scrambled45952.smt2                                          | 1200.101s | 54.575GiB| timeout | 0 |  |  |
|scrambled128732.smt2                                         | 1200.112s | 2426.0MiB| timeout | 0 |  |  |
|scrambled3854.smt2                                           | 1200.133s | 50.445GiB| timeout | 0 |  |  |
|scrambled94658.smt2                                          | 1200.134s | 19.903GiB| timeout | 0 |  |  |
|scrambled103783.smt2                                         | 1200.147s | 51.192GiB| timeout | 0 |  |  |
|scrambled107115.smt2                                         | 1200.259s | 15.772GiB| timeout | 0 |  |  |