7 files changed, 44 insertions, 5 deletions
diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index a38dfdfe5..357a54b1a 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/simple_bitblaster.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/theory_model.h"
 #include "theory/theory_state.h"
+#include "options/bv_options.h"
 
 namespace cvc5 {
 namespace theory {
@@ -129,6 +130,15 @@ Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel)
   return utils::mkConst(bits.size(), value);
 }
 
+void BBSimple::computeRelevantTerms(std::set<Node>& termSet)
+{
+  Assert(options::bitblastMode() == options::BitblastMode::EAGER);
+  for (const auto& var : d_variables)
+  {
+    termSet.insert(var);
+  }
+}
+
 bool BBSimple::collectModelValues(TheoryModel* m,
                                   const std::set<Node>& relevantTerms)
 {
diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index ebbb2891f..ec0899145 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/simple_bitblaster.h
@@ -53,6 +53,8 @@ class BBSimple : public TBitblaster<Node>
   /** Create 'bits' for variable 'var'. */
   void makeVariable(TNode var, Bits& bits) override;
 
+  /** Add d_variables to termSet. */
+  void computeRelevantTerms(std::set<Node>& termSet);
   /** Collect model values for all relevant terms given in 'relevantTerms'. */
   bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
 
diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index 8ff4318c0..6ccc6c7c1 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -32,7 +32,7 @@ class BVSolver
   BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr)
       : d_state(state), d_im(inferMgr){};
 
-  virtual ~BVSolver(){};
+  virtual ~BVSolver() {}
 
   /**
    * Returns true if we need an equality engine. If so, we initialize the
@@ -71,7 +71,7 @@ class BVSolver
 
   virtual bool needsCheckLastEffort() { return false; }
 
-  virtual void propagate(Theory::Effort e){};
+  virtual void propagate(Theory::Effort e) {}
 
   virtual TrustNode explain(TNode n)
   {
@@ -80,17 +80,20 @@ class BVSolver
     return TrustNode::null();
   }
 
+  /** Additionally collect terms relevant for collecting model values. */
+  virtual void computeRelevantTerms(std::set<Node>& termSet) {}
+
   /** Collect model values in m based on the relevant terms given by termSet */
   virtual bool collectModelValues(TheoryModel* m,
                                   const std::set<Node>& termSet) = 0;
 
   virtual std::string identify() const = 0;
 
-  virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
+  virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }
 
-  virtual void ppStaticLearn(TNode in, NodeBuilder& learned){};
+  virtual void ppStaticLearn(TNode in, NodeBuilder& learned) {}
 
-  virtual void presolve(){};
+  virtual void presolve() {}
 
   virtual void notifySharedTerm(TNode t) {}
 
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 414e57e19..3ae4a7f0a 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -238,6 +238,21 @@ TrustNode BVSolverBitblast::explain(TNode n)
   return d_im.explainLit(n);
 }
 
+void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet)
+{
+  /* BITVECTOR_EAGER_ATOM wraps input assertions that may also contain
+   * equalities. As a result, these equalities are not handled by the equality
+   * engine and terms below these equalities do not appear in `termSet`.
+   * We need to make sure that we compute model values for all relevant terms
+   * in BitblastMode::EAGER and therefore add all variables from the
+   * bit-blaster to `termSet`.
+   */
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
+    d_bitblaster->computeRelevantTerms(termSet);
+  }
+}
+
 bool BVSolverBitblast::collectModelValues(TheoryModel* m,
                                           const std::set<Node>& termSet)
 {
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index 31d9443c8..c5134c6fc 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -64,6 +64,8 @@ class BVSolverBitblast : public BVSolver
 
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
+  void computeRelevantTerms(std::set<Node>& termSet) override;
+
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 22b05b026..3d7f11f6d 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -175,6 +175,11 @@ bool TheoryBV::needsCheckLastEffort()
   return d_internal->needsCheckLastEffort();
 }
 
+void TheoryBV::computeRelevantTerms(std::set<Node>& termSet)
+{
+  return d_internal->computeRelevantTerms(termSet);
+}
+
 bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 {
   return d_internal->collectModelValues(m, termSet);
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 4b3a1f3b2..e884f621c 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -83,6 +83,8 @@ class TheoryBV : public Theory
 
   TrustNode explain(TNode n) override;
 
+  void computeRelevantTerms(std::set<Node>& termSet) override;
+
   /** Collect model values in m based on the relevant terms given by termSet */
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;