bug fix

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index b5127c64ba2b480b9ae14e74625da76996c4444d..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++) {

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 62b08284cbcd446fccb6677e01b49d26b53d563b..6da5e4aa5eb3765c87fe921bc48f749c033e69f0 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -328,7 +328,12 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
                BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
                BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
                updateEdgePolarity(benew, be);
-               solver->replaceBooleanWithBoolean(be, benew);
+               if (solver->isTrue(benew))
+                 solver->replaceBooleanWithTrue(be);
+               else if (solver->isFalse(benew))
+                 solver->replaceBooleanWithFalse(be);
+               else
+                 solver->replaceBooleanWithBoolean(be, benew);
        }
        dstnode->inEdges.reset();
        delete inedgeit;
@@ -358,7 +363,12 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
                BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
                BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
                updateEdgePolarity(benew, be);
-               solver->replaceBooleanWithBoolean(be, benew);
+               if (solver->isTrue(benew))
+                 solver->replaceBooleanWithTrue(be);
+               else if (solver->isFalse(benew))
+                 solver->replaceBooleanWithFalse(be);
+               else
+                 solver->replaceBooleanWithBoolean(be, benew);
        }
        dstnode->outEdges.reset();
        delete outedgeit;