From: bdemsky <bdemsky@uci.edu>
Date: Fri, 25 Aug 2017 23:47:44 +0000 (-0700)
Subject: Big Bug Fix
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=be10925dbe373dcbdc2f6acc1ed11273a9b201ff;p=satune.git

Big Bug Fix
---

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index cd1cb17..0a93045 100644
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -35,8 +35,8 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) {
 		model_print("Encoding All ...\n\n");
 		Edge c = encodeConstraintSATEncoder(This, constraint);
 		model_print("Returned Constraint in EncodingAll:\n");
-		if( equalsEdge(c, E_BOGUS) )
-			addConstraintCNF(This->cnf, c);
+		ASSERT( ! equalsEdge(c, E_BOGUS));
+		addConstraintCNF(This->cnf, c);
 	}
 	delete iterator;
 }
diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 9061f76..6ec1f33 100644
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -22,8 +22,6 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
 		default:
 			ASSERT(0);
 	}
-	default:
-		ASSERT(0);
 	return E_BOGUS;
 }