One bug in our port and another bug in the original version

diff --git a/src/Backend/cnfexpr.cc b/src/Backend/cnfexpr.cc
index 1aa6cf0abc09d388cb89481b5b5cc822969d7f22..fb01d3f09b9d8957c9f6a4db1951ea1cd376586e 100644 (file)
--- a/src/Backend/cnfexpr.cc
+++ b/src/Backend/cnfexpr.cc
@@ -190,7 +190,7 @@ void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
 
 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
        if (expr->litSize == 0) {
-               if (!This->isTrue) {
+               if (!expr->isTrue) {
                        clearCNFExpr(This, false);
                }
                if (destroy) {

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 0372536ea36c3cec769a4096f768b2b91e5bd6d0..61fba12ed5ed190aa967347bc3c05fefa74e0c29 100644 (file)
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -839,8 +839,8 @@ CNFExpr *produceDisjunction(CNF *cnf, Edge e) {
                                int eL = argExp->litSize;                       // lits in argument
                                int aC = getClauseSizeCNF(accum);               // clauses in accum
                                int eC = getClauseSizeCNF(argExp);      // clauses in argument
-
-                               if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + aC + aL + aC)) {
+                               //POSSIBLE BUG #2 (eL * aC +aL * eC > eL +aC +aL +aC)
+                               if (eC > CLAUSE_MAX || (eL * aC + aL * eC > eL + eC + aL + aC)) {
                                        disjoinCNFLit(accum, introProxy(cnf, arg, argExp, isNegEdge(arg)));
                                } else {
                                        disjoinCNFExpr(accum, argExp, destroy);