From: Hamed <hamed.gorjiara@gmail.com>
Date: Mon, 10 Jul 2017 22:12:29 +0000 (-0700)
Subject: fixing more bugs ...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=f5c782cb6352d8a1b71bdb400df025c739165105;p=satune.git

fixing more bugs ...
---

diff --git a/src/AST/order.c b/src/AST/order.c
index 2f3de74..b943392 100644
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -29,6 +29,7 @@ void setOrderEncodingType(Order* order, OrderEncodingType type){
 void deleteOrder(Order* order){
 	deleteVectorArrayBoolean(& order->constraints);
 	deleteOrderEncoding(& order->order);
-	deleteHashTableBoolConst(order->boolsToConstraints);
+	if(order->boolsToConstraints!= NULL)
+		deleteHashTableBoolConst(order->boolsToConstraints);
 	ourfree(order);
 }
diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index b491ca3..ef60709 100644
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -159,6 +159,7 @@ void printConstraint(Constraint * This) {
 		model_print("!t%u",This->numoperandsorvar);
 		break;
 	default:
+		model_print("In printingConstraint: %d", This->type);
 		ASSERT(0);
 	}
 }
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 4a72f0a..3c2d3e1 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -82,9 +82,9 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
 	for(uint i=0;i<size;i++) {
 		Boolean *constraint=getVectorBoolean(constraints, i);
 		Constraint* c= encodeConstraintSATEncoder(This, constraint);
-		addConstraintToSATSolver(c, This->satSolver);
 		printConstraint(c);
 		model_print("\n\n");
+		addConstraintToSATSolver(c, This->satSolver);
 		//FIXME: When do we want to delete constraints? Should we keep an array of them
 		// and delete them later, or it would be better to just delete them right away?
 	}
diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index c91fd57..81f01b3 100644
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -38,6 +38,6 @@ int main(int numargs, char ** argv) {
 	Element* inputs2 [] = {e4, e3};
 	Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
 	addBoolean(solver, pred);
-//	startEncoding(solver);
+	startEncoding(solver);
 	deleteSolver(solver);
 }