From 2ac885d81b9533ac8fc83f964a1852fab8e60112 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Mon, 4 Sep 2017 00:00:15 -0700
Subject: [PATCH] Bug Fix

---
 src/AST/boolean.h                           | 3 +++
 src/ASTTransform/decomposeordertransform.cc | 4 +++-
 src/Backend/constraint.cc                   | 2 ++
 src/Tuner/autotuner.cc                      | 1 +
 src/csolver.cc                              | 6 +-----
 5 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 41e9d5b..ecaebaf 100644
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -79,4 +79,7 @@ public:
 	Array<BooleanEdge> inputs;
 	CMEMALLOC;
 };
+BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e);
+
+
 #endif
diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 85b43b1..7d276e2 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -60,11 +60,13 @@ void DecomposeOrderTransform::doTransform() {
 			}
 		}
 
+		/*
 		bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
 
 		if (mustReachPrune)
 			removeMustBeTrueNodes(solver, graph);
-
+		*/
+		
 		//This is needed for splitorder
 		computeStronglyConnectedComponentGraph(graph);
 		decomposeOrder(order, graph);
diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index b90ec4a..0372536 100644
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -59,6 +59,8 @@ CNF *createCNF() {
 	initDefVectorEdge(&cnf->constraints);
 	initDefVectorEdge(&cnf->args);
 	cnf->solver = allocIncrementalSolver();
+	cnf->solveTime = 0;
+	cnf->encodeTime = 0;
 	return cnf;
 }
 
diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index 9082ae4..5247d86 100644
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -17,6 +17,7 @@ long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
 	CSolver *copy = problem->clone();
 	copy->setTuner(tuner);
 	int result = copy->solve();
+	model_print("SAT %d\n", result);
 	long long elapsedTime = copy->getElapsedTime();
 	long long encodeTime = copy->getEncodeTime();
 	long long solveTime = copy->getSolveTime();
diff --git a/src/csolver.cc b/src/csolver.cc
index ea16b80..b353791 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -77,7 +77,7 @@ CSolver *CSolver::clone() {
 	SetIteratorBooleanEdge *it = getConstraints();
 	while (it->hasNext()) {
 		BooleanEdge b = it->next();
-		copy->addConstraint(b->clone(copy, &map));
+		copy->addConstraint(cloneEdge(copy, &map, b));
 	}
 	delete it;
 	return copy;
@@ -374,10 +374,6 @@ void CSolver::addConstraint(BooleanEdge constraint) {
 		}
 		constraints.add(constraint);
 		Boolean *ptr=constraint.getBoolean();
-		if (constraint.isNegated())
-			updateMustValue(ptr, BV_MUSTBEFALSE);
-		else
-			updateMustValue(ptr, BV_MUSTBETRUE);
 		
 		if (ptr->boolVal == BV_UNSAT)
 			setUnSAT();
-- 
2.34.1