Add LTE function for completeness and fix bug in LT

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

diff --git a/src/Test/elemequalunsattest.c b/src/Test/elemequalunsattest.c
index bd38ed9183d1711c1c60a05ee4f27c0d80cfb9ee..5cbdd0460435a8cc52fa6b6b413c64b9d66082e4 100644 (file)
--- a/src/Test/elemequalunsattest.c
+++ b/src/Test/elemequalunsattest.c
@@ -3,24 +3,24 @@
  * e1 = {0, 1, 2}
  * e2 = {3, 4}
  * e1 == e2
- * 
+ *
  * Result: UNSAT
  */
-int main(int numargs, char ** argv) {
-       CSolver * solver=allocCSolver();
-       uint64_t set1[]={0, 1, 2};
-       uint64_t set2[]={3, 4};
-       Set * s1=createSet(solver, 0, set1, 3);
-       Set * s2=createSet(solver, 0, set2, 2);
-       Element * e1=getElementVar(solver, s1);
-       Element * e2=getElementVar(solver, s2);
-       Set * domain[]={s1, s2};
-       Predicate *equals=createPredicateOperator(solver, EQUALS, domain, 2);
-       Element * inputs[]={e1, e2};
-       Boolean *b=applyPredicate(solver, equals, inputs, 2);
+int main(int numargs, char **argv) {
+       CSolver *solver = allocCSolver();
+       uint64_t set1[] = {0, 1, 2};
+       uint64_t set2[] = {3, 4};
+       Set *s1 = createSet(solver, 0, set1, 3);
+       Set *s2 = createSet(solver, 0, set2, 2);
+       Element *e1 = getElementVar(solver, s1);
+       Element *e2 = getElementVar(solver, s2);
+       Set *domain[] = {s1, s2};
+       Predicate *equals = createPredicateOperator(solver, EQUALS, domain, 2);
+       Element *inputs[] = {e1, e2};
+       Boolean *b = applyPredicate(solver, equals, inputs, 2);
        addConstraint(solver, b);
-       
-       if (startEncoding(solver)==1)
+
+       if (startEncoding(solver) == 1)
                printf("e1=%llu e2=%llu\n", getElementValue(solver,e1), getElementValue(solver, e2));
        else
                printf("UNSAT\n");