# . * SAT 7 * UNSAT 0 * TIMEOUT 37 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-4-smtcomp2025-QF_LIA-timeout_20min-local_bb1
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: bdff96fde97215ca1c28b4d30df7a4a20cbfc050
Z3 branch: backbones
Z3 options: "-T:1260 -v:0 smt.threads=4 tactic.default_tactic=smt smt.auto_config=false smt_parallel.local_backbones=true"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_LIA
Z3 commit message: undo local bb ablation about resetting phase/activities, and reinstate the shared lemmas of length 2 and 3 experiment
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled95803.smt2 | 14.739s | 623.0MiB| sat | 0 | | | |scrambled125827.smt2 | 121.310s | 411.0MiB| sat | 0 | | | |scrambled20101.smt2 | 165.349s | 671.0MiB| sat | 0 | | | |scrambled25238.smt2 | 456.424s | 2714.0MiB| sat | 0 | | | |scrambled125888.smt2 | 548.859s | 676.0MiB| sat | 0 | | | |scrambled32836.smt2 | 579.329s | 1084.0MiB| sat | 0 | | | |scrambled118793.smt2 | 891.427s | 413.0MiB| sat | 0 | | | |scrambled65181.smt2 | 1260.023s | 42.364MiB| timeout | 0 | | | |scrambled45952.smt2 | 1260.024s | 41.8MiB| timeout | 0 | | | |scrambled39514.smt2 | 1260.035s | 74.68MiB| timeout | 0 | | | |scrambled103783.smt2 | 1260.039s | 42.808MiB| timeout | 0 | | | |scrambled79867.smt2 | 1260.051s | 41.796MiB| timeout | 0 | | | |scrambled79766.smt2 | 1260.053s | 42.824MiB| timeout | 0 | | | |scrambled59713.smt2 | 1260.053s | 41.792MiB| timeout | 0 | | | |scrambled3854.smt2 | 1260.054s | 42.604MiB| timeout | 0 | | | |scrambled1417.smt2 | 1260.087s | 157.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1260.191s | 1569.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1260.205s | 2062.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 1260.305s | 1319.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1260.395s | 2164.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1260.403s | 2490.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1260.415s | 2575.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1260.419s | 1996.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1260.423s | 2713.0MiB| timeout | 0 | | | |scrambled72668.smt2 | 1260.466s | 2163.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1260.583s | 4279.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1260.602s | 4039.0MiB| timeout | 0 | | | |scrambled61922.smt2 | 1260.843s | 5565.0MiB| timeout | 0 | | | |scrambled107115.smt2 | 1261.070s | 8696.0MiB| timeout | 0 | | | |scrambled27843.smt2 | 1261.184s | 11.128GiB| timeout | 0 | | | |scrambled43577.smt2 | 1261.545s | 15.338GiB| timeout | 0 | | | |scrambled107826.smt2 | 1261.587s | 14.244GiB| timeout | 0 | | | |scrambled19335.smt2 | 1261.718s | 15.597GiB| timeout | 0 | | | |scrambled111627.smt2 | 1261.859s | 18.981GiB| timeout | 0 | | | |scrambled75189.smt2 | 1261.904s | 17.038GiB| timeout | 0 | | | |scrambled4198.smt2 | 1262.062s | 24.522GiB| timeout | 0 | | | |scrambled108840.smt2 | 1262.118s | 22.301GiB| timeout | 0 | | | |scrambled102166.smt2 | 1262.211s | 23.489GiB| timeout | 0 | | | |scrambled79760.smt2 | 1262.293s | 21.909GiB| timeout | 0 | | | |scrambled55680.smt2 | 1262.335s | 25.02GiB| timeout | 0 | | | |scrambled68944.smt2 | 1262.413s | 23.315GiB| timeout | 0 | | | |scrambled4299.smt2 | 1262.651s | 26.155GiB| timeout | 0 | | | |scrambled12042.smt2 | 1262.949s | 29.835GiB| timeout | 0 | | | |scrambled94658.smt2 | 1263.109s | 31.37GiB| timeout | 0 | | |