From: Hamed <hamed.gorjiara@gmail.com>
Date: Mon, 17 Jul 2017 21:27:31 +0000 (-0700)
Subject: Add some printings for debugging ...
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=5b8fc6a05e9fe509cb247621763b674fb906d089;p=satune.git

Add some printings for debugging ...
---

diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index d7fb6a2..87be4b7 100644
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -222,6 +222,11 @@ void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction*
 			default:
 				ASSERT(0);
 			}
+#ifdef TRACE_DEBUG
+			model_print("added clause in operator function\n");
+			printCNF(clause);
+			model_print("\n");
+#endif
 			pushVectorEdge(clauses, clause);
 		}
 		
diff --git a/src/Test/funcencoding.c b/src/Test/funcencoding.c
index 40567d9..0dacef0 100644
--- a/src/Test/funcencoding.c
+++ b/src/Test/funcencoding.c
@@ -58,7 +58,8 @@ int main(int numargs, char ** argv) {
 	addConstraint(solver, pred);
 	
 	if (startEncoding(solver)==1)
-		printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
+		printf("e1=%llu e2=%llu e7=%llu\n", 
+			 getElementValue(solver,e1), getElementValue(solver, e2), getElementValue(solver, e7));
 	else
 		printf("UNSAT\n");
 	deleteSolver(solver);