# .

* SAT 4
* UNSAT 11
* TIMEOUT 29
* UNKNOWN 0

* UNSET 0

* ERROR 0

# Meta data

<pre>
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_NIA-timeout20min-FL-v1
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 9802bb4838b72199dab085698cfcfdc169ab06e5
Z3 branch: 9802bb4838b72199dab085698cfcfdc169ab06e5
Z3 options: "-T:1200 -v:0 smt.threads=8 tactic.default_tactic=smt smt.auto_config=false smt_parallel.failed_literal_backbones=true"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_NIA
Z3 commit message: ablate continuous FL checking

</pre>


# Statistics
|FILE                                                         |TIME     |MEM        | STATUS   | EXIT | STDOUT | STDERR | 
|------------|----------:|---------:|-------------:| ----------:|--------|--------| 
|scrambled50258.smt2                                          |    0.934s | 242.0MiB| unsat | 0 |  |  |
|scrambled30073.smt2                                          |    3.592s | 228.0MiB| unsat | 0 |  |  |
|scrambled28176.smt2                                          |    3.646s | 364.0MiB| sat | 0 |  |  |
|scrambled82407.smt2                                          |    5.356s | 235.0MiB| unsat | 0 |  |  |
|scrambled48569.smt2                                          |    5.492s | 1258.0MiB| sat | 0 |  |  |
|scrambled9548.smt2                                           |    5.672s | 270.0MiB| unsat | 0 |  |  |
|scrambled129467.smt2                                         |    9.969s | 410.0MiB| unsat | 0 |  |  |
|scrambled31071.smt2                                          |   13.153s | 417.0MiB| sat | 0 |  |  |
|scrambled17293.smt2                                          |   13.664s | 968.0MiB| sat | 0 |  |  |
|scrambled12959.smt2                                          |   16.327s | 365.0MiB| unsat | 0 |  |  |
|scrambled29780.smt2                                          |   23.673s | 263.0MiB| unsat | 0 |  |  |
|scrambled103775.smt2                                         |   49.913s | 347.0MiB| unsat | 0 |  |  |
|scrambled61060.smt2                                          |  157.923s | 1524.0MiB| unsat | 0 |  |  |
|scrambled80288.smt2                                          |  213.560s | 686.0MiB| unsat | 0 |  |  |
|scrambled14845.smt2                                          |  585.197s | 5957.0MiB| unsat | 0 |  |  |
|scrambled31575.smt2                                          | 1200.108s | 567.0MiB| timeout | 0 |  |  |
|scrambled100714.smt2                                         | 1200.132s | 1191.0MiB| timeout | 0 |  |  |
|scrambled97386.smt2                                          | 1200.175s | 1475.0MiB| timeout | 0 |  |  |
|scrambled119582.smt2                                         | 1200.177s | 1373.0MiB| timeout | 0 |  |  |
|scrambled35280.smt2                                          | 1200.180s | 1388.0MiB| timeout | 0 |  |  |
|scrambled98111.smt2                                          | 1200.180s | 1257.0MiB| timeout | 0 |  |  |
|scrambled41135.smt2                                          | 1200.193s | 1570.0MiB| timeout | 0 |  |  |
|scrambled58311.smt2                                          | 1200.198s | 1830.0MiB| timeout | 0 |  |  |
|scrambled38587.smt2                                          | 1200.198s | 1409.0MiB| timeout | 0 |  |  |
|scrambled96401.smt2                                          | 1200.212s | 1355.0MiB| timeout | 0 |  |  |
|scrambled101716.smt2                                         | 1200.214s | 1387.0MiB| timeout | 0 |  |  |
|scrambled62032.smt2                                          | 1200.220s | 1503.0MiB| timeout | 0 |  |  |
|scrambled36790.smt2                                          | 1200.235s | 1542.0MiB| timeout | 0 |  |  |
|scrambled39467.smt2                                          | 1200.240s | 1751.0MiB| timeout | 0 |  |  |
|scrambled8852.smt2                                           | 1200.245s | 1532.0MiB| timeout | 0 |  |  |
|scrambled79354.smt2                                          | 1200.253s | 1607.0MiB| timeout | 0 |  |  |
|scrambled9883.smt2                                           | 1200.258s | 1493.0MiB| timeout | 0 |  |  |
|scrambled47700.smt2                                          | 1200.278s | 2047.0MiB| timeout | 0 |  |  |
|scrambled108663.smt2                                         | 1200.284s | 2629.0MiB| timeout | 0 |  |  |
|scrambled87588.smt2                                          | 1200.295s | 2315.0MiB| timeout | 0 |  |  |
|scrambled12033.smt2                                          | 1200.310s | 2636.0MiB| timeout | 0 |  |  |
|scrambled73281.smt2                                          | 1200.314s | 2500.0MiB| timeout | 0 |  |  |
|scrambled108406.smt2                                         | 1200.319s | 2510.0MiB| timeout | 0 |  |  |
|scrambled130111.smt2                                         | 1200.327s | 2174.0MiB| timeout | 0 |  |  |
|scrambled82760.smt2                                          | 1200.376s | 2168.0MiB| timeout | 0 |  |  |
|scrambled91750.smt2                                          | 1200.409s | 2329.0MiB| timeout | 0 |  |  |
|scrambled122926.smt2                                         | 1200.413s | 3334.0MiB| timeout | 0 |  |  |
|scrambled73755.smt2                                          | 1200.533s | 3725.0MiB| timeout | 0 |  |  |
|scrambled85357.smt2                                          | 1202.426s | 25.497GiB| timeout | 0 |  |  |