From c53a5c97df5189f82b618e510bb7fcad8671e5ff Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 6 Dec 2018 15:08:50 -0800
Subject: [PATCH] Preprocessing check

---
 src/ASTTransform/preprocess.cc | 2 +-
 src/csolver.cc                 | 4 ++++
 src/csolver.h                  | 5 +++--
 3 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/ASTTransform/preprocess.cc b/src/ASTTransform/preprocess.cc
index 1e60c19..7b4877b 100644
--- a/src/ASTTransform/preprocess.cc
+++ b/src/ASTTransform/preprocess.cc
@@ -13,7 +13,7 @@ Preprocess::~Preprocess() {
 }
 
 void Preprocess::doTransform() {
-	if (solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
+	if (!solver->isBooleanVarUsed() && solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
 		return;
 
 	BooleanIterator bit(solver);
diff --git a/src/csolver.cc b/src/csolver.cc
index fbe0dd0..45163be 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -34,6 +34,7 @@ CSolver::CSolver() :
 	boolTrue(BooleanEdge(new BooleanConst(true))),
 	boolFalse(boolTrue.negate()),
 	unsat(false),
+	booleanVarUsed(false),
 	tuner(NULL),
 	elapsedTime(0),
 	satsolverTimeout(NOTIMEOUT)
@@ -136,6 +137,7 @@ void CSolver::resetSolver() {
 	boolTrue = BooleanEdge(new BooleanConst(true));
 	boolFalse = boolTrue.negate();
 	unsat = false;
+	booleanVarUsed = false;
 	elapsedTime = 0;
 	tuner = NULL;
 	satEncoder->resetSATEncoder();
@@ -308,6 +310,8 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
 BooleanEdge CSolver::getBooleanVar(VarType type) {
 	Boolean *boolean = new BooleanVar(type);
 	allBooleans.push(boolean);
+	if(!booleanVarUsed)
+		booleanVarUsed = true;
 	return BooleanEdge(boolean);
 }
 
diff --git a/src/csolver.h b/src/csolver.h
index 16937dd..c604486 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -141,7 +141,7 @@ public:
 	void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
 	void setSatSolverTimeout(long seconds) { satsolverTimeout = seconds;}
 	bool isUnSAT() { return unsat; }
-
+        bool isBooleanVarUsed(){return booleanVarUsed;}
 	void printConstraint(BooleanEdge boolean);
 	void printConstraints();
 
@@ -218,7 +218,8 @@ private:
 
 	SATEncoder *satEncoder;
 	bool unsat;
-	Tuner *tuner;
+        bool booleanVarUsed;
+        Tuner *tuner;
 	long long elapsedTime;
 	long satsolverTimeout;
 	friend class ElementOpt;
-- 
2.34.1