From 953a4c5437c5a5d1a2be60e68991f0f15a0b49a2 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 2 Dec 2015 20:48:15 -0500
Subject: [PATCH] add temporary variables to m_trail

---
 src/smt/theory_str.cpp | 8 +++++---
 src/smt/theory_str.h   | 3 +++
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 3c6261243..9d0f9d689 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -30,6 +30,7 @@ theory_str::theory_str(ast_manager & m):
         m_autil(m),
         m_strutil(m),
         sLevel(0),
+        m_trail(m),
         tmpStringVarCount(0),
 		tmpXorVarCount(0),
 		tmpLenTestVarCount(0),
@@ -357,9 +358,8 @@ app * theory_str::mk_internal_xor_var() {
     strcpy(new_buffer, name.c_str());
 	symbol sym(new_buffer);
 
-	app* a = m.mk_const(m.mk_const_decl(sym, int_sort));
-
-	// TODO ctx.save_ast_trail(a)?
+	app * a = m.mk_const(m.mk_const_decl(sym, int_sort));
+	m_trail.push_back(a);
 	return a;
 }
 
@@ -382,6 +382,7 @@ app * theory_str::mk_str_var(std::string name) {
 	SASSERT(ctx.e_internalized(a));
 	m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
 
+	m_trail.push_back(a);
 	variable_set.insert(a);
 	internal_variable_set.insert(a);
 	track_variable_scope(a);
@@ -424,6 +425,7 @@ app * theory_str::mk_nonempty_str_var() {
     }
 
     // add 'a' to variable sets, so we can keep track of it
+    m_trail.push_back(a);
     variable_set.insert(a);
     internal_variable_set.insert(a);
     track_variable_scope(a);
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index f126ca019..ca985cb8f 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -67,6 +67,9 @@ namespace smt {
         str_util m_strutil;
         int sLevel;
 
+        // TODO make sure that all generated expressions are saved into the trail
+        expr_ref_vector m_trail; // trail for generated terms
+
         str_value_factory * m_factory;
 
         ptr_vector<enode> m_basicstr_axiom_todo;