# . * SAT 7 * UNSAT 1 * TIMEOUT 36 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_LIA-timeout20min-v1
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: 9802bb4838b72199dab085698cfcfdc169ab06e5
Z3 branch: 9802bb4838b72199dab085698cfcfdc169ab06e5
Z3 options: "-T:1200 -v:0 smt.threads=8"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_LIA
Z3 commit message: ablate continuous FL checking
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled61922.smt2 | 7.057s | 383.0MiB| unsat | 0 | | | |scrambled107826.smt2 | 46.916s | 1130.0MiB| sat | 0 | | | |scrambled125888.smt2 | 123.003s | 1337.0MiB| sat | 0 | | | |scrambled51053.smt2 | 168.846s | 530.0MiB| sat | 0 | | | |scrambled20101.smt2 | 270.703s | 1480.0MiB| sat | 0 | | | |scrambled118793.smt2 | 327.791s | 876.0MiB| sat | 0 | | | |scrambled125827.smt2 | 437.671s | 920.0MiB| sat | 0 | | | |scrambled95803.smt2 | 570.611s | 2106.0MiB| sat | 0 | | | |scrambled103783.smt2 | 1200.013s | 42.812MiB| timeout | 0 | | | |scrambled59713.smt2 | 1200.021s | 42.312MiB| timeout | 0 | | | |scrambled45952.smt2 | 1200.021s | 42.592MiB| timeout | 0 | | | |scrambled39514.smt2 | 1200.028s | 75.252MiB| timeout | 0 | | | |scrambled65181.smt2 | 1200.033s | 42.824MiB| timeout | 0 | | | |scrambled79867.smt2 | 1200.034s | 42.812MiB| timeout | 0 | | | |scrambled1417.smt2 | 1200.047s | 261.0MiB| timeout | 0 | | | |scrambled79766.smt2 | 1200.054s | 42.828MiB| timeout | 0 | | | |scrambled3854.smt2 | 1200.065s | 43.324MiB| timeout | 0 | | | |scrambled27843.smt2 | 1200.087s | 640.0MiB| timeout | 0 | | | |scrambled107115.smt2 | 1200.104s | 601.0MiB| timeout | 0 | | | |scrambled75189.smt2 | 1200.146s | 1073.0MiB| timeout | 0 | | | |scrambled43577.smt2 | 1200.153s | 1421.0MiB| timeout | 0 | | | |scrambled19335.smt2 | 1200.156s | 1174.0MiB| timeout | 0 | | | |scrambled111627.smt2 | 1200.160s | 1220.0MiB| timeout | 0 | | | |scrambled108840.smt2 | 1200.163s | 1473.0MiB| timeout | 0 | | | |scrambled79760.smt2 | 1200.191s | 1674.0MiB| timeout | 0 | | | |scrambled68944.smt2 | 1200.223s | 1770.0MiB| timeout | 0 | | | |scrambled4299.smt2 | 1200.248s | 2011.0MiB| timeout | 0 | | | |scrambled55680.smt2 | 1200.263s | 2512.0MiB| timeout | 0 | | | |scrambled102166.smt2 | 1200.270s | 2761.0MiB| timeout | 0 | | | |scrambled94658.smt2 | 1200.272s | 2666.0MiB| timeout | 0 | | | |scrambled32836.smt2 | 1200.311s | 2302.0MiB| timeout | 0 | | | |scrambled12042.smt2 | 1200.313s | 2600.0MiB| timeout | 0 | | | |scrambled4198.smt2 | 1200.319s | 2558.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1200.472s | 4799.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1200.540s | 3104.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1200.600s | 5744.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1200.606s | 3692.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1200.638s | 4047.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1200.650s | 4197.0MiB| timeout | 0 | | | |scrambled72668.smt2 | 1200.682s | 4430.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1200.732s | 6458.0MiB| timeout | 0 | | | |scrambled25238.smt2 | 1200.775s | 6108.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1200.934s | 4959.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1200.956s | 5470.0MiB| timeout | 0 | | |