From 4433417b6ebdf34384e46462fbe5c2f647437200 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 20 Sep 2016 16:25:28 -0400
Subject: [PATCH] faster push_scope in theory_str

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 798e16e7c..59db86212 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -32,7 +32,7 @@ theory_str::theory_str(ast_manager & m):
         /* Options */
         opt_AggressiveLengthTesting(false),
         opt_AggressiveValueTesting(false),
-        opt_AggressiveUnrollTesting(false),
+        opt_AggressiveUnrollTesting(true),
         opt_EagerStringConstantLengthAssertions(true),
         opt_VerifyFinalCheckProgress(true),
 		opt_LCMUnrollStep(2),
@@ -6551,10 +6551,12 @@ void theory_str::push_scope_eh() {
     m_trail_stack.push_scope();
 
     // TODO out-of-scope term debugging, see comment in pop_scope_eh()
+    /*
     context & ctx = get_context();
     ast_manager & m = get_manager();
     expr_ref_vector assignments(m);
     ctx.get_assignments(assignments);
+    */
 
     sLevel += 1;
     TRACE("t_str", tout << "push to " << sLevel << std::endl;);