checked all 1 and 2 cases
[mc1516pa.git] / modelchecker / main.c
index 16eecbe..fd37c23 100644 (file)
@@ -66,9 +66,11 @@ void solve(FILE *inputstream)
        BDD new = init->bdd;
        int iteration = 0;
        while(new != old){
-               ERRPRINT("Iteration %d\n", iteration++);
                old = new;
+               ERRPRINT("Iteration %d\n", iteration++);
+               ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
         trans_t *t = rls->rell;
+
         while (t != NULL){
             new = sylvan_or(new, sylvan_relnext(new, t->bdd, t->varset.varset));
             t = t->next_rel;