1 files changed, 19 insertions, 1 deletions
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 90c17be4a..9cb232908 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -27,7 +27,10 @@ namespace arith {
 InferenceManager::InferenceManager(TheoryArith& ta,
                                    ArithState& astate,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::")
+    : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::"),
+      // currently must track propagated literals if using the equality solver
+      d_trackPropLits(options::arithEqSolver()),
+      d_propLits(astate.getSatContext())
 {
 }
 
@@ -146,6 +149,21 @@ bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem)
   return false;
 }
 
+bool InferenceManager::propagateLit(TNode lit)
+{
+  if (d_trackPropLits)
+  {
+    d_propLits.insert(lit);
+  }
+  return TheoryInferenceManager::propagateLit(lit);
+}
+
+bool InferenceManager::hasPropagated(TNode lit) const
+{
+  Assert(d_trackPropLits);
+  return d_propLits.find(lit) != d_propLits.end();
+}
+
 }  // namespace arith
 }  // namespace theory
 }  // namespace cvc5