# .

* SAT 7
* UNSAT 0
* TIMEOUT 37
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-4-smtcomp2025-QF_LIA-timeout_20min-vsids-aggressivebacktrack
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 8e294820a0bcdbe59f6282f7a0a3f73f594bd601
Z3 branch: backbones
Z3 options: "-T:1260 -v:0 smt.threads=4 tactic.default_tactic=smt smt.auto_config=false"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_LIA
Z3 commit message: backtrack more aggressively in search tree: close matching external targets (i.e. repeat literals on other branches)

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|scrambled20101.smt2                                          |   68.566s | 623.0MiB| sat | 0 |  |  |
|scrambled118793.smt2                                         |  114.059s | 370.0MiB| sat | 0 |  |  |
|scrambled125888.smt2                                         |  203.232s | 644.0MiB| sat | 0 |  |  |
|scrambled32836.smt2                                          |  482.830s | 1021.0MiB| sat | 0 |  |  |
|scrambled25238.smt2                                          |  624.633s | 2845.0MiB| sat | 0 |  |  |
|scrambled72668.smt2                                          | 1058.226s | 2136.0MiB| sat | 0 |  |  |
|scrambled125827.smt2                                         | 1180.114s | 415.0MiB| sat | 0 |  |  |
|scrambled79766.smt2                                          | 1260.017s | 42.356MiB| timeout | 0 |  |  |
|scrambled65181.smt2                                          | 1260.023s | 42.56MiB| timeout | 0 |  |  |
|scrambled59713.smt2                                          | 1260.023s | 41.796MiB| timeout | 0 |  |  |
|scrambled45952.smt2                                          | 1260.025s | 41.54MiB| timeout | 0 |  |  |
|scrambled103783.smt2                                         | 1260.031s | 42.544MiB| timeout | 0 |  |  |
|scrambled1417.smt2                                           | 1260.034s | 158.0MiB| timeout | 0 |  |  |
|scrambled39514.smt2                                          | 1260.038s | 74.92MiB| timeout | 0 |  |  |
|scrambled3854.smt2                                           | 1260.048s | 42.592MiB| timeout | 0 |  |  |
|scrambled79867.smt2                                          | 1260.050s | 42.04MiB| timeout | 0 |  |  |
|scrambled55777.smt2                                          | 1260.196s | 1782.0MiB| timeout | 0 |  |  |
|scrambled51053.smt2                                          | 1260.212s | 1316.0MiB| timeout | 0 |  |  |
|scrambled95803.smt2                                          | 1260.229s | 1003.0MiB| timeout | 0 |  |  |
|scrambled44911.smt2                                          | 1260.245s | 2016.0MiB| timeout | 0 |  |  |
|scrambled128874.smt2                                         | 1260.354s | 2113.0MiB| timeout | 0 |  |  |
|scrambled128732.smt2                                         | 1260.444s | 2085.0MiB| timeout | 0 |  |  |
|scrambled7741.smt2                                           | 1260.462s | 2658.0MiB| timeout | 0 |  |  |
|scrambled131241.smt2                                         | 1260.464s | 2578.0MiB| timeout | 0 |  |  |
|scrambled128128.smt2                                         | 1260.489s | 2571.0MiB| timeout | 0 |  |  |
|scrambled40621.smt2                                          | 1260.565s | 4736.0MiB| timeout | 0 |  |  |
|scrambled119331.smt2                                         | 1260.591s | 3775.0MiB| timeout | 0 |  |  |
|scrambled61922.smt2                                          | 1260.806s | 5556.0MiB| timeout | 0 |  |  |
|scrambled107115.smt2                                         | 1260.910s | 8691.0MiB| timeout | 0 |  |  |
|scrambled107826.smt2                                         | 1261.427s | 14.227GiB| timeout | 0 |  |  |
|scrambled27843.smt2                                          | 1261.482s | 11.123GiB| timeout | 0 |  |  |
|scrambled43577.smt2                                          | 1261.489s | 15.292GiB| timeout | 0 |  |  |
|scrambled19335.smt2                                          | 1261.510s | 15.594GiB| timeout | 0 |  |  |
|scrambled75189.smt2                                          | 1261.907s | 17.036GiB| timeout | 0 |  |  |
|scrambled108840.smt2                                         | 1262.073s | 22.294GiB| timeout | 0 |  |  |
|scrambled111627.smt2                                         | 1262.077s | 18.995GiB| timeout | 0 |  |  |
|scrambled4198.smt2                                           | 1262.146s | 25.315GiB| timeout | 0 |  |  |
|scrambled68944.smt2                                          | 1262.245s | 23.207GiB| timeout | 0 |  |  |
|scrambled79760.smt2                                          | 1262.318s | 21.916GiB| timeout | 0 |  |  |
|scrambled102166.smt2                                         | 1262.435s | 23.383GiB| timeout | 0 |  |  |
|scrambled55680.smt2                                          | 1262.577s | 24.975GiB| timeout | 0 |  |  |
|scrambled4299.smt2                                           | 1262.706s | 25.996GiB| timeout | 0 |  |  |
|scrambled12042.smt2                                          | 1263.003s | 29.827GiB| timeout | 0 |  |  |
|scrambled94658.smt2                                          | 1263.120s | 31.336GiB| timeout | 0 |  |  |