# . * SAT 6 * UNSAT 0 * TIMEOUT 38 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: Z3-threads-8-smtcomp2025-QF_LIA-timeout20min-bb2-ablate
Runner: rise-runner-2
Z3 repo: ilanashapiro/z3
Z3 commit: ae632291327d6cc0ccd360d0d267ddd7b28f703e
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: ablate
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |scrambled20101.smt2 | 51.455s | 1503.0MiB| sat | 0 | | | |scrambled125827.smt2 | 86.311s | 1006.0MiB| sat | 0 | | | |scrambled118793.smt2 | 113.557s | 945.0MiB| sat | 0 | | | |scrambled125888.smt2 | 148.401s | 1604.0MiB| sat | 0 | | | |scrambled25238.smt2 | 204.714s | 5957.0MiB| sat | 0 | | | |scrambled32836.smt2 | 574.308s | 2588.0MiB| sat | 0 | | | |scrambled45952.smt2 | 1200.012s | 41.796MiB| timeout | 0 | | | |scrambled59713.smt2 | 1200.026s | 41.58MiB| timeout | 0 | | | |scrambled79867.smt2 | 1200.027s | 42.176MiB| timeout | 0 | | | |scrambled65181.smt2 | 1200.027s | 42.556MiB| timeout | 0 | | | |scrambled39514.smt2 | 1200.032s | 74.932MiB| timeout | 0 | | | |scrambled79766.smt2 | 1200.035s | 42.552MiB| timeout | 0 | | | |scrambled103783.smt2 | 1200.040s | 42.808MiB| timeout | 0 | | | |scrambled3854.smt2 | 1200.050s | 42.556MiB| timeout | 0 | | | |scrambled1417.smt2 | 1200.085s | 375.0MiB| timeout | 0 | | | |scrambled95803.smt2 | 1200.321s | 2557.0MiB| timeout | 0 | | | |scrambled128874.smt2 | 1200.547s | 5166.0MiB| timeout | 0 | | | |scrambled55777.smt2 | 1200.550s | 4607.0MiB| timeout | 0 | | | |scrambled128128.smt2 | 1200.587s | 6535.0MiB| timeout | 0 | | | |scrambled44911.smt2 | 1200.637s | 5025.0MiB| timeout | 0 | | | |scrambled51053.smt2 | 1200.646s | 2914.0MiB| timeout | 0 | | | |scrambled128732.smt2 | 1200.711s | 5119.0MiB| timeout | 0 | | | |scrambled7741.smt2 | 1200.783s | 6845.0MiB| timeout | 0 | | | |scrambled119331.smt2 | 1200.833s | 9489.0MiB| timeout | 0 | | | |scrambled131241.smt2 | 1200.917s | 6443.0MiB| timeout | 0 | | | |scrambled40621.smt2 | 1200.997s | 10.546GiB| timeout | 0 | | | |scrambled72668.smt2 | 1201.078s | 5302.0MiB| timeout | 0 | | | |scrambled61922.smt2 | 1201.664s | 10.832GiB| timeout | 0 | | | |scrambled107115.smt2 | 1201.758s | 17.782GiB| timeout | 0 | | | |scrambled27843.smt2 | 1202.351s | 21.05GiB| timeout | 0 | | | |scrambled107826.smt2 | 1202.411s | 27.988GiB| timeout | 0 | | | |scrambled75189.smt2 | 1202.728s | 31.687GiB| timeout | 0 | | | |scrambled19335.smt2 | 1203.085s | 32.44GiB| timeout | 0 | | | |scrambled43577.smt2 | 1203.284s | 34.327GiB| timeout | 0 | | | |scrambled111627.smt2 | 1203.649s | 37.787GiB| timeout | 0 | | | |scrambled108840.smt2 | 1203.670s | 43.085GiB| timeout | 0 | | | |scrambled79760.smt2 | 1204.043s | 44.268GiB| timeout | 0 | | | |scrambled68944.smt2 | 1204.380s | 47.277GiB| timeout | 0 | | | |scrambled102166.smt2 | 1204.397s | 48.159GiB| timeout | 0 | | | |scrambled4198.smt2 | 1204.520s | 49.189GiB| timeout | 0 | | | |scrambled4299.smt2 | 1204.844s | 56.787GiB| timeout | 0 | | | |scrambled12042.smt2 | 1205.037s | 54.434GiB| timeout | 0 | | | |scrambled55680.smt2 | 1205.801s | 50.699GiB| timeout | 0 | | | |scrambled94658.smt2 | 1208.508s | 63.524GiB| timeout | 0 | | |