Fixing a bug related to explaining propagations with non-normalized witnesses.

1 files changed, 9 insertions, 0 deletions

diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 1864bc89e..fd8eef1f1 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -152,6 +152,15 @@ private:
     ++(d_statistics.d_propagations);
   }
 
+  void pushBack(TNode n, TNode r, TNode w){
+    d_explanationMap.insert(w, d_propagatations.size());
+    d_explanationMap.insert(r, d_propagatations.size());
+    d_explanationMap.insert(n, d_propagatations.size());
+    d_propagatations.enqueue(n);
+
+    ++(d_statistics.d_propagations);
+  }
+
   bool propagate(TNode x);
   void explain(TNode literal, std::vector<TNode>& assumptions);