From: bdemsky <bdemsky@uci.edu>
Date: Tue, 5 Sep 2017 07:56:27 +0000 (-0700)
Subject: One bug in our port and another bug in the original version
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=b104cc7c3b98c1f0024d36933dd35cc82fe10a53;p=satune.git

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 1aa6cf0..fb01d3f 100644
--- 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 0372536..61fba12 100644
--- 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);