# . * SAT 9 * UNSAT 34 * TIMEOUT 32 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: smt_qfaufbv-threads-1
Runner: lev-ripper
Z3 repo: ilanashapiro/z3
Z3 commit: 47ce383ab5ffb3930ebc99a3d81d5b4e7b62f521
Z3 branch: 
Z3 options: "-T:30 smt.threads=1 tactic.default_tactic=smt"
Z3 inputs: inputs/QF_AUFBV
Z3 commit message: Merge branch 'Z3Prover:master' into parallel-solving
# Statistics |FILE |TIME |MEM | STATUS | EXIT | STDOUT | STDERR | |------------|----------:|---------:|-------------:| ----------:|--------|--------| |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner13.short.smt2 | 0.022s | 21.78MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div10.short.smt2 | 0.025s | 19.956MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mul_inner4.short.smt2 | 0.030s | 25.228MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner23.short.smt2 | 0.034s | 25.496MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner12.short.smt2 | 0.036s | 22.868MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_add1.short.smt2 | 0.036s | 19.456MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2/gzip/250_gzip.smt2 | 0.040s | 20.7MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div1.short.smt2 | 0.040s | 29.448MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div14.short.smt2 | 0.041s | 29.424MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div12.short.smt2 | 0.041s | 29.328MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_add2.short.smt2 | 0.044s | 27.808MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_init.short.smt2 | 0.045s | 28.66MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_init2.short.smt2 | 0.046s | 28.764MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_init1.short.smt2 | 0.049s | 28.876MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner22.short.smt2 | 0.049s | 26.544MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_add4.short.smt2 | 0.052s | 29.836MiB| unsat | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_armv8_one_block_correct_fn_calls_equal.smt2 | 0.053s | 22.076MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2-partial-undef/gzip/322_gzip.smt2 | 0.053s | 22.26MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_add3.short.smt2 | 0.057s | 32.804MiB| unsat | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_data_order_one_block_correct_fn_calls_equal.smt2 | 0.069s | 21.016MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2/gzip/272_gzip.smt2 | 0.081s | 23.712MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mul_inner3.short.smt2 | 0.082s | 27.572MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.signHash5.short.smt2 | 0.088s | 37.812MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.signHash4.short.smt2 | 0.091s | 38.704MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.signHash3.short.smt2 | 0.092s | 38.588MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_aux12.short.smt2 | 0.120s | 60.54MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_aux1.short.smt2 | 0.124s | 60.476MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_aux11.short.smt2 | 0.130s | 60.776MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2-partial-undef/gzip/332_gzip.smt2 | 0.235s | 22.744MiB| unsat | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_NPT_2.smt2 | 0.431s | 30.384MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_mul_aux3.short.smt2 | 0.656s | 39.576MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_mul_aux2.short.smt2 | 0.660s | 39.424MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_mul_aux4.short.smt2 | 0.664s | 39.42MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.group_red1.short.smt2 | 1.248s | 34.008MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2-partial-undef/gcc/204_gcc.smt2 | 2.070s | 33.68MiB| unsat | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_armv8_one_block_correct_fn_calls_equal_no_rewrite.smt2 | 3.110s | 182.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_sub1.short.smt2 | 6.045s | 61.18MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2/ph7/708_ph7.smt2 | 8.162s | 159.0MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.verifySignature.short.smt2 | 9.094s | 67.196MiB| unsat | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/picorv32-check-compact-mem.smt2 | 9.578s | 137.0MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2-partial-undef/sqlite3/891_sqlite3.smt2 | 13.218s | 72.684MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_sub2.short.smt2 | 15.392s | 133.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_sub3.short.smt2 | 17.573s | 116.0MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2/sqlite3/906_sqlite3.smt2 | 30.016s | 125.0MiB| timeout | 0 | | | |QF_AUFBV/20210301-Alive2/gcc/033_gcc.smt2 | 30.019s | 145.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/VexRiscv-regch0-20-compact-mem.smt2 | 30.020s | 117.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/zipcpu-zipmmu-compact-mem.smt2 | 30.025s | 169.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/VexRiscv-regch0-30-compact-mem.smt2 | 30.027s | 154.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/VexRiscv-regch0-15-compact-mem.smt2 | 30.028s | 83.484MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/zipcpu-busdelay-compact-mem.smt2 | 30.031s | 159.0MiB| timeout | 0 | | | |QF_AUFBV/20210301-Alive2/sqlite3/823_sqlite3.smt2 | 30.034s | 322.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutBY_QF_AUFBV_NONINCR.smt2 | 30.034s | 213.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/picorv32-pcregs-compact-mem.smt2 | 30.035s | 111.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_NPT_1.smt2 | 30.036s | 82.108MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutAX_QF_AUFBV_NONINCR.smt2 | 30.036s | 208.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutCX_QF_AUFBV_NONINCR.smt2 | 30.042s | 232.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutCY_QF_AUFBV_NONINCR.smt2 | 30.045s | 217.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutAY_QF_AUFBV_NONINCR.smt2 | 30.056s | 160.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutBX_QF_AUFBV_NONINCR.smt2 | 30.061s | 232.0MiB| timeout | 0 | | | |QF_AUFBV/20210301-Alive2/gcc/073_gcc.smt2 | 30.074s | 740.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/ponylink-slaveTXlen-unsat-compact-mem.smt2 | 30.111s | 1206.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_C_16_32_2_2.smt2 | 30.121s | 1116.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/zipcpu-pfcache-compact-mem.smt2 | 30.139s | 1127.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/ponylink-slaveTXlen-sat-compact-mem.smt2 | 30.148s | 1270.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_O_32_32_2_2.smt2 | 30.161s | 1748.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_O_16_32_2_2.smt2 | 30.178s | 1790.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_O_16_24_2_2.smt2 | 30.179s | 1797.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_O_32_16_2_2.smt2 | 30.186s | 1779.0MiB| timeout | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_armv8_loop_inductive_invariantLoopInductive.smt2 | 30.259s | 2649.0MiB| timeout | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_data_order_loop_inductive_invariant_no_rewriteLoopInductive.smt2 | 30.298s | 2528.0MiB| timeout | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_data_order_one_block_correct_fn_calls_equal_no_rewrite.smt2 | 30.310s | 3063.0MiB| timeout | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_armv8_loop_inductive_invariant_no_rewriteLoopInductive.smt2 | 30.359s | 3022.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_MBA_6.smt2 | 30.516s | 5267.0MiB| timeout | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_data_order_loop_inductive_invariantLoopInductive.smt2 | 30.521s | 5246.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_MBA_7.smt2 | 30.785s | 8014.0MiB| timeout | 0 | | |