Add some printings for debugging ...

diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index d7fb6a289c2c5acaaa334d6e37102111d941af5c..87be4b78da7672dcb12a254ab24f4d16cc7f6c57 100644 (file)
--- 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 40567d91386013b161a707e33578e5ce74632633..0dacef0a4b39dce55184711631efcc1425422230 100644 (file)
--- 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);