# .

* 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-test
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: 61
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 | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|scrambled119331.smt2                                         |   61.018s | 17.528MiB| timeout | 0 |  |  |
|scrambled45952.smt2                                          |   61.021s | 19.836MiB| timeout | 0 |  |  |
|scrambled55777.smt2                                          |   61.021s | 14.712MiB| timeout | 0 |  |  |
|scrambled55680.smt2                                          |   61.024s | 79.192MiB| timeout | 0 |  |  |
|scrambled107115.smt2                                         |   61.024s | 26.816MiB| timeout | 0 |  |  |
|scrambled43577.smt2                                          |   61.025s | 55.96MiB| timeout | 0 |  |  |
|scrambled20101.smt2                                          |   61.026s | 12.636MiB| timeout | 0 |  |  |
|scrambled128128.smt2                                         |   61.029s | 14.716MiB| timeout | 0 |  |  |
|scrambled125888.smt2                                         |   61.030s | 13.788MiB| timeout | 0 |  |  |
|scrambled125827.smt2                                         |   61.031s | 13.6MiB| timeout | 0 |  |  |
|scrambled65181.smt2                                          |   61.031s | 18.616MiB| timeout | 0 |  |  |
|scrambled128732.smt2                                         |   61.031s | 14.528MiB| timeout | 0 |  |  |
|scrambled95803.smt2                                          |   61.032s | 14.436MiB| timeout | 0 |  |  |
|scrambled72668.smt2                                          |   61.032s | 14.384MiB| timeout | 0 |  |  |
|scrambled44911.smt2                                          |   61.032s | 15.592MiB| timeout | 0 |  |  |
|scrambled39514.smt2                                          |   61.033s | 18.256MiB| timeout | 0 |  |  |
|scrambled1417.smt2                                           |   61.033s | 12.348MiB| timeout | 0 |  |  |
|scrambled40621.smt2                                          |   61.033s | 17.86MiB| timeout | 0 |  |  |
|scrambled118793.smt2                                         |   61.033s | 13.64MiB| timeout | 0 |  |  |
|scrambled7741.smt2                                           |   61.033s | 16.44MiB| timeout | 0 |  |  |
|scrambled79766.smt2                                          |   61.033s | 18.728MiB| timeout | 0 |  |  |
|scrambled103783.smt2                                         |   61.033s | 18.052MiB| timeout | 0 |  |  |
|scrambled131241.smt2                                         |   61.033s | 14.788MiB| timeout | 0 |  |  |
|scrambled61922.smt2                                          |   61.034s | 24.024MiB| timeout | 0 |  |  |
|scrambled107826.smt2                                         |   61.034s | 57.34MiB| timeout | 0 |  |  |
|scrambled27843.smt2                                          |   61.034s | 42.664MiB| timeout | 0 |  |  |
|scrambled59713.smt2                                          |   61.034s | 18.92MiB| timeout | 0 |  |  |
|scrambled51053.smt2                                          |   61.035s | 25.356MiB| timeout | 0 |  |  |
|scrambled4299.smt2                                           |   61.035s | 64.172MiB| timeout | 0 |  |  |
|scrambled111627.smt2                                         |   61.036s | 54.488MiB| timeout | 0 |  |  |
|scrambled94658.smt2                                          |   61.036s | 97.0MiB| timeout | 0 |  |  |
|scrambled102166.smt2                                         |   61.036s | 64.016MiB| timeout | 0 |  |  |
|scrambled68944.smt2                                          |   61.036s | 50.6MiB| timeout | 0 |  |  |
|scrambled12042.smt2                                          |   61.037s | 88.412MiB| timeout | 0 |  |  |
|scrambled19335.smt2                                          |   61.037s | 54.392MiB| timeout | 0 |  |  |
|scrambled79760.smt2                                          |   61.037s | 56.348MiB| timeout | 0 |  |  |
|scrambled108840.smt2                                         |   61.038s | 68.256MiB| timeout | 0 |  |  |
|scrambled128874.smt2                                         |   61.039s | 15.632MiB| timeout | 0 |  |  |
|scrambled32836.smt2                                          |   61.041s | 15.292MiB| timeout | 0 |  |  |
|scrambled4198.smt2                                           |   61.041s | 96.448MiB| timeout | 0 |  |  |
|scrambled79867.smt2                                          |   61.042s | 19.8MiB| timeout | 0 |  |  |
|scrambled25238.smt2                                          |   61.042s | 15.956MiB| timeout | 0 |  |  |
|scrambled75189.smt2                                          |   61.044s | 51.812MiB| timeout | 0 |  |  |
|scrambled3854.smt2                                           |   61.044s | 18.464MiB| timeout | 0 |  |  |