From 3db73e442c13c76185fe4c271234448d7fddc7c2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 29 Nov 2018 21:04:43 -0800
Subject: [PATCH] reset max unfolding literal on backtrack

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_seq.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 04abe5949..4ff0fb7bc 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -5550,6 +5550,7 @@ void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {
     if (m_util.has_re()) {
         expr_ref dlimit(m);
         dlimit = mk_max_unfolding_depth();
+        m_trail_stack.push(value_trail<theory_seq, literal>(m_max_unfolding_lit));
         m_max_unfolding_lit = mk_literal(dlimit);        
         assumptions.push_back(dlimit);
     }