From fd1bf65b6472b883203ea3f0fecb33ee028c66df Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 30 Nov 2016 15:52:58 -0500
Subject: [PATCH] experimental non-reuse of XOR vars in theory_str

---
 src/smt/theory_str.cpp | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 84adf819d..ec0a432d1 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -2815,13 +2815,12 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
         if (entry1InScope) {
             t1 = varForBreakConcat[key1][0];
             t2 = varForBreakConcat[key1][1];
-            xorFlag = varForBreakConcat[key1][2];
+            xorFlag = mk_internal_xor_var();
         } else {
             t1 = varForBreakConcat[key2][0];
             t2 = varForBreakConcat[key2][1];
-            xorFlag = varForBreakConcat[key2][2];
+            xorFlag = mk_internal_xor_var();
         }
-        // TODO do I need to refresh the xorFlag, which is an integer var, and if so, how?
         refresh_theory_var(t1);
         refresh_theory_var(t2);
     }
@@ -3141,12 +3140,11 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
 	} else {
 		if (entry1InScope) {
 			temp1 = varForBreakConcat[key1][0];
-			xorFlag = varForBreakConcat[key1][1];
+			xorFlag = mk_internal_xor_var();
 		} else if (entry2InScope) {
 			temp1 = varForBreakConcat[key2][0];
-			xorFlag = varForBreakConcat[key2][1];
+			xorFlag = mk_internal_xor_var();
 		}
-		// TODO refresh xorFlag?
 		refresh_theory_var(temp1);
 	}
 
@@ -3451,10 +3449,10 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
     } else {
         if (entry1InScope) {
             temp1 = varForBreakConcat[key1][0];
-            xorFlag = varForBreakConcat[key1][1];
+            xorFlag = mk_internal_xor_var();
         } else if (varForBreakConcat.find(key2) != varForBreakConcat.end()) {
             temp1 = varForBreakConcat[key2][0];
-            xorFlag = varForBreakConcat[key2][1];
+            xorFlag = mk_internal_xor_var();
         }
         refresh_theory_var(temp1);
     }
@@ -3948,10 +3946,10 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) {
     } else {
         if (entry1InScope) {
             commonVar = (entry1->second)[0];
-            xorFlag = (entry1->second)[1];
+            xorFlag = mk_internal_xor_var();
         } else {
             commonVar = (entry2->second)[0];
-            xorFlag = (entry2->second)[1];
+            xorFlag = mk_internal_xor_var();
         }
         refresh_theory_var(commonVar);
     }
@@ -6113,9 +6111,9 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) {
         				xorFlag = mk_internal_xor_var();
         				varForBreakConcat[key1][0] = xorFlag;
         			} else if (entry1InScope) {
-        				xorFlag = varForBreakConcat[key1][0];
+        				xorFlag = mk_internal_xor_var();
         			} else { // entry2InScope
-        				xorFlag = varForBreakConcat[key2][0];
+        				xorFlag = mk_internal_xor_var();
         			}
 
         			int concatStrLen = const_str.length();