From f774755b299ad524986c4bf628dbbed47a572a65 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Fri, 20 Jul 2018 12:38:40 -0700
Subject: [PATCH] bug fixes

---
 src/ASTTransform/integerencoding.cc | 2 ++
 src/Backend/constraint.cc           | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 78f1b73..5e4bfb8 100644
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -6,6 +6,7 @@
 #include "integerencodingrecord.h"
 #include "integerencorderresolver.h"
 #include "tunable.h"
+#include "polarityassignment.h"
 
 IntegerEncodingTransform::IntegerEncodingTransform(CSolver *_solver)
 	: Transform(_solver)
@@ -48,6 +49,7 @@ void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *bool
 	Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2);
 	Element *parray[] = {elem1, elem2};
 	BooleanEdge boolean = solver->applyPredicate(predicate, parray, 2);
+	updateEdgePolarity(boolean, boolOrder);
 	solver->replaceBooleanWithBoolean(boolOrder, boolean);
 }
 
diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 535d058..34ddb0a 100644
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -471,7 +471,7 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
 			uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
 			if (equalsEdge(cedge, nedge)) {
 				addEdgeToResizeNode(&result, cedge);
-				result->numVars += cedge.node_ptr->numEdges;
+				result->numVars += cSize;
 			} else if (!sameNodeOppSign(nedge, cedge)) {
 				Node *clause = allocResizeNode(cSize + nSize);
 				if (isNodeEdge(nedge)) {
-- 
2.34.1