5 files changed, 34 insertions, 9 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 13791bfd6..80183b71f 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -639,11 +639,26 @@ header = "options/smt_options.h"
 [[option]]
   name       = "solveBVAsInt"
   category   = "undocumented"
-  long       = "solve-bv-as-int=N"
+  long       = "solve-bv-as-int=MODE"
+  type       = "SolveBVAsIntMode"
+  default    = "OFF"
+  help       = "mode for translating BVAnd to integer"
+  help_mode  = "solve-bv-as-int modes."
+[[option.mode.OFF]]
+  name = "off"
+  help = "Do not translate bit-vectors to integers"
+[[option.mode.SUM]]
+  name = "sum"
+  help = "Generate a sum expression for each bvand instance, based on the value in --solbv-bv-as-int-granularity"
+
+[[option]]
+  name       = "BVAndIntegerGranularity"
+  category   = "undocumented"
+  long       = "bvand-integer-granularity=N"
   type       = "uint32_t"
-  default    = "0"
+  default    = "1"
   read_only  = true
-  help       = "attempt to solve BV formulas by translation to integer arithmetic (experimental)"
+  help       = "granularity to use in --solve-bv-as-int mode and for iand operator (experimental)"
 
 [[option]]
   name       = "iandMode"
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 5b125b4b6..bb0bde2f9 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -269,7 +269,7 @@ Node BVToInt::bvToInt(Node n)
   n = makeBinary(n);
   vector<Node> toVisit;
   toVisit.push_back(n);
-  uint64_t granularity = options::solveBVAsInt();
+  uint64_t granularity = options::BVAndIntegerGranularity();
 
   while (!toVisit.empty())
   {
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 4eedfd863..4fed33f3c 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -222,7 +222,7 @@ bool ProcessAssertions::apply(AssertionPipeline& assertions)
   {
     d_passes["bv-to-bool"]->apply(&assertions);
   }
-  if (options::solveBVAsInt() > 0)
+  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
   {
     d_passes["bv-to-int"]->apply(&assertions);
   }
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 4ce4b8db8..11751079e 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -154,7 +154,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     logic.lock();
   }
 
-  if (options::solveBVAsInt() > 0)
+  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
   {
     // not compatible with incremental
     if (options::incrementalSolving())
@@ -168,7 +168,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
       throw OptionException(
           "solving bitvectors as integers is incompatible with --bool-to-bv.");
     }
-    if (options::solveBVAsInt() > 8)
+    if (options::BVAndIntegerGranularity() > 8)
     {
       /**
        * The granularity sets the size of the ITE in each element
@@ -382,7 +382,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   }
 
 
-  if (options::solveBVAsInt() > 0)
+  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
   {
     /**
      * Operations on 1 bits are better handled as Boolean operations
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 851ae414e..2bbdcceb3 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1787,6 +1787,8 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
           new std::set<Node>(proofRecipe->getStep(0)->getAssertions()));
     }
   });
+  // cache of nodes we have already explained by some theory
+  std::unordered_set<Node, NodeHashFunction> cache;
 
   while (i < explanationVector.size()) {
     // Get the current literal to explain
@@ -1868,7 +1870,15 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector
         continue;
       }
     }
-
+    // We must cache after checking the timestamp in the block of code above.
+    // Afterwards, we can ignore this timestamp, as well as caching the Node,
+    // since any theory's explanation will suffice.
+    if (cache.find(toExplain.d_node) != cache.end())
+    {
+      ++i;
+      continue;
+    }
+    cache.insert(toExplain.d_node);
     // It was produced by the theory, so ask for an explanation
     Node explanation;
     if (toExplain.d_theory == THEORY_BUILTIN)