3 files changed, 29 insertions, 2 deletions
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 954f921ce..30441a8f4 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -148,7 +148,10 @@ void IAndSolver::checkFullRefine()
       // ************* additional lemma schemas go here
       if (options::iandMode() == options::IandMode::SUM)
       {
-        // add lemmas based on sum mode
+        Node lem = sumBasedLemma(i);  // add lemmas based on sum mode
+        Trace("iand-lemma")
+            << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl;
+        d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_SUM_REFINE, true);
       }
       else if (options::iandMode() == options::IandMode::BITWISE)
       {
@@ -245,6 +248,18 @@ Node IAndSolver::valueBasedLemma(Node i)
   return lem;
 }
 
+Node IAndSolver::sumBasedLemma(Node i)
+{
+  Assert(i.getKind() == IAND);
+  Node x = i[0];
+  Node y = i[1];
+  size_t bvsize = i.getOperator().getConst<IntAnd>().d_size;
+  uint64_t granularity = options::BVAndIntegerGranularity();
+  NodeManager* nm = NodeManager::currentNM();
+  Node lem = nm->mkNode(
+      EQUAL, i, d_iandTable.createBitwiseNode(x, y, bvsize, granularity));
+  return lem;
+}
 
 }  // namespace nl
 }  // namespace arith
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index d74365784..e00cb92a9 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -22,6 +22,7 @@
 #include "expr/node.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/iand_table.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/nl_model.h"
 
@@ -88,6 +89,7 @@ class IAndSolver
   Node d_two;
   Node d_true;
   Node d_false;
+  IAndTable d_iandTable;
   /** IAND terms that have been given initial refinement lemmas */
   NodeSet d_initRefine;
   /** all IAND terms, for each bit-width */
@@ -118,6 +120,13 @@ class IAndSolver
    *     ((_ iand k) x y) = Rewriter::rewrite(((_ iand k) M(x) M(y)))
    */
   Node valueBasedLemma(Node i);
+  /**
+   * Sum-based refinement lemma for i of the form ((_ iand k) x y). Returns:
+   * i = 2^0*min(x[0],y[0])+...2^{k-1}*min(x[k-1],y[k-1])
+   * where x[i] is x div i mod 2
+   * and min is defined with an ite.
+   */
+  Node sumBasedLemma(Node i);
 }; /* class IAndSolver */
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/iand_table.cpp b/src/theory/arith/nl/iand_table.cpp
index 12e06ed58..050e6baed 100644
--- a/src/theory/arith/nl/iand_table.cpp
+++ b/src/theory/arith/nl/iand_table.cpp
@@ -198,7 +198,7 @@ void IAndTable::addDefaultValue(
   }
 
   // compute the most common result
-  uint64_t most_common_result;
+  uint64_t most_common_result = 0;
   uint64_t max_num_of_occ = 0;
   for (uint64_t i = 0; i <= num_of_values; i++)
   {
@@ -208,6 +208,9 @@ void IAndTable::addDefaultValue(
       most_common_result = i;
     }
   }
+  // sanity check: some value appears at least once.
+  Assert(max_num_of_occ != 0);
+
   // -1 is the default case of the table.
   // add it to the table
   table[std::make_pair(-1, -1)] = most_common_result;