# . * SAT 7 * UNSAT 0 * TIMEOUT 37 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_LIA-timeout20min-bb2-auto_config-ablate
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: dd30b9eaf3624ea8d87e9e84ece5b50b171e5eda
Z3 branch: dd30b9eaf3624ea8d87e9e84ece5b50b171e5eda
Z3 options: "-T:1200 -v:0 smt.threads=8 tactic.default_tactic=smt smt_parallel.num_global_bb_batch_threads=2"
Z3 inputs: inputs/smt_comp_2025_parallel/QF_LIA
Z3 commit message: restore incomplete-theory give-up paths
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled125827.smt2 | 39.638s | 939.0MiB| sat | 0 | | | |scrambled118793.smt2 | 78.687s | 899.0MiB| sat | 0 | | | |scrambled25238.smt2 | 89.711s | 3600.0MiB| sat | 0 | | | |scrambled125888.smt2 | 232.314s | 1550.0MiB| sat | 0 | | | |scrambled128128.smt2 | 335.828s | 4778.0MiB| sat | 0 | | | |scrambled20101.smt2 | 350.108s | 1648.0MiB| sat | 0 | | | |scrambled44911.smt2 | 363.941s | 3867.0MiB| sat | 0 | | | |scrambled45952.smt2 | 1200.015s | 41.78MiB| timeout | 0 | | | |scrambled39514.smt2 | 1200.035s | 74.668MiB| timeout | 0 | | | |scrambled79867.smt2 | 1200.036s | 41.8MiB| timeout | 0 | | | |scrambled65181.smt2 | 1200.036s | 42.576MiB| timeout | 0 | | | |scrambled59713.smt2 | 1200.036s | 42.044MiB| timeout | 0 | | | |scrambled103783.smt2 | 1200.040s | 42.308MiB| timeout | 0 | | | |scrambled3854.smt2 | 1200.051s | 42.792MiB| timeout | 0 | | | |scrambled1417.smt2 | 1200.075s | 375.0MiB| timeout | 0 | | | |scrambled79766.smt2 | 1200.081s | 42.588MiB| timeout | 0 | | | |scrambled55777.smt2 | 1200.339s | 3239.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 1200.400s | 2888.0MiB| timeout | 0 | | | |scrambled32836.smt2 | 1200.408s | 2611.0MiB| timeout | 0 | | | |scrambled95803.smt2 | 1200.440s | 2329.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1200.509s | 4760.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1200.635s | 5139.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1200.653s | 4704.0MiB| timeout | 0 | | | |scrambled72668.smt2 | 1200.752s | 5160.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1200.759s | 5900.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1200.764s | 7062.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1200.791s | 6444.0MiB| timeout | 0 | | | |scrambled61922.smt2 | 1201.345s | 10.754GiB| timeout | 0 | | | |scrambled107115.smt2 | 1201.808s | 17.678GiB| timeout | 0 | | | |scrambled107826.smt2 | 1202.741s | 27.659GiB| timeout | 0 | | | |scrambled27843.smt2 | 1202.878s | 20.866GiB| timeout | 0 | | | |scrambled19335.smt2 | 1202.975s | 32.161GiB| timeout | 0 | | | |scrambled43577.smt2 | 1203.108s | 33.981GiB| timeout | 0 | | | |scrambled75189.smt2 | 1203.395s | 31.457GiB| timeout | 0 | | | |scrambled108840.smt2 | 1203.727s | 42.728GiB| timeout | 0 | | | |scrambled79760.smt2 | 1204.086s | 43.99GiB| timeout | 0 | | | |scrambled111627.smt2 | 1204.111s | 37.479GiB| timeout | 0 | | | |scrambled102166.smt2 | 1204.341s | 47.752GiB| timeout | 0 | | | |scrambled55680.smt2 | 1204.573s | 50.279GiB| timeout | 0 | | | |scrambled4198.smt2 | 1204.886s | 48.897GiB| timeout | 0 | | | |scrambled68944.smt2 | 1205.012s | 46.644GiB| timeout | 0 | | | |scrambled4299.smt2 | 1205.244s | 56.444GiB| timeout | 0 | | | |scrambled12042.smt2 | 1206.231s | 54.035GiB| timeout | 0 | | | |scrambled94658.smt2 | 1207.013s | 62.581GiB| timeout | 0 | | |