From f2bb71e84525d9ebc1841d5c2867d8b48c070cd5 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 18 Mar 2019 16:41:46 -0700 Subject: [PATCH] bug fix --- src/AST/rewriter.cc | 2 +- src/ASTTransform/decomposeordertransform.cc | 14 ++++++++++++-- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc index b5127c6..fef4dcb 100644 --- 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 62b0828..6da5e4a 100644 --- 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; -- 2.34.1