From 649d48d2697fb45f36bbbdd52ee067d7b5490fb2 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Mon, 23 Oct 2017 15:10:47 -0700
Subject: [PATCH] Bug fix

---
 src/AST/boolean.cc            |  2 ++
 src/Collections/corestructs.h |  4 +++-
 src/csolver.cc                | 27 +++++++++++----------------
 3 files changed, 16 insertions(+), 17 deletions(-)

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index dcc201d..939f937 100644
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -96,6 +96,8 @@ Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) {
 
 void BooleanPredicate::updateParents() {
 	for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+	if (undefStatus)
+		undefStatus->parents.push(this);
 }
 
 void BooleanLogic::updateParents() {
diff --git a/src/Collections/corestructs.h b/src/Collections/corestructs.h
index 7a8104d..b0ff819 100644
--- a/src/Collections/corestructs.h
+++ b/src/Collections/corestructs.h
@@ -20,7 +20,9 @@ public:
 	Boolean *getBoolean() {return (Boolean *)(((uintptr_t)b) & ~((uintptr_t) 1));}
 	Boolean *getRaw() {return b;}
 	Boolean *operator->() {return getBoolean();}
-	operator bool() const {return b != NULL;}
+	operator bool() {
+		return getBoolean() != NULL;
+	}
 private:
 	Boolean *b;
 };
diff --git a/src/csolver.cc b/src/csolver.cc
index be4a3a8..a2163a0 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -65,7 +65,6 @@ CSolver::~CSolver() {
 	for (uint i = 0; i < size; i++) {
 		delete allOrders.get(i);
 	}
-
 	size = allFunctions.getSize();
 	for (uint i = 0; i < size; i++) {
 		delete allFunctions.get(i);
@@ -103,7 +102,6 @@ void CSolver::serialize() {
 		Deserializer deserializer("dump");
 		deserializer.deserialize();
 	}
-
 }
 
 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
@@ -175,6 +173,7 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) {
 	}
 }
 
+
 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
 	Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
 	Element *e = elemMap.get(element);
@@ -311,13 +310,11 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 	}
 	case SATC_IFF: {
 		for (uint i = 0; i < 2; i++) {
-			if (array[i]->type == BOOLCONST) {
-				if (isTrue(array[i])) {	// It can be undefined
-					return array[1 - i];
-				} else if (isFalse(array[i])) {
-					newarray[0] = array[1 - i];
-					return applyLogicalOperation(SATC_NOT, newarray, 1);
-				}
+			if (isTrue(array[i])) {	// It can be undefined
+				return array[1 - i];
+			} else if (isFalse(array[i])) {
+				newarray[0] = array[1 - i];
+				return applyLogicalOperation(SATC_NOT, newarray, 1);
 			} else if (array[i]->type == LOGICOP) {
 				BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
 				if (b->replaced) {
@@ -341,12 +338,10 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 				if (((BooleanLogic *)b.getBoolean())->replaced)
 					return rewriteLogicalOperation(op, array, asize);
 			}
-			if (b->type == BOOLCONST) {
-				if (isTrue(b))
-					continue;
-				else {
-					return boolFalse;
-				}
+			if (isTrue(b))
+				continue;
+			else if (isFalse(b)) {
+				return boolFalse;
 			} else
 				newarray[newindex++] = b;
 		}
@@ -389,7 +384,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 	//	ASSERT(first != second);
 	if (first == second)
 		return getBooleanFalse();
-	
+
 	bool negate = false;
 	if (order->type == SATC_TOTAL) {
 		if (first > second) {
-- 
2.34.1