# . * SAT 9 * UNSAT 35 * TIMEOUT 31 * UNKNOWN 0 * UNSET 0 * ERROR 0 # Meta data 
Ramon benchmark for Z3
-
Job description: 
Job tag: smt_qfaufbv-threads-4-shareunits-nonrelevant
Runner: lev-ripper
Z3 repo: ilanashapiro/z3
Z3 commit: 47ce383ab5ffb3930ebc99a3d81d5b4e7b62f521
Z3 branch: 
Z3 options: "-T:30 smt.threads=4 tactic.default_tactic=smt smt_parallel.never_cube=true smt_parallel.share_conflicts=true smt_parallel.share_units=false smt_parallel.relevant_units_only=false"
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.ec_full_add1.short.smt2 | 0.080s | 88.868MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2/gzip/250_gzip.smt2 | 0.082s | 92.36MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner13.short.smt2 | 0.086s | 97.768MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mul_inner4.short.smt2 | 0.120s | 111.0MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner23.short.smt2 | 0.123s | 111.0MiB| sat | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_data_order_one_block_correct_fn_calls_equal.smt2 | 0.127s | 91.16MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner12.short.smt2 | 0.131s | 100.0MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div10.short.smt2 | 0.140s | 122.0MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2-partial-undef/gzip/322_gzip.smt2 | 0.143s | 97.904MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_init.short.smt2 | 0.144s | 121.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.sq_inner22.short.smt2 | 0.145s | 115.0MiB| sat | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_armv8_one_block_correct_fn_calls_equal.smt2 | 0.149s | 91.952MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_init2.short.smt2 | 0.150s | 121.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_add2.short.smt2 | 0.153s | 118.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_add4.short.smt2 | 0.154s | 126.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mul_inner3.short.smt2 | 0.157s | 118.0MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_init1.short.smt2 | 0.160s | 121.0MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2/gzip/272_gzip.smt2 | 0.166s | 97.16MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_add3.short.smt2 | 0.192s | 136.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.signHash5.short.smt2 | 0.305s | 177.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.signHash3.short.smt2 | 0.322s | 184.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.signHash4.short.smt2 | 0.326s | 182.0MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2-partial-undef/gzip/332_gzip.smt2 | 0.334s | 98.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_aux11.short.smt2 | 0.408s | 249.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_aux1.short.smt2 | 0.408s | 249.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_twin_mul_aux12.short.smt2 | 0.431s | 249.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div12.short.smt2 | 0.480s | 135.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div14.short.smt2 | 0.519s | 135.0MiB| unsat | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_NPT_2.smt2 | 0.700s | 135.0MiB| sat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_mul_aux2.short.smt2 | 0.714s | 178.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_mul_aux3.short.smt2 | 0.719s | 178.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_mul_aux4.short.smt2 | 0.733s | 178.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.mod_div1.short.smt2 | 0.845s | 139.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.group_red1.short.smt2 | 1.567s | 159.0MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2/ph7/708_ph7.smt2 | 2.250s | 560.0MiB| sat | 0 | | | |QF_AUFBV/20210301-Alive2-partial-undef/gcc/204_gcc.smt2 | 3.116s | 150.0MiB| unsat | 0 | | | |QF_AUFBV/20210301-Alive2-partial-undef/sqlite3/891_sqlite3.smt2 | 3.749s | 252.0MiB| sat | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_armv8_one_block_correct_fn_calls_equal_no_rewrite.smt2 | 5.582s | 230.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.verifySignature.short.smt2 | 11.546s | 265.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_sub3.short.smt2 | 14.280s | 409.0MiB| unsat | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/picorv32-check-compact-mem.smt2 | 18.443s | 557.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_sub2.short.smt2 | 19.105s | 553.0MiB| unsat | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/zipcpu-busdelay-compact-mem.smt2 | 21.874s | 568.0MiB| unsat | 0 | | | |QF_AUFBV/ecc/com.galois.ecc.P384ECC64.ec_full_sub1.short.smt2 | 22.387s | 667.0MiB| unsat | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_NPT_1.smt2 | 30.049s | 408.0MiB| timeout | 0 | | | |QF_AUFBV/20210301-Alive2/sqlite3/906_sqlite3.smt2 | 30.057s | 444.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/VexRiscv-regch0-20-compact-mem.smt2 | 30.070s | 383.0MiB| timeout | 0 | | | |QF_AUFBV/20210301-Alive2/gcc/033_gcc.smt2 | 30.073s | 654.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/VexRiscv-regch0-15-compact-mem.smt2 | 30.076s | 317.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/zipcpu-zipmmu-compact-mem.smt2 | 30.092s | 627.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutAY_QF_AUFBV_NONINCR.smt2 | 30.096s | 619.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/picorv32-pcregs-compact-mem.smt2 | 30.100s | 419.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/VexRiscv-regch0-30-compact-mem.smt2 | 30.101s | 633.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutBY_QF_AUFBV_NONINCR.smt2 | 30.102s | 691.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutCX_QF_AUFBV_NONINCR.smt2 | 30.105s | 771.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutCY_QF_AUFBV_NONINCR.smt2 | 30.108s | 680.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutAX_QF_AUFBV_NONINCR.smt2 | 30.112s | 662.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2019A/picorv32_mutBX_QF_AUFBV_NONINCR.smt2 | 30.131s | 780.0MiB| timeout | 0 | | | |QF_AUFBV/20210301-Alive2/sqlite3/823_sqlite3.smt2 | 30.190s | 1434.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_O_32_32_2_2.smt2 | 30.206s | 1950.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_O_16_24_2_2.smt2 | 30.206s | 1831.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_O_32_16_2_2.smt2 | 30.227s | 1843.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_O_16_32_2_2.smt2 | 30.240s | 1879.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_C_16_32_2_2.smt2 | 30.360s | 2963.0MiB| timeout | 0 | | | |QF_AUFBV/20210301-Alive2/gcc/073_gcc.smt2 | 30.375s | 3146.0MiB| timeout | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_data_order_one_block_correct_fn_calls_equal_no_rewrite.smt2 | 30.400s | 3228.0MiB| timeout | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_data_order_loop_inductive_invariant_no_rewriteLoopInductive.smt2 | 30.408s | 2852.0MiB| timeout | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_armv8_loop_inductive_invariant_no_rewriteLoopInductive.smt2 | 30.410s | 3298.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/ponylink-slaveTXlen-sat-compact-mem.smt2 | 30.537s | 4976.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/zipcpu-pfcache-compact-mem.smt2 | 30.613s | 4614.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Wolf-fmbench/2018E/ponylink-slaveTXlen-unsat-compact-mem.smt2 | 30.654s | 4871.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_MBA_7.smt2 | 30.768s | 7236.0MiB| timeout | 0 | | | |QF_AUFBV/2019-Gonzalvez/opStructure_MBA_6.smt2 | 30.841s | 7368.0MiB| timeout | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_armv8_loop_inductive_invariantLoopInductive.smt2 | 30.965s | 8675.0MiB| timeout | 0 | | | |QF_AUFBV/20231002-nysm/sha512_block_data_order_loop_inductive_invariantLoopInductive.smt2 | 30.965s | 9541.0MiB| timeout | 0 | | |