Adding a new test case for testing FLAGIFFUNDEFINED + bug fixes

[satune.git] / src / Test / ltelemconsttest.c

diff --git a/src/Test/ltelemconsttest.c b/src/Test/ltelemconsttest.c
index 018e36adbbe58e2e77db26e62036ca7f1cd3f7de..382394900345f7c13706915d199ad6cebe7223c6 100644 (file)
--- a/src/Test/ltelemconsttest.c
+++ b/src/Test/ltelemconsttest.c
@@ -1,5 +1,10 @@
 #include "csolver.h"
-
+/**
+ * e1 = 5
+ * e2 = {1, 3, 4, 6}
+ * e1 < e2
+ * Result: e1=5 e2=6
+ */
 int main(int numargs, char ** argv){
        CSolver *solver=allocCSolver();
        uint64_t set1[]={5};
@@ -11,7 +16,7 @@ int main(int numargs, char ** argv){
        Set * domain2[]={s1, s3};
        Predicate *lt=createPredicateOperator(solver, LT, domain2, 2);
        Element * inputs2[]={e1, e2};
-       Boolean *b=applyPredicate(solver, lt, inputs2, 2, NULL);
+       Boolean *b=applyPredicate(solver, lt, inputs2, 2);
        addConstraint(solver, b);
        if (startEncoding(solver)==1)
                printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));