From: bdemsky <bdemsky@uci.edu>
Date: Mon, 18 Mar 2019 23:41:46 +0000 (-0700)
Subject: bug fix
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=f2bb71e84525d9ebc1841d5c2867d8b48c070cd5;ds=inline

bug fix
---

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;