# .

* SAT 0
* UNSAT 0
* TIMEOUT 44
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for SMTS
-
Job description: 
Job tag: SMTS_z3-threads-8-smtcomp2025-QF_LIA-timeout_20min
Runner: rise-runner-2
SMTS repo: ilanashapiro/SMTS
SMTS commit: bd82256ff952d2c8d799b038a0faa343d2805eb2
SMTS branch: master
SMTS options: "-oz 8 -p -l"
SMTS solver mode: z3
SMTS timeout: 1260
SMTS inputs: inputs/smt_comp_2025_parallel/QF_LIA
SMTS commit message: wire OpenSMTZ3 hybrid solver into server launcher

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|scrambled39514.smt2                                          | 1260.018s | 18.472MiB| timeout | 0 |  |  |
|scrambled95803.smt2                                          | 1260.020s | 13.832MiB| timeout | 0 |  |  |
|scrambled45952.smt2                                          | 1260.021s | 18.612MiB| timeout | 0 |  |  |
|scrambled111627.smt2                                         | 1260.023s | 55.208MiB| timeout | 0 |  |  |
|scrambled72668.smt2                                          | 1260.023s | 15.012MiB| timeout | 0 |  |  |
|scrambled128732.smt2                                         | 1260.023s | 14.648MiB| timeout | 0 |  |  |
|scrambled61922.smt2                                          | 1260.024s | 24.14MiB| timeout | 0 |  |  |
|scrambled128128.smt2                                         | 1260.024s | 14.28MiB| timeout | 0 |  |  |
|scrambled44911.smt2                                          | 1260.024s | 15.264MiB| timeout | 0 |  |  |
|scrambled27843.smt2                                          | 1260.026s | 40.752MiB| timeout | 0 |  |  |
|scrambled125827.smt2                                         | 1260.027s | 13.604MiB| timeout | 0 |  |  |
|scrambled40621.smt2                                          | 1260.028s | 17.956MiB| timeout | 0 |  |  |
|scrambled125888.smt2                                         | 1260.029s | 14.292MiB| timeout | 0 |  |  |
|scrambled94658.smt2                                          | 1260.029s | 98.0MiB| timeout | 0 |  |  |
|scrambled59713.smt2                                          | 1260.029s | 19.28MiB| timeout | 0 |  |  |
|scrambled7741.smt2                                           | 1260.030s | 16.312MiB| timeout | 0 |  |  |
|scrambled79760.smt2                                          | 1260.030s | 51.528MiB| timeout | 0 |  |  |
|scrambled107826.smt2                                         | 1260.031s | 50.188MiB| timeout | 0 |  |  |
|scrambled51053.smt2                                          | 1260.032s | 25.896MiB| timeout | 0 |  |  |
|scrambled131241.smt2                                         | 1260.032s | 15.144MiB| timeout | 0 |  |  |
|scrambled55680.smt2                                          | 1260.033s | 70.376MiB| timeout | 0 |  |  |
|scrambled118793.smt2                                         | 1260.033s | 14.068MiB| timeout | 0 |  |  |
|scrambled107115.smt2                                         | 1260.033s | 26.816MiB| timeout | 0 |  |  |
|scrambled65181.smt2                                          | 1260.033s | 20.272MiB| timeout | 0 |  |  |
|scrambled119331.smt2                                         | 1260.033s | 17.38MiB| timeout | 0 |  |  |
|scrambled68944.smt2                                          | 1260.034s | 48.732MiB| timeout | 0 |  |  |
|scrambled12042.smt2                                          | 1260.035s | 99.0MiB| timeout | 0 |  |  |
|scrambled79867.smt2                                          | 1260.035s | 19.572MiB| timeout | 0 |  |  |
|scrambled4299.smt2                                           | 1260.035s | 67.576MiB| timeout | 0 |  |  |
|scrambled108840.smt2                                         | 1260.035s | 66.048MiB| timeout | 0 |  |  |
|scrambled32836.smt2                                          | 1260.036s | 15.584MiB| timeout | 0 |  |  |
|scrambled19335.smt2                                          | 1260.036s | 53.568MiB| timeout | 0 |  |  |
|scrambled75189.smt2                                          | 1260.037s | 49.676MiB| timeout | 0 |  |  |
|scrambled128874.smt2                                         | 1260.037s | 15.284MiB| timeout | 0 |  |  |
|scrambled103783.smt2                                         | 1260.051s | 18.16MiB| timeout | 0 |  |  |
|scrambled20101.smt2                                          | 1260.052s | 13.408MiB| timeout | 0 |  |  |
|scrambled55777.smt2                                          | 1260.052s | 15.916MiB| timeout | 0 |  |  |
|scrambled25238.smt2                                          | 1260.053s | 15.412MiB| timeout | 0 |  |  |
|scrambled3854.smt2                                           | 1260.058s | 17.272MiB| timeout | 0 |  |  |
|scrambled43577.smt2                                          | 1260.059s | 56.504MiB| timeout | 0 |  |  |
|scrambled4198.smt2                                           | 1260.059s | 98.872MiB| timeout | 0 |  |  |
|scrambled1417.smt2                                           | 1260.060s | 13.308MiB| timeout | 0 |  |  |
|scrambled102166.smt2                                         | 1260.062s | 70.912MiB| timeout | 0 |  |  |
|scrambled79766.smt2                                          | 1260.063s | 18.676MiB| timeout | 0 |  |  |
