From 8958eea27cf282b86945d7fa86d03d6e60ef6273 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sun, 31 Jul 2016 11:22:04 -0400
Subject: [PATCH] crash avoidance in theory_str cut_var_map writes

---
 src/smt/theory_str.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index fe68b02ad..624892ee1 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -306,6 +306,9 @@ bool theory_str::has_self_cut(expr * n1, expr * n2) {
 }
 
 void theory_str::add_cut_info_one_node(expr * baseNode, int slevel, expr * node) {
+    // crash avoidance?
+    m_trail.push_back(baseNode);
+    m_trail.push_back(node);
     if (cut_var_map.find(baseNode) == cut_var_map.end()) {
         T_cut * varInfo = alloc(T_cut);
         varInfo->level = slevel;
@@ -334,6 +337,9 @@ void theory_str::add_cut_info_one_node(expr * baseNode, int slevel, expr * node)
 }
 
 void theory_str::add_cut_info_merge(expr * destNode, int slevel, expr * srcNode) {
+    // crash avoidance?
+    m_trail.push_back(destNode);
+    m_trail.push_back(srcNode);
     if (cut_var_map.find(srcNode) == cut_var_map.end()) {
         get_manager().raise_exception("illegal state in add_cut_info_merge(): cut_var_map doesn't contain srcNode");
     }