# . * SAT 8 * UNSAT 0 * 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-bb2
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: dd30b9eaf3624ea8d87e9e84ece5b50b171e5eda
Z3 branch: core_min
Z3 options: "-T:1200 -v:0 smt.threads=8 tactic.default_tactic=smt smt.auto_config=false 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 | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled20101.smt2 | 125.361s | 1631.0MiB| sat | 0 | | | |scrambled125827.smt2 | 138.956s | 1012.0MiB| sat | 0 | | | |scrambled125888.smt2 | 145.287s | 1604.0MiB| sat | 0 | | | |scrambled118793.smt2 | 150.254s | 962.0MiB| sat | 0 | | | |scrambled25238.smt2 | 205.382s | 5921.0MiB| sat | 0 | | | |scrambled95803.smt2 | 405.493s | 2470.0MiB| sat | 0 | | | |scrambled72668.smt2 | 669.769s | 5210.0MiB| sat | 0 | | | |scrambled32836.smt2 | 1012.554s | 2650.0MiB| sat | 0 | | | |scrambled3854.smt2 | 1200.014s | 42.324MiB| timeout | 0 | | | |scrambled45952.smt2 | 1200.014s | 41.536MiB| timeout | 0 | | | |scrambled39514.smt2 | 1200.033s | 74.704MiB| timeout | 0 | | | |scrambled59713.smt2 | 1200.036s | 41.796MiB| timeout | 0 | | | |scrambled103783.smt2 | 1200.037s | 42.564MiB| timeout | 0 | | | |scrambled65181.smt2 | 1200.040s | 42.464MiB| timeout | 0 | | | |scrambled79867.smt2 | 1200.041s | 41.816MiB| timeout | 0 | | | |scrambled79766.smt2 | 1200.052s | 42.556MiB| timeout | 0 | | | |scrambled1417.smt2 | 1200.097s | 370.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1200.504s | 5142.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 1200.638s | 2914.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1200.655s | 5058.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1200.707s | 5176.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1200.741s | 6487.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1200.770s | 6776.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1200.776s | 6457.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1200.838s | 4561.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1200.903s | 9348.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1201.155s | 10.951GiB| timeout | 0 | | | |scrambled61922.smt2 | 1201.246s | 10.83GiB| timeout | 0 | | | |scrambled107115.smt2 | 1201.818s | 17.756GiB| timeout | 0 | | | |scrambled27843.smt2 | 1202.248s | 21.034GiB| timeout | 0 | | | |scrambled107826.smt2 | 1202.529s | 27.847GiB| timeout | 0 | | | |scrambled19335.smt2 | 1203.193s | 31.987GiB| timeout | 0 | | | |scrambled43577.smt2 | 1203.490s | 34.291GiB| timeout | 0 | | | |scrambled111627.smt2 | 1203.643s | 37.772GiB| timeout | 0 | | | |scrambled108840.smt2 | 1203.999s | 43.088GiB| timeout | 0 | | | |scrambled75189.smt2 | 1204.030s | 31.663GiB| timeout | 0 | | | |scrambled68944.smt2 | 1204.356s | 46.867GiB| timeout | 0 | | | |scrambled79760.smt2 | 1204.386s | 44.258GiB| timeout | 0 | | | |scrambled102166.smt2 | 1205.196s | 48.042GiB| timeout | 0 | | | |scrambled4299.smt2 | 1205.279s | 56.815GiB| timeout | 0 | | | |scrambled12042.smt2 | 1205.335s | 54.49GiB| timeout | 0 | | | |scrambled4198.smt2 | 1205.458s | 49.17GiB| timeout | 0 | | | |scrambled55680.smt2 | 1205.686s | 50.628GiB| timeout | 0 | | | |scrambled94658.smt2 | 1205.987s | 63.168GiB| timeout | 0 | | |