Proof summary for theory abs abs2_impl_TCC1..............................proved - complete [O](0.20 s) abs2_impl_TCC2..............................proved - complete [O](0.13 s) abs2_impl_TCC3..............................proved - complete [O](0.18 s) abs2_impl_TCC4..............................proved - complete [O](0.16 s) abs2_impl_TCC5..............................proved - complete [O](0.15 s) abs2_impl_correct...........................proved - complete [O](2.04 s) abs_impl_TCC1...............................proved - complete [O](0.13 s) abs_impl_correct............................proved - complete [O](3.33 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (6.32 s) Proof summary for theory compound compound_t_TCC1............................proved - complete [O]( 0.13 s) compound_TCC1..............................proved - complete [O]( 0.12 s) compound_TCC2..............................proved - complete [O]( 0.15 s) compound_TCC3..............................proved - complete [O]( 0.14 s) compound_TCC4..............................proved - complete [O]( 0.13 s) compound_TCC5..............................proved - complete [O]( 0.13 s) compound_TCC6..............................proved - complete [O]( 0.17 s) compound_TCC7..............................proved - complete [O]( 0.54 s) compound_TCC8..............................proved - complete [O]( 0.55 s) compound_TCC9..............................proved - complete [O]( 0.55 s) compound_TCC10.............................proved - complete [O]( 0.14 s) compound_TCC11.............................proved - complete [O]( 0.14 s) compound_TCC12.............................proved - complete [O]( 0.15 s) compound_TCC13.............................proved - complete [O]( 0.80 s) compound_TCC14.............................proved - complete [O]( 0.80 s) compound_TCC15.............................proved - complete [O]( 0.14 s) compound_TCC16.............................proved - complete [O]( 0.14 s) compound_correct...........................proved - complete [O](32.40 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (37.32 s) Proof summary for theory condit_sum_adder condit_sum_adder_impl_TCC1.................proved - complete [O]( 0.13 s) condit_sum_adder_impl_TCC2.................proved - complete [O]( 0.12 s) condit_sum_adder_impl_TCC3.................proved - complete [O]( 0.12 s) condit_sum_adder_impl_TCC4.................proved - complete [O]( 0.18 s) condit_sum_adder_impl_TCC5.................proved - complete [O]( 0.23 s) condit_sum_adder_impl_TCC6.................proved - complete [O]( 0.14 s) condit_sum_adder_impl_TCC7.................proved - complete [O]( 0.56 s) condit_sum_adder_impl_TCC8.................proved - complete [O]( 0.14 s) condit_sum_adder_impl_TCC9.................proved - complete [O]( 0.15 s) condit_sum_adder_impl_TCC10................proved - complete [O]( 0.16 s) condit_sum_adder_impl_TCC11................proved - complete [O]( 0.14 s) condit_sum_adder_impl_TCC12................proved - complete [O]( 0.60 s) condit_sum_adder_impl_TCC13................proved - complete [O]( 0.15 s) condit_sum_adder_impl_TCC14................proved - complete [O]( 0.15 s) condit_sum_adder_impl_TCC15................proved - complete [O]( 0.15 s) condit_sum_adder_impl_TCC16................proved - complete [O]( 0.15 s) condit_sum_adder_impl_TCC17................proved - complete [O]( 0.15 s) condit_sum_adder_impl_TCC18................proved - complete [O]( 0.15 s) condit_sum_adder_impl_TCC19................proved - complete [O]( 0.16 s) condit_sum_adder_impl_TCC20................proved - complete [O]( 0.16 s) condit_sum_adder_impl_TCC21................proved - complete [O]( 0.15 s) condit_sum_adder_impl_TCC22................proved - complete [O]( 0.15 s) condit_sum_adder_impl_TCC23................proved - complete [O]( 0.15 s) condit_sum_add_lem1........................proved - complete [O]( 0.35 s) condit_sum_adder_impl_correct..............proved - complete [O](27.59 s) Theory totals: 25 formulas, 25 attempted, 25 succeeded (32.28 s) Proof summary for theory adder_top Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory multiplier multiplier_stg1_TCC1........................proved - complete [O](0.15 s) multiplier_stg1_TCC2........................proved - complete [O](0.22 s) multiplier_stg1_TCC3........................proved - complete [O](0.17 s) multiplier_stg1_correct.....................proved - complete [O](4.00 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (4.54 s) Proof summary for theory multiplier_exp2 product_correct_TCC1........................proved - complete [O](0.13 s) product_correct.............................proved - complete [O](0.64 s) mult_addtr_impl_TCC1........................proved - complete [O](0.14 s) mult_addtr_impl_TCC2........................proved - complete [O](0.13 s) mult_addtr_impl_TCC3........................proved - complete [O](0.13 s) mult_addtr_impl_TCC4........................proved - complete [O](0.31 s) multiplier_impl_TCC1........................proved - complete [O](0.28 s) multiplier_impl_TCC2........................proved - complete [O](0.20 s) multiplier_exp2_correct.....................proved - complete [O](9.46 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (11.42 s) Proof summary for theory complete_42_adder_tree complete_42_adder_tree_TCC1................proved - complete [O]( 0.16 s) complete_42_adder_tree_TCC2................proved - complete [O]( 0.16 s) complete_42_adder_tree_TCC3................proved - complete [O]( 0.16 s) complete_42_adder_tree_TCC4................proved - complete [O]( 0.16 s) complete_42_adder_tree_TCC5................proved - complete [O]( 0.16 s) complete_42_adder_tree_TCC6................proved - complete [O]( 0.19 s) complete_42_adder_tree_TCC7................proved - complete [O]( 0.33 s) complete_42_adder_tree_TCC8................proved - complete [O]( 0.13 s) complete_42_adder_tree_TCC9................proved - complete [O]( 0.20 s) complete_42_adder_tree_TCC10...............proved - complete [O]( 0.23 s) complete_42_adder_tree_TCC11...............proved - complete [O]( 0.41 s) complete_42_adder_tree_TCC12...............proved - complete [O]( 0.14 s) complete_42_adder_tree_correct_TCC1........proved - complete [O]( 0.13 s) complete_42_adder_tree_correct_TCC2........proved - complete [O]( 0.21 s) complete_42_adder_tree_correct.............proved - complete [O](15.84 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (18.61 s) Proof summary for theory carry_save_adder carry_save_adder_impl_TCC1.................proved - complete [O]( 0.13 s) carry_save_adder_impl_TCC2.................proved - complete [O]( 0.13 s) carry_save_adder_impl_TCC3.................proved - complete [O]( 0.13 s) carry_save_adder_impl_TCC4.................proved - complete [O]( 0.13 s) carry_save_adder_impl_TCC5.................proved - complete [O]( 0.14 s) carry_save_adder_impl_TCC6.................proved - complete [O]( 0.14 s) carry_save_adder_impl_TCC7.................proved - complete [O]( 0.14 s) carry_save_adder_impl_TCC8.................proved - complete [O]( 0.12 s) carry_save_adder_impl_TCC9.................proved - complete [O]( 0.13 s) carry_save_adder_impl_TCC10................proved - complete [O]( 0.14 s) carry_save_adder_impl_TCC11................proved - complete [O]( 0.14 s) carry_save_adder_impl_TCC12................proved - complete [O]( 0.14 s) carry_save_adder_impl_correct..............proved - complete [O]( 9.85 s) carry_save_adder_impl_twoc.................proved - complete [O](24.61 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (36.07 s) Proof summary for theory carry_save_adder42 carry_save_adder42_impl_TCC1................proved - complete [O](0.13 s) carry_save_adder42_impl_TCC2................proved - complete [O](0.13 s) carry_save_adder42_impl_TCC3................proved - complete [O](0.14 s) carry_save_adder42_impl_TCC4................proved - complete [O](0.13 s) csa_annahm_correct..........................proved - complete [O](0.77 s) carry_save_adder42_impl_correct.............proved - complete [O](1.96 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (3.26 s) Proof summary for theory halfdecoder halfdecoder_tree_impl_TCC1..................proved - complete [O](0.13 s) halfdecoder_tree_impl_TCC2..................proved - complete [O](0.22 s) halfdecoder_tree_impl_TCC3..................proved - complete [O](0.14 s) halfdecoder_tree_impl_TCC4..................proved - complete [O](0.14 s) halfdecoder_tree_impl_TCC5..................proved - complete [O](0.14 s) halfdecoder_tree_impl_TCC6..................proved - complete [O](0.13 s) halfdecoder_tree_impl_TCC7..................proved - complete [O](0.14 s) halfdecoder_tree_impl_TCC8..................proved - complete [O](0.29 s) halfdecoder_tree_impl_TCC9..................proved - complete [O](0.15 s) halfdecoder_tree_impl_correct...............proved - complete [O](2.17 s) halfdecoder_impl_TCC1.......................proved - complete [O](0.14 s) halfdecoder_impl_correct....................proved - complete [O](0.21 s) hdec_lem_TCC1...............................proved - complete [O](0.18 s) hdec_lem....................................proved - complete [O](0.33 s) halfdecoder_impl_correct2_TCC1..............proved - complete [O](0.26 s) halfdecoder_impl_correct2...................proved - complete [O](0.30 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (5.07 s) Proof summary for theory decoder decoder_tree_impl_TCC1......................proved - complete [O](0.13 s) decoder_tree_impl_TCC2......................proved - complete [O](0.22 s) decoder_tree_impl_TCC3......................proved - complete [O](0.14 s) decoder_tree_impl_TCC4......................proved - complete [O](0.14 s) decoder_tree_impl_TCC5......................proved - complete [O](0.13 s) decoder_tree_impl_TCC6......................proved - complete [O](0.17 s) decoder_tree_impl_TCC7......................proved - complete [O](0.30 s) decoder_tree_impl_TCC8......................proved - complete [O](0.13 s) decoder_tree_impl_TCC9......................proved - complete [O](0.29 s) decoder_tree_impl_TCC10.....................proved - complete [O](0.14 s) decoder_tree_impl_TCC11.....................proved - complete [O](0.56 s) decoder_tree_impl_TCC12.....................proved - complete [O](0.65 s) decoder_tree_impl_TCC13.....................proved - complete [O](0.57 s) decoder_tree_impl_TCC14.....................proved - complete [O](0.66 s) decoder_tree_impl_correct...................proved - complete [O](3.30 s) decoder_impl_TCC1...........................proved - complete [O](0.14 s) decoder_impl_correct........................proved - complete [O](0.21 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (7.88 s) Proof summary for theory encoder_decoder dec_enc_theorem_TCC1........................proved - complete [O](0.12 s) dec_enc_theorem_TCC2........................proved - complete [O](0.17 s) dec_enc_theorem.............................proved - complete [O](1.26 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.55 s) Proof summary for theory encoder_rec encf_rec_TCC1...............................proved - complete [O](0.20 s) encf_rec_TCC2...............................proved - complete [O](0.18 s) encf_rec_TCC3...............................proved - complete [O](0.16 s) encf_rec_TCC4...............................proved - complete [O](0.17 s) encf_rec_TCC5...............................proved - complete [O](0.38 s) encf_rec_TCC6...............................proved - complete [O](0.13 s) encf_rec_TCC7...............................proved - complete [O](0.20 s) encf_rec_TCC8...............................proved - complete [O](0.13 s) encf_rec_TCC9...............................proved - complete [O](0.30 s) encf_rec_TCC10..............................proved - complete [O](0.35 s) encf_rec_TCC11..............................proved - complete [O](0.60 s) encf_rec_TCC12..............................proved - complete [O](0.53 s) encf_rec_TCC13..............................proved - complete [O](0.14 s) encf_rec_TCC14..............................proved - complete [O](0.46 s) encf_rec_TCC15..............................proved - complete [O](0.46 s) enc_rec_TCC1................................proved - complete [O](0.29 s) enc_rec_TCC2................................proved - complete [O](0.61 s) enc_rec_TCC3................................proved - complete [O](0.53 s) enc_rec_TCC4................................proved - complete [O](0.52 s) enc_rec_TCC5................................proved - complete [O](0.45 s) enc_rec_TCC6................................proved - complete [O](0.45 s) encf_lemma1.................................proved - complete [O](1.79 s) encf_lemma2.................................proved - complete [O](1.56 s) encf_lemma3.................................proved - complete [O](6.47 s) enc_lemma0..................................proved - complete [O](3.45 s) enc_lemma1..................................proved - complete [O](4.78 s) enc_lemma...................................proved - complete [O](0.30 s) Theory totals: 27 formulas, 27 attempted, 27 succeeded (25.59 s) Proof summary for theory encoder encoderf_impl_TCC1..........................proved - complete [O](0.15 s) encoderf_impl_TCC2..........................proved - complete [O](0.16 s) encf_theorem................................proved - complete [O](2.24 s) encf_ortree_theorem.........................proved - complete [O](0.78 s) enc_theorem.................................proved - complete [O](9.55 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (12.88 s) Proof summary for theory lzero_exp2_impl lzero_plus_exp2_TCC1.......................proved - complete [O]( 0.13 s) lzero_plus_exp2_TCC2.......................proved - complete [O]( 0.12 s) lzero_plus_exp2_TCC3.......................proved - complete [O]( 0.13 s) lzero_plus_exp2_TCC4.......................proved - complete [O]( 0.13 s) lzero_plus_exp2............................proved - complete [O]( 2.50 s) lzero_exp2_impl_TCC1.......................proved - complete [O]( 0.13 s) lzero_exp2_impl_TCC2.......................proved - complete [O]( 0.14 s) lzero_exp2_impl_TCC3.......................proved - complete [O]( 0.17 s) lzero_exp2_impl_TCC4.......................proved - complete [O]( 0.14 s) lzero_exp2_impl_TCC5.......................proved - complete [O]( 0.21 s) lzero_exp2_impl_TCC6.......................proved - complete [O]( 0.17 s) lzero_exp2_impl_TCC7.......................proved - complete [O]( 0.14 s) lzero_exp2_impl_TCC8.......................proved - complete [O]( 0.17 s) lzero_exp2_impl_TCC9.......................proved - complete [O]( 1.49 s) lzero_exp2_impl_TCC10......................proved - complete [O]( 0.32 s) lzero_exp2_impl_TCC11......................proved - complete [O]( 0.13 s) lzero_exp2_impl_TCC12......................proved - complete [O]( 0.25 s) lzero_exp2_impl_TCC13......................proved - complete [O]( 0.50 s) lzero_exp2_impl_TCC14......................proved - complete [O]( 0.29 s) lzero_exp2_impl_TCC15......................proved - complete [O]( 0.13 s) lzero_exp2_impl_TCC16......................proved - complete [O]( 0.33 s) lzero_exp2_impl_TCC17......................proved - complete [O]( 0.33 s) lzero_exp2_impl_TCC18......................proved - complete [O]( 0.33 s) lzero_exp2_impl_TCC19......................proved - complete [O]( 0.32 s) lzero_exp2_impl_TCC20......................proved - complete [O]( 0.33 s) lzero_exp2_impl_correct_TCC1...............proved - complete [O]( 0.29 s) lzero_exp2_impl_correct....................proved - complete [O](30.15 s) Theory totals: 27 formulas, 27 attempted, 27 succeeded (39.47 s) Proof summary for theory lzero_concat lzero_concat1_TCC1.........................proved - complete [O]( 0.36 s) lzero_concat1_TCC2.........................proved - complete [O]( 0.16 s) lzero_concat1..............................proved - complete [O](15.85 s) lzero_concat4_TCC1.........................proved - complete [O]( 0.15 s) lzero_concat4_TCC2.........................proved - complete [O]( 0.15 s) lzero_concat4..............................proved - complete [O]( 2.55 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (19.22 s) Proof summary for theory lzero_concat2 lzero_concat0_TCC1..........................proved - complete [O](0.13 s) lzero_concat0_TCC2..........................proved - complete [O](0.22 s) lzero_concat0...............................proved - complete [O](1.88 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (2.23 s) Proof summary for theory lzero lzero_TCC_TCC1..............................proved - complete [O](0.14 s) lzero_TCC_TCC2..............................proved - complete [O](0.15 s) lzero_TCC_TCC3..............................proved - complete [O](0.18 s) lzero_TCC_TCC4..............................proved - complete [O](0.18 s) lzero_TCC...................................proved - complete [O](1.04 s) lzero_TCC1..................................proved - complete [O](0.12 s) lzero_TCC2..................................proved - complete [O](0.36 s) lzero_bound.................................proved - complete [O](1.24 s) lzero_lem1_TCC1.............................proved - complete [O](0.13 s) lzero_lem1_TCC2.............................proved - complete [O](0.13 s) lzero_lem1_TCC3.............................proved - complete [O](0.13 s) lzero_lem1_TCC4.............................proved - complete [O](0.13 s) lzero_lem1_TCC5.............................proved - complete [O](0.13 s) lzero_lem1..................................proved - complete [O](5.37 s) lzero_lem2_TCC1.............................proved - complete [O](0.13 s) lzero_lem2_TCC2.............................proved - complete [O](0.13 s) lzero_lem2_TCC3.............................proved - complete [O](0.13 s) lzero_lem2..................................proved - complete [O](2.30 s) lzero_lem3..................................proved - complete [O](3.43 s) lzero_lem4..................................proved - complete [O](1.94 s) lzero_bvnat_TCC1............................proved - complete [O](0.20 s) lzero_bvnat_TCC2............................proved - complete [O](0.19 s) lzero_bvnat_TCC3............................proved - complete [O](0.16 s) lzero_bvnat.................................proved - complete [O](4.67 s) lzero_bit...................................proved - complete [O](1.67 s) Theory totals: 25 formulas, 25 attempted, 25 succeeded (24.38 s) Proof summary for theory lzero_log IMP_lzero_TCC1..............................proved - complete [O](0.12 s) lzero_computes_log_TCC1.....................proved - complete [O](0.16 s) lzero_computes_log..........................proved - complete [O](6.53 s) lzero_computes_log_vv.......................proved - complete [O](0.23 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (7.04 s) Proof summary for theory lzero_impl lzero_impl_TCC1............................proved - complete [O]( 0.14 s) lzero_impl_TCC2............................proved - complete [O]( 0.13 s) lzero_impl_TCC3............................proved - complete [O]( 0.16 s) lzero_impl_TCC4............................proved - complete [O]( 0.14 s) lzero_impl_TCC5............................proved - complete [O]( 0.14 s) lzero_impl_correct_TCC1....................proved - complete [O]( 0.12 s) lzero_impl_correct.........................proved - complete [O](11.16 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (11.99 s) Proof summary for theory pp_rec pp_rec_TCC1.................................proved - complete [O](0.13 s) pp_rec_TCC2.................................proved - complete [O](0.19 s) pp_rec_TCC3.................................proved - complete [O](0.27 s) pp_rec_TCC4.................................proved - complete [O](0.14 s) pp_rec_TCC5.................................proved - complete [O](0.17 s) pp_rec_TCC6.................................proved - complete [O](0.14 s) pp_rec_TCC7.................................proved - complete [O](0.17 s) pp_rec_TCC8.................................proved - complete [O](0.56 s) pp_rec_TCC9.................................proved - complete [O](0.43 s) pp_lemma_TCC1...............................proved - complete [O](0.13 s) pp_lemma....................................proved - complete [O](2.07 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (4.40 s) Proof summary for theory pp pp_theorem_TCC1.............................proved - complete [O](0.15 s) pp_theorem..................................proved - complete [O](0.21 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.36 s) Proof summary for theory shifter cls_func_TCC1..............................proved - complete [O]( 0.19 s) cls_func_TCC2..............................proved - complete [O]( 0.61 s) cls_func_TCC3..............................proved - complete [O]( 0.16 s) cls_func_TCC4..............................proved - complete [O]( 0.17 s) cls_func_TCC5..............................proved - complete [O]( 0.16 s) cls_func_TCC6..............................proved - complete [O]( 0.18 s) cls_stage_impl_is_func_TCC1................proved - complete [O]( 0.18 s) cls_stage_impl_is_func.....................proved - complete [O]( 1.07 s) cls_stage_impl_test_TCC1...................proved - complete [O]( 0.14 s) cls_stage_impl_test........................proved - complete [O]( 0.36 s) cls_combine................................proved - complete [O](11.94 s) cls_rec_impl_TCC1..........................proved - complete [O]( 0.22 s) cls_rec_impl_TCC2..........................proved - complete [O]( 0.13 s) cls_rec_impl_TCC3..........................proved - complete [O]( 0.15 s) cls_rec_impl_TCC4..........................proved - complete [O]( 0.14 s) cls_rec_impl_TCC5..........................proved - complete [O]( 0.17 s) cls_rec_impl_correct_TCC1..................proved - complete [O]( 0.13 s) cls_rec_impl_correct_TCC2..................proved - complete [O]( 0.42 s) cls_rec_impl_correct.......................proved - complete [O]( 3.88 s) cls_impl_TCC1..............................proved - complete [O]( 0.13 s) cls_impl_correct_TCC1......................proved - complete [O]( 0.19 s) cls_impl_correct...........................proved - complete [O]( 0.46 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (21.18 s) Proof summary for theory logic_left_shifter lls_stage_impl_TCC1.........................proved - complete [O](0.13 s) lls_stage_impl_TCC2.........................proved - complete [O](0.13 s) lls_stage_impl_TCC3.........................proved - complete [O](0.13 s) lls_stage_impl_is_leftshift.................proved - complete [O](1.31 s) lls_rec_impl_TCC1...........................proved - complete [O](0.13 s) lls_rec_impl_TCC2...........................proved - complete [O](0.14 s) lls_rec_impl_TCC3...........................proved - complete [O](0.14 s) lls_rec_impl_TCC4...........................proved - complete [O](0.13 s) lls_rec_impl_TCC5...........................proved - complete [O](0.19 s) lls_rec_impl_correct_TCC1...................proved - complete [O](0.12 s) lls_rec_impl_correct........................proved - complete [O](7.85 s) lls_impl_TCC1...............................proved - complete [O](0.13 s) lls_impl_correct............................proved - complete [O](0.27 s) lls_arith_TCC1..............................proved - complete [O](0.15 s) lls_arith_TCC2..............................proved - complete [O](0.14 s) lls_arith_TCC3..............................proved - complete [O](0.15 s) lls_arith...................................proved - complete [O](1.10 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (12.34 s) Proof summary for theory logic_right_shifter lrs_stage_impl_TCC1.........................proved - complete [O](0.13 s) lrs_stage_impl_TCC2.........................proved - complete [O](0.12 s) lrs_stage_impl_TCC3.........................proved - complete [O](0.12 s) lrs_rec_impl_TCC1...........................proved - complete [O](0.13 s) lrs_rec_impl_TCC2...........................proved - complete [O](0.14 s) lrs_rec_impl_TCC3...........................proved - complete [O](0.14 s) lrs_rec_impl_TCC4...........................proved - complete [O](0.13 s) lrs_rec_impl_TCC5...........................proved - complete [O](0.18 s) lrs_rec_impl_correct_TCC1...................proved - complete [O](0.12 s) lrs_rec_impl_correct........................proved - complete [O](5.56 s) lrs_impl_TCC1...............................proved - complete [O](0.13 s) lrs_impl_correct............................proved - complete [O](0.27 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (7.17 s) Proof summary for theory zero zero_correct................................proved - complete [O](0.13 s) zero_impl_correct...........................proved - complete [O](0.16 s) one_impl_correct............................proved - complete [O](0.30 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.59 s) Proof summary for theory equal equal_impl_correct..........................proved - complete [O](0.42 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.42 s) Proof summary for theory mult_lin mult_lin_TCC1...............................proved - complete [O](0.14 s) mult_lin_TCC2...............................proved - complete [O](0.13 s) mult_lin_TCC3...............................proved - complete [O](0.23 s) mult_lin_TCC4...............................proved - complete [O](0.18 s) mult_lin_TCC5...............................proved - complete [O](0.17 s) mult_lin_TCC6...............................proved - complete [O](0.17 s) mult_lin_TCC7...............................proved - complete [O](0.14 s) mult_lin_TCC8...............................proved - complete [O](0.14 s) mult_lin_TCC9...............................proved - complete [O](0.15 s) mult_lin_TCC10..............................proved - complete [O](0.14 s) mult_lin_TCC11..............................proved - complete [O](0.13 s) mult_lin_TCC12..............................proved - complete [O](0.32 s) mult_lin_TCC13..............................proved - complete [O](0.32 s) mult_lin_TCC14..............................proved - complete [O](0.15 s) mult_lin_correct............................proved - complete [O](3.44 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (5.95 s) Proof summary for theory vectorand vectorand_correct...........................proved - complete [O](0.25 s) vectorand_bv2nat............................proved - complete [O](0.32 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.57 s) Proof summary for theory basicsub basicsub_impl_TCC1..........................proved - complete [O](0.14 s) basicsub_impl_correct.......................proved - complete [O](0.98 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.12 s) Proof summary for theory sub sub_impl_correct_binsum.....................proved - complete [O](0.38 s) sub_impl_correct_intsum.....................proved - complete [O](0.28 s) sub_impl_correct_ovf........................proved - complete [O](0.22 s) sub_impl_correct_neg........................proved - complete [O](0.22 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (1.10 s) Proof summary for theory add_sub add_sub_impl_correct_binsum.................proved - complete [O](2.18 s) add_sub_impl_correct_intsum.................proved - complete [O](0.88 s) add_sub_impl_correct_ovf....................proved - complete [O](0.70 s) add_sub_impl_correct_neg....................proved - complete [O](0.63 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (4.39 s) Proof summary for theory sext sext_impl_TCC1..............................proved - complete [O](0.13 s) sext_impl_TCC2..............................proved - complete [O](0.13 s) sext_impl_is_sext...........................proved - complete [O](0.34 s) sext_impl_preserves_value...................proved - complete [O](0.21 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.81 s) Proof summary for theory mult_karatsuba mult_karatsuba_t_TCC1......................proved - complete [O]( 0.14 s) mult_karatsuba_stg1_TCC1...................proved - complete [O]( 0.14 s) mult_karatsuba_stg1_TCC2...................proved - complete [O]( 0.15 s) mult_karatsuba_stg1_TCC3...................proved - complete [O]( 0.15 s) mult_karatsuba_stg1_TCC4...................proved - complete [O]( 0.18 s) mult_karatsuba_stg1_TCC5...................proved - complete [O]( 0.22 s) mult_karatsuba_stg1_TCC6...................proved - complete [O]( 0.15 s) mult_karatsuba_stg1_TCC7...................proved - complete [O]( 0.16 s) mult_karatsuba_stg1_TCC8...................proved - complete [O]( 0.24 s) mult_karatsuba_stg1_TCC9...................proved - complete [O]( 0.28 s) mult_karatsuba_stg2_TCC1...................proved - complete [O]( 0.24 s) mult_karatsuba_stg2_TCC2...................proved - complete [O]( 0.18 s) mult_karatsuba_stg2_TCC3...................proved - complete [O]( 0.22 s) mult_karatsuba_stg2_TCC4...................proved - complete [O]( 0.22 s) mult_karatsuba_stg2_TCC5...................proved - complete [O]( 0.68 s) mult_karatsuba_stg2_TCC6...................proved - complete [O]( 0.25 s) mult_karatsuba_stg2_TCC7...................proved - complete [O]( 0.67 s) mult_karatsuba_stg2_TCC8...................proved - complete [O]( 2.31 s) mult_karatsuba_stg2_TCC9...................proved - complete [O]( 2.31 s) mult_karatsuba_correct.....................proved - complete [O](20.51 s) Theory totals: 20 formulas, 20 attempted, 20 succeeded (29.40 s) Proof summary for theory mux_tree_rec mux_tree_rec_TCC1...........................proved - complete [O](0.16 s) mux_tree_rec_TCC2...........................proved - complete [O](0.20 s) mux_tree_rec_TCC3...........................proved - complete [O](0.12 s) mux_tree_rec_TCC4...........................proved - complete [O](0.24 s) mux_tree_rec_TCC5...........................proved - complete [O](0.38 s) mux_tree_rec_TCC6...........................proved - complete [O](0.27 s) mux_tree_rec_TCC7...........................proved - complete [O](0.27 s) mux_tree_rec_TCC8...........................proved - complete [O](0.36 s) mux_tree_rec_TCC9...........................proved - complete [O](0.38 s) mux_tree_rec_TCC10..........................proved - complete [O](0.14 s) mux_tree_rec_TCC11..........................proved - complete [O](0.38 s) mux_tree_rec_TCC12..........................proved - complete [O](0.41 s) mux_tree_rec_TCC13..........................proved - complete [O](0.15 s) mux_tree_rec_TCC14..........................proved - complete [O](0.15 s) mux_tree_rec_correct_TCC1...................proved - complete [O](0.18 s) mux_tree_rec_correct........................proved - complete [O](1.81 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (5.60 s) Proof summary for theory mux mux_impl_correct............................proved - complete [O](0.15 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.15 s) Proof summary for theory mux_tree mux_tree_impl_correct.......................proved - complete [O](0.25 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.25 s) Proof summary for theory or_ or_linear_impl_TCC1.........................proved - complete [O](0.12 s) or_linear_impl_TCC2.........................proved - complete [O](0.13 s) or_linear_impl_TCC3.........................proved - complete [O](0.16 s) or_linear_impl_TCC4.........................proved - complete [O](0.13 s) or_linear_impl_TCC5.........................proved - complete [O](0.16 s) or_linear_impl_TCC6.........................proved - complete [O](0.13 s) or_linear_impl_correct......................proved - complete [O](0.93 s) or_tree_impl_TCC1...........................proved - complete [O](0.14 s) or_tree_impl_TCC2...........................proved - complete [O](0.18 s) or_tree_impl_TCC3...........................proved - complete [O](0.14 s) or_tree_impl_TCC4...........................proved - complete [O](0.20 s) or_tree_impl_TCC5...........................proved - complete [O](0.28 s) or_tree_impl_TCC6...........................proved - complete [O](0.29 s) or_tree_impl_TCC7...........................proved - complete [O](0.28 s) or_tree_impl_TCC8...........................proved - complete [O](0.14 s) or_tree_impl_correct........................proved - complete [O](1.58 s) or_impl_correct.............................proved - complete [O](0.15 s) or_impl_correct2............................proved - complete [O](0.15 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (5.29 s) Proof summary for theory mux_tree_unary_select mux_tree_unary_select_correct...............proved - complete [O](0.60 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.60 s) Proof summary for theory incrementer incr_impl_TCC1..............................proved - complete [O](0.13 s) incr_impl_correct...........................proved - complete [O](0.23 s) incr_topbit_TCC1............................proved - complete [O](0.13 s) incr_topbit.................................proved - complete [O](0.67 s) incr_vs_adder_TCC1..........................proved - complete [O](0.15 s) incr_vs_adder_TCC2..........................proved - complete [O](0.13 s) incr_vs_adder...............................proved - complete [O](0.55 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.99 s) Proof summary for theory carry_chain_inc carry_chain_inc_impl_TCC1...................proved - complete [O](0.13 s) carry_chain_inc_impl_TCC2...................proved - complete [O](0.13 s) carry_chain_inc_impl_TCC3...................proved - complete [O](0.16 s) carry_chain_inc_impl_TCC4...................proved - complete [O](0.14 s) carry_chain_inc_impl_TCC5...................proved - complete [O](0.14 s) carry_chain_inc_impl_TCC6...................proved - complete [O](0.14 s) carry_chain_inc_impl_TCC7...................proved - complete [O](0.12 s) carry_chain_inc_impl_TCC8...................proved - complete [O](0.13 s) carry_chain_inc_impl_TCC9...................proved - complete [O](0.23 s) carry_chain_inc_impl_TCC10..................proved - complete [O](0.23 s) carry_chain_inc_impl_TCC11..................proved - complete [O](0.13 s) carry_chain_inc_impl_correct................proved - complete [O](2.68 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (4.36 s) Proof summary for theory halfadder halfadder_impl_correct......................proved - complete [O](0.27 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.27 s) Proof summary for theory add IMP_adder_TCC1..............................proved - complete [O](0.17 s) add_impl_TCC1...............................proved - complete [O](0.13 s) add_impl_TCC2...............................proved - complete [O](0.15 s) add_impl_TCC3...............................proved - complete [O](0.15 s) add_impl_TCC4...............................proved - complete [O](0.15 s) add_is_adder................................proved - complete [O](0.26 s) add_impl_correct............................proved - complete [O](0.87 s) add_impl_correct_sum........................proved - complete [O](0.61 s) add_impl_correct_intsum.....................proved - complete [O](0.82 s) add_impl_correct_ovf........................proved - complete [O](0.81 s) add_impl_correct_neg........................proved - complete [O](0.82 s) add_impl_binsum.............................proved - complete [O](0.76 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (5.70 s) Proof summary for theory basicadder basicadder_impl_TCC1........................proved - complete [O](0.14 s) basicadder_impl_correct.....................proved - complete [O](0.22 s) basicadder_topbit_TCC1......................proved - complete [O](0.13 s) basicadder_topbit_TCC2......................proved - complete [O](0.14 s) basicadder_topbit_TCC3......................proved - complete [O](0.15 s) basicadder_topbit...........................proved - complete [O](3.06 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (3.84 s) Proof summary for theory carry_chain carry_chain_impl_TCC1.......................proved - complete [O](0.13 s) carry_chain_impl_TCC2.......................proved - complete [O](0.12 s) carry_chain_impl_TCC3.......................proved - complete [O](0.17 s) carry_chain_impl_TCC4.......................proved - complete [O](0.14 s) carry_chain_impl_TCC5.......................proved - complete [O](0.14 s) carry_chain_impl_TCC6.......................proved - complete [O](0.14 s) carry_chain_impl_TCC7.......................proved - complete [O](0.13 s) carry_chain_impl_TCC8.......................proved - complete [O](0.13 s) carry_chain_impl_TCC9.......................proved - complete [O](0.29 s) carry_chain_impl_TCC10......................proved - complete [O](0.29 s) carry_chain_impl_TCC11......................proved - complete [O](0.13 s) carry_chain_impl_correct....................proved - complete [O](5.31 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (7.12 s) Proof summary for theory adder ADD_TCC1....................................proved - complete [O](0.14 s) IMP_adder_lem_TCC1..........................proved - complete [O](0.16 s) adder_impl_TCC1.............................proved - complete [O](0.13 s) adder_impl_TCC2.............................proved - complete [O](0.15 s) adder_impl_TCC3.............................proved - complete [O](0.15 s) adder_impl_TCC4.............................proved - complete [O](0.15 s) adder_impl_correct..........................proved - complete [O](6.26 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (7.14 s) Proof summary for theory fulladder fulladder_impl_correct......................proved - complete [O](0.38 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.38 s) Proof summary for theory basics_import IMP_finite_sets_minmax_TCC1.................proved - complete [O](0.36 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.36 s) Proof summary for theory adder_lem ADD_TCC1....................................proved - complete [O](0.14 s) adder_lem1_TCC1.............................proved - complete [O](0.13 s) adder_lem1_TCC2.............................proved - complete [O](0.14 s) adder_lem1_TCC3.............................proved - complete [O](0.15 s) adder_lem1..................................proved - complete [O](3.03 s) adder_xor_lem_TCC1..........................proved - complete [O](0.14 s) adder_xor_lem_TCC2..........................proved - complete [O](0.15 s) adder_xor_lem_TCC3..........................proved - complete [O](0.13 s) adder_xor_lem...............................proved - complete [O](3.71 s) bv2int_in_rng_2s_comp_TCC1..................proved - complete [O](0.12 s) bv2int_in_rng_2s_comp_TCC2..................proved - complete [O](0.12 s) bv2int_in_rng_2s_comp_TCC3..................proved - complete [O](0.13 s) bv2int_in_rng_2s_comp.......................proved - complete [O](1.71 s) bv2int_ovf..................................proved - complete [O](0.56 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (10.36 s) Proof summary for theory neg neg_impl_TCC1...............................proved - complete [O](0.15 s) neg_impl_TCC2...............................proved - complete [O](0.13 s) neg_impl_correct............................proved - complete [O](0.44 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.72 s) Proof summary for theory basics Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Grand Totals: 471 proofs, 471 attempted, 471 succeeded (451.05 s)