From 8fed13e71e8ce1734d54398c34fd382452befc60 Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Mon, 1 Jul 2019 12:36:24 -0700
Subject: [PATCH] Freezing bug fix - Incremental SATTune works for Sypet

---
 src/Backend/satelemencoder.cc | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index aa73924..d924e6a 100644
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -227,6 +227,15 @@ void SATEncoder::freezeElementVariables(ElementEncoding *encoding){
 		ASSERT(edgeIsVarConst(e));
 		freezeVariable(cnf, e);
 	}
+	for(uint i=0; i< encoding->encArraySize; i++){
+		if(encoding->isinUseElement(i) && encoding->encoding != EENC_NONE && encoding->numVars > 1){
+			Edge e = encoding->edgeArray[i];
+			if(!edgeIsNull(e)){
+				ASSERT(edgeIsVarConst(e));
+				freezeVariable(cnf, e);
+			}
+		}
+	}
 }
 
 void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
@@ -294,6 +303,9 @@ void SATEncoder::generateElementEncoding(Element *element) {
 }
 
 int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
+	if(encoding->encArraySize == 1){
+		return 1;
+	}
 	for (int i = encoding->encArraySize - 1; i >= 0; i--) {
 		if (encoding->isinUseElement(i))
 			return i + 1;
-- 
2.34.1