From 81c3966331c13920d1641f19a06ee01eebf56f19 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 29 Sep 2020 13:39:59 -0700
Subject: [PATCH] merge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/bv_delay_internalize.cpp | 13 +++++++++----
 src/sat/smt/bv_solver.cpp            |  1 +
 src/sat/smt/bv_solver.h              |  1 +
 3 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp
index a18bbd2b6..87f198dc5 100644
--- a/src/sat/smt/bv_delay_internalize.cpp
+++ b/src/sat/smt/bv_delay_internalize.cpp
@@ -77,7 +77,6 @@ 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;
@@ -159,19 +158,23 @@ namespace bv {
     }
 
 
+
     /*
     * Check that multiplication with 0 is correctly propagated.
     * If not, create algebraic axioms enforcing 0*x = 0 and x*0 = 0
     * 
     * z = 0, then lsb(x) + 1 + lsb(y) + 1 >= sz
+
     */
     bool solver::check_mul_zero(app* n, expr_ref_vector const& arg_values, expr* mul_value, expr* arg_value) {
         SASSERT(mul_value != arg_value);
         SASSERT(!(bv.is_zero(mul_value) && bv.is_zero(arg_value)));
+
         if (bv.is_zero(arg_value)) {
             unsigned sz = n->get_num_args();
             expr_ref_vector args(m, sz, n->get_args());
             for (unsigned i = 0; i < sz && !s().inconsistent(); ++i) {
+
                 args[i] = arg_value;
                 expr_ref r(m.mk_app(n->get_decl(), args), m);
                 set_delay_internalize(r, internalize_mode::init_bits_only_i); // do not bit-blast this multiplier.
@@ -318,6 +321,7 @@ namespace bv {
     };
 
     /**
+
      * The i'th bit in xs is 1 if the least significant bit of x is i or lower.
      */
     void solver::encode_lsb_tail(expr* x, expr_ref_vector& xs) {
@@ -384,6 +388,7 @@ namespace bv {
         auto r2 = eval_args(n, args);
         if (r1 == r2)
             return true;
+
         if (m_cheap_axioms)
             return true;
         set_delay_internalize(a, internalize_mode::no_delay_i);
@@ -425,9 +430,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:
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index d09affb91..eb3cbe10d 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -500,6 +500,7 @@ namespace bv {
         svector<std::pair<expr*, internalize_mode>> delay;
         for (auto kv : m_delay_internalize)
             delay.push_back(std::make_pair(kv.m_key, kv.m_value));
+
         flet<bool> _cheap1(m_cheap_axioms, true);
         for (auto kv : delay) 
             if (!check_delay_internalized(kv.first))
diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h
index d3deea85d..d55a23b1b 100644
--- a/src/sat/smt/bv_solver.h
+++ b/src/sat/smt/bv_solver.h
@@ -272,6 +272,7 @@ namespace bv {
         bool check_mul_zero(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2);
         bool check_mul_one(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2);
         bool check_mul_low_bits(app* n, expr_ref_vector const& arg_values, expr* value1, expr* value2);
+
         bool check_umul_no_overflow(app* n, expr_ref_vector const& arg_values, expr* value);
         bool check_bv_eval(euf::enode* n);
         bool check_bool_eval(euf::enode* n);