Caught another bug

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index 75a5dfbb486d322725c820dfaf2ef19ebdbc3103..a1e596ff1ae133d340dc4e5c7ddb193c359fda97 100644 (file)
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -503,7 +503,7 @@ void produceCNF(CNF * cnf, Edge e) {
        /// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
        
        // propagate from positive to negative, negative to positive
-       propagate(cnf, expPos, expNeg, true) || propagate(cnf, expNeg, expPos, true);
+       propagate(cnf, & expPos, expNeg, true) || propagate(cnf, & expNeg, expPos, true);
        
        // The polarity heuristic entails visiting the discovery polarity first
        if (isPosEdge(e)) {
@@ -515,10 +515,10 @@ void produceCNF(CNF * cnf, Edge e) {
        }
 }
 
-bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate) {
+bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) {
        if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
                if (dest == NULL) {
-                       dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+                       *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
                } else if (isProxy(dest)) {
                        bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
                        if (alwaysTrue) {
@@ -529,7 +529,7 @@ bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate) {
                                addArrayClauseLiteral(cnf->solver, 1, clause);
                        }
                        
-                       dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+                       *dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
                } else {
                        clearCNFExpr(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
                }

diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index 7933bf8b57b70704764c0c953c594e4eaef36ed0..ee9502b8977900350117ecc8e3aa5abbd05092fa 100644 (file)
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -193,7 +193,7 @@ void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp);
 void produceCNF(CNF * cnf, Edge e);
 CNFExpr * produceConjunction(CNF * cnf, Edge e);
 CNFExpr* produceDisjunction(CNF *cnf, Edge e);
-bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate);
+bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate);
 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign);
 CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge);
 Literal introProxy(CNF * cnf, Edge e, CNFExpr* exp, bool isNeg);