Getting some bugs fixed ...

diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c
index 72c74c7a96de74bb8d6699cc9e9396f712110175..8c4b7c896db8e9036a579075434baae810992c54 100644 (file)
--- a/src/Backend/constraint.c
+++ b/src/Backend/constraint.c
@@ -487,6 +487,7 @@ void convertConstraint(CNF *cnf, VectorEdge *stack, Edge root, bool backtrackLit
                }
        }
        CNFExpr * cnfExp = (CNFExpr *) nroot->ptrAnnot[isNegEdge(root)];
+       ASSERT(cnfExp!=NULL);
        if (isProxy(cnfExp)) {
                Literal l=getProxy(cnfExp);
                Literal clause[] = {l};

diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
index 741806ea2cd350debe590ecc720e62c80edb8dc0..e64cb09ff00b59a79fb07e7945852fa4c3bd8c7a 100644 (file)
--- a/src/Backend/satfuncencoder.c
+++ b/src/Backend/satfuncencoder.c
@@ -255,6 +255,10 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* fu
        ArrayElement* elements= &func->inputs;
        Table* table = ((FunctionTable*) (func->function))->table;
        uint size = getSizeVectorTableEntry(&table->entries);
+       for(uint i=0; i<getSizeArrayElement(elements); i++){
+               Element *elem = getArrayElement( elements, i);
+               encodeElementSATEncoder(This, elem);
+       }
        Edge constraints[size]; //FIXME: should add a space for the case that didn't match any entries
        for(uint i=0; i<size; i++) {
                TableEntry* entry = getVectorTableEntry(&table->entries, i);