diff options
author | Tim King <taking@cs.nyu.edu> | 2012-06-14 20:59:14 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-06-14 20:59:14 +0000 |
commit | 66033cd2059d817cdeab5adc25f1397532a3fa78 (patch) | |
tree | 21aea6e8862c3868d5cecc449c951d64350dcca9 /src/theory/arith/congruence_manager.cpp | |
parent | 2211b6969c43436eb25b003bbeae7494217777c8 (diff) |
Fixing a bug related to explaining propagations with non-normalized witnesses.
Diffstat (limited to 'src/theory/arith/congruence_manager.cpp')
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 18 |
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); } |