From: bdemsky <bdemsky@uci.edu>
Date: Fri, 25 Aug 2017 02:24:36 +0000 (-0700)
Subject: fix bug
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=88f2dbc9d903381e2ce9ab15b12495eec8f5676e;p=satune.git

fix bug
---

diff --git a/src/Encoders/polarityassignment.cc b/src/Encoders/polarityassignment.cc
index 77d2a06..bf787ea 100644
--- a/src/Encoders/polarityassignment.cc
+++ b/src/Encoders/polarityassignment.cc
@@ -35,8 +35,10 @@ void computePolarityAndBooleanValue(Boolean *This) {
 }
 
 void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
-	updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
-	computePolarityAndBooleanValue(This->undefStatus);
+	if (This->undefStatus != NULL) {
+		updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
+		computePolarityAndBooleanValue(This->undefStatus);
+	}
 }
 
 void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
diff --git a/src/Test/buildconstraintstest.cc b/src/Test/buildconstraintstest.cc
index af28c49..71cb211 100644
--- a/src/Test/buildconstraintstest.cc
+++ b/src/Test/buildconstraintstest.cc
@@ -49,7 +49,7 @@ int main(int numargs, char **argv) {
 	Predicate *equal2 = solver->createPredicateOperator(EQUALS, domain2, 2);
 	Element *inputs2 [] = {e4, e3};
 	Boolean *pred = solver->applyPredicate(equal2, inputs2, 2);
-solver->	addConstraint(pred);
+	solver->addConstraint(pred);
 
 	if (solver->startEncoding() == 1)
 		printf("e1=%llu e2=%llu\n", solver->getElementValue(e1), solver->getElementValue(e2));