From 3205f0d406e65454360fff49f06dad85787689a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 25 Sep 2020 11:16:34 -0700 Subject: [PATCH] use default in model construction Signed-off-by: Nikolaj Bjorner --- src/sat/smt/array_model.cpp | 2 -- src/sat/smt/bv_delay_internalize.cpp | 8 +++++--- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp index 39e648a36..a9c06e698 100644 --- a/src/sat/smt/array_model.cpp +++ b/src/sat/smt/array_model.cpp @@ -66,7 +66,6 @@ namespace array { if (!fi->get_else()) { expr* else_value = nullptr; - unsigned max_occ_num = 0; obj_map num_occ; for (euf::enode* p : euf::enode_parents(n)) { @@ -84,7 +83,6 @@ namespace array { } } } - if (else_value) fi->set_else(else_value); } diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp index 6af9ffcf9..a18bbd2b6 100644 --- a/src/sat/smt/bv_delay_internalize.cpp +++ b/src/sat/smt/bv_delay_internalize.cpp @@ -77,6 +77,7 @@ namespace bv { if (!check_mul_one(e, args, r1, r2)) return false; + // Add propagation axiom for arguments if (!check_mul_invertibility(e, args, r1)) return false; @@ -157,6 +158,7 @@ namespace bv { return ok; } + /* * Check that multiplication with 0 is correctly propagated. * If not, create algebraic axioms enforcing 0*x = 0 and x*0 = 0 @@ -423,9 +425,9 @@ namespace bv { internalize_mode mode; switch (to_app(e)->get_decl_kind()) { case OP_BMUL: - case OP_BSMUL_NO_OVFL: - case OP_BSMUL_NO_UDFL: - case OP_BUMUL_NO_OVFL: + //case OP_BSMUL_NO_OVFL: + //case OP_BSMUL_NO_UDFL: + //case OP_BUMUL_NO_OVFL: case OP_BSMOD_I: case OP_BUREM_I: case OP_BSREM_I: