bug fix

[satune.git] / src / AST / rewriter.cc

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index 58ef96b05228d2eb36adcb97bcf351eb2a1d37ff..fef4dcbb17aaf40626791272a67db9d68cf0de11 100644 (file)
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -23,7 +23,7 @@ void CSolver::replaceBooleanWithFalseNoRemove(BooleanEdge bexpr) {
 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
        updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
 
-       ASSERT(bexpr->boolVal != BV_UNSAT);
+       ASSERT((bexpr->boolVal != BV_UNSAT ) || unsat);
 
        uint size = bexpr->parents.getSize();
        for (uint i = 0; i < size; i++) {
@@ -51,7 +51,7 @@ void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
        }
 }
 
-void CSolver::handleFunction(ElementFunction * ef, BooleanEdge child) {
+void CSolver::handleFunction(ElementFunction *ef, BooleanEdge child) {
        BooleanEdge childNegate = child.negate();
        elemMap.remove(ef);
        if (ef->overflowstatus == child) {
@@ -106,7 +106,7 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
                } else {
                        BooleanLogic *logicop = (BooleanLogic *) parent;
                        boolMap.remove(logicop);        //could change parent's hash
-                       
+
                        uint parentsize = logicop->inputs.getSize();
                        for (uint j = 0; j < parentsize; j++) {
                                BooleanEdge b = logicop->inputs.get(j);