Big Bug Fix

diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index cd1cb1713b746dfb112a51252a8c705ca855542f..0a93045073d30146195362287413d620a2460e60 100644 (file)
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -35,8 +35,8 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) {
                model_print("Encoding All ...\n\n");
                Edge c = encodeConstraintSATEncoder(This, constraint);
                model_print("Returned Constraint in EncodingAll:\n");
-               if( equalsEdge(c, E_BOGUS) )
-                       addConstraintCNF(This->cnf, c);
+               ASSERT( ! equalsEdge(c, E_BOGUS));
+               addConstraintCNF(This->cnf, c);
        }
        delete iterator;
 }

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 9061f76f432aa1ff3af7c3df490aaa65f9779824..6ec1f33f3e38c4e2592eb67a82e16c45142e44c9 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -22,8 +22,6 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
                default:
                        ASSERT(0);
        }
-       default:
-               ASSERT(0);
        return E_BOGUS;
 }