# . * SAT 7 * UNSAT 3 * TIMEOUT 64 * UNKNOWN 1 * ERRORS 0 # Meta data 
Ramon benchmark for Z3
-
Job description: Triggered by CoZ3 Benchmark Runner | Benchmark suite: https://zenodo.org/records/16740866/files/QF_AUFBV.tar.zst?download=1 | Source list: benchmarks.txt
Job tag: coz3-https-zenodo.org-records-16740866-files-QF_AUFBV.tar.zst-d
Runner: rise-runner-2
Z3 repo: Z3Prover/z3
Z3 commit: 459629c662eb7abf25a010b7383431a9f729d234
Z3 branch: master
Z3 options: "-T:20 -v:2 -st tactic.default_tactic="(then simplify propagate-values solve-eqs simplify sls-smt)" model_validate=true"
Z3 inputs: https://zenodo.org/records/16740866/files/QF_AUFBV.tar.zst?download=1
Z3 commit message: bugfixes to ho_matcher

Signed-off-by: Nikolaj Bjorner
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner23.short.smt2 | 0.030s | 20.612MiB| sat | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div10.short.smt2 | 0.032s | 20.096MiB| unsat | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mul_inner4.short.smt2 | 0.033s | 20.144MiB| sat | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner13.short.smt2 | 0.033s | 20.36MiB| sat | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_add1.short.smt2 | 0.044s | 19.928MiB| unsat | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner12.short.smt2 | 0.045s | 20.58MiB| sat | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div1.short.smt2 | 0.049s | 19.852MiB| unsat | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner22.short.smt2 | 0.049s | 20.624MiB| sat | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mul_inner3.short.smt2 | 0.304s | 22.108MiB| sat | 0 | | | |non-incremental/QF_AUFBV/2019-Gonzalvez/opStructure_MBA_6.smt2 | 1.135s | 115.0MiB| unknown | 0 | | | |non-incremental/QF_AUFBV/2019-Gonzalvez/opStructure_MBA_7.smt2 | 2.806s | 227.0MiB| sat | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div14.short.smt2 | 20.010s | 20.684MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20210301-Alive2-partial-undef/gzip/322_gzip.smt2 | 20.012s | 21.896MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_sub1.short.smt2 | 20.012s | 20.7MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.verifySignature.short.smt2 | 20.012s | 22.8MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.signHash5.short.smt2 | 20.013s | 22.592MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_sub3.short.smt2 | 20.013s | 20.7MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2018E/VexRiscv-regch0-20-compact-mem.smt2 | 20.015s | 57.604MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2018E/VexRiscv-regch0-15-compact-mem.smt2 | 20.015s | 49.276MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2018E/VexRiscv-regch0-30-compact-mem.smt2 | 20.019s | 73.412MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.signHash4.short.smt2 | 20.019s | 22.512MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.signHash3.short.smt2 | 20.020s | 22.744MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_sub2.short.smt2 | 20.020s | 20.432MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2018E/picorv32-pcregs-compact-mem.smt2 | 20.021s | 101.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2018E/picorv32-check-compact-mem.smt2 | 20.023s | 111.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20210301-Alive2-partial-undef/gzip/332_gzip.smt2 | 20.024s | 22.292MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20210301-Alive2/gcc/033_gcc.smt2 | 20.025s | 31.324MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20210301-Alive2-partial-undef/gcc/204_gcc.smt2 | 20.025s | 33.876MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20231002-nysm/sha512_block_armv8_one_block_correct_fn_calls_equal.smt2 | 20.026s | 34.148MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20210301-Alive2/sqlite3/906_sqlite3.smt2 | 20.027s | 36.22MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20231002-nysm/sha512_block_data_order_one_block_correct_fn_calls_equal.smt2 | 20.028s | 38.816MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20210301-Alive2-partial-undef/sqlite3/891_sqlite3.smt2 | 20.028s | 32.02MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20210301-Alive2/ph7/708_ph7.smt2 | 20.029s | 46.072MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Gonzalvez/opStructure_NPT_1.smt2 | 20.029s | 20.644MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Gonzalvez/opStructure_C_16_32_2_2.smt2 | 20.029s | 35.392MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20231002-nysm/sha512_block_armv8_loop_inductive_invariantLoopInductive.smt2 | 20.030s | 38.68MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20231002-nysm/sha512_block_data_order_loop_inductive_invariantLoopInductive.smt2 | 20.030s | 44.344MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_init2.short.smt2 | 20.030s | 20.412MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_mul_aux3.short.smt2 | 20.030s | 25.552MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutAX_QF_AUFBV_NONINCR.smt2 | 20.031s | 206.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div12.short.smt2 | 20.031s | 20.536MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20231002-nysm/sha512_block_data_order_loop_inductive_invariant_no_rewriteLoopInductive.smt2 | 20.032s | 266.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Gonzalvez/opStructure_NPT_2.smt2 | 20.032s | 20.076MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_aux11.short.smt2 | 20.032s | 21.344MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.group_red1.short.smt2 | 20.032s | 20.608MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_mul_aux2.short.smt2 | 20.032s | 25.664MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutAY_QF_AUFBV_NONINCR.smt2 | 20.033s | 125.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_add3.short.smt2 | 20.033s | 20.36MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20210301-Alive2/gzip/272_gzip.smt2 | 20.034s | 21.264MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Gonzalvez/opStructure_O_16_24_2_2.smt2 | 20.034s | 217.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutBX_QF_AUFBV_NONINCR.smt2 | 20.034s | 229.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_add2.short.smt2 | 20.034s | 20.5MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20210301-Alive2/gzip/250_gzip.smt2 | 20.035s | 21.156MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutCX_QF_AUFBV_NONINCR.smt2 | 20.035s | 229.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_add4.short.smt2 | 20.035s | 20.4MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_mul_aux4.short.smt2 | 20.035s | 25.628MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_init1.short.smt2 | 20.035s | 20.504MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_aux12.short.smt2 | 20.036s | 21.528MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_aux1.short.smt2 | 20.036s | 21.456MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_init.short.smt2 | 20.036s | 20.58MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20210301-Alive2/sqlite3/823_sqlite3.smt2 | 20.037s | 95.392MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2018E/zipcpu-zipmmu-compact-mem.smt2 | 20.039s | 82.004MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Gonzalvez/opStructure_O_16_32_2_2.smt2 | 20.041s | 276.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2018E/zipcpu-pfcache-compact-mem.smt2 | 20.041s | 316.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutCY_QF_AUFBV_NONINCR.smt2 | 20.042s | 159.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2018E/zipcpu-busdelay-compact-mem.smt2 | 20.045s | 156.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutBY_QF_AUFBV_NONINCR.smt2 | 20.045s | 143.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Gonzalvez/opStructure_O_32_16_2_2.smt2 | 20.047s | 271.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20210301-Alive2/gcc/073_gcc.smt2 | 20.048s | 147.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20231002-nysm/sha512_block_armv8_one_block_correct_fn_calls_equal_no_rewrite.smt2 | 20.063s | 388.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20231002-nysm/sha512_block_armv8_loop_inductive_invariant_no_rewriteLoopInductive.smt2 | 20.065s | 505.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/20231002-nysm/sha512_block_data_order_one_block_correct_fn_calls_equal_no_rewrite.smt2 | 20.068s | 415.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Gonzalvez/opStructure_O_32_32_2_2.smt2 | 20.073s | 536.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2018E/ponylink-slaveTXlen-sat-compact-mem.smt2 | 20.073s | 496.0MiB| timeout | 0 | | | |non-incremental/QF_AUFBV/2019-Wolf-fmbench/2018E/ponylink-slaveTXlen-unsat-compact-mem.smt2 | 20.078s | 498.0MiB| timeout | 0 | | |