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

1 files changed, 15 insertions, 3 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 14d2370ab..52f4c7014 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -160,7 +160,11 @@ bool ArithCongruenceManager::propagate(TNode x){
   // 11* : drop the constraint, do not propagate x or c
 
   if(!c->hasProof() && x != rewritten){
-    pushBack(x, rewritten);
+    if(c->assertedToTheTheory()){
+      pushBack(x, rewritten, c->getWitness());
+    }else{
+      pushBack(x, rewritten);
+    }
 
     c->setEqualityEngineProof();
     if(c->canBePropagated() && !c->assertedToTheTheory()){
@@ -169,10 +173,18 @@ bool ArithCongruenceManager::propagate(TNode x){
       c->propagate();
     }
   }else if(!c->hasProof() && x == rewritten){
-    pushBack(x, rewritten);
+    if(c->assertedToTheTheory()){
+      pushBack(x, c->getWitness());
+    }else{
+      pushBack(x);
+    }
     c->setEqualityEngineProof();
   }else if(c->hasProof() && x != rewritten){
-    pushBack(x, rewritten);
+    if(c->assertedToTheTheory()){
+      pushBack(x, rewritten, c->getWitness());
+    }else{
+      pushBack(x, rewritten);
+    }
   }else{
     Assert(c->hasProof() && x == rewritten);
   }