From 481e97a274c994d66f9c34bd615c8b4af214439d Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Fri, 19 Aug 2016 22:53:36 -0400
Subject: [PATCH] propagate early in theory_str to set up contains/regex maps
 this fixes an unsat-as-sat error in a regex test and flips around some
 timeouts so more work will be required to track this down

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 360bfa26a..c781cae04 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -6052,6 +6052,10 @@ void theory_str::init_search_eh() {
     }
     */
 
+    // this might be cheating but we need to make sure that certain maps are populated
+    // before the first call to new_eq_eh()
+    propagate();
+
     TRACE("t_str", tout << "search started" << std::endl;);
     search_started = true;
 }