bug fix

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index b5127c6..fef4dcb 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);
 
 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++) {
 
        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 62b0828..6da5e4a 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);
                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;
        }
        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);
                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;
        }
        dstnode->outEdges.reset();
        delete outedgeit;