From 685edbb268cb1034c580fda269c1e226118da17e Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 15 Aug 2016 18:58:36 -0400
Subject: [PATCH] pull out incorrectly-used data structures in theory_str for
 contains check, this will need to be revisited

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 93173402c..40745b069 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -4376,7 +4376,7 @@ void theory_str::check_contain_by_substr(expr * varNode, expr_ref_vector & willE
 }
 
 bool theory_str::in_contain_idx_map(expr * n) {
-    return contain_pair_idx_map.contains(n);
+    return contain_pair_idx_map.find(n) != contain_pair_idx_map.end();
 }
 
 void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) {
@@ -4384,8 +4384,8 @@ void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) {
     ast_manager & m = get_manager();
 
     if (in_contain_idx_map(n1) && in_contain_idx_map(n2)) {
-        obj_pair_set<expr, expr>::iterator keysItor1 = contain_pair_idx_map[n1].begin();
-        obj_pair_set<expr, expr>::iterator keysItor2;
+        std::set<std::pair<expr*, expr*> >::iterator keysItor1 = contain_pair_idx_map[n1].begin();
+        std::set<std::pair<expr*, expr*> >::iterator keysItor2;
 
         for (; keysItor1 != contain_pair_idx_map[n1].end(); keysItor1++) {
             // keysItor1 is on set {<.., n1>, ..., <n1, ...>, ...}
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index e5fd25894..fd93edfd4 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -214,7 +214,9 @@ namespace smt {
         expr_ref_vector contains_map;
 
         theory_str_contain_pair_bool_map_t contain_pair_bool_map;
-        obj_map<expr, obj_pair_set<expr, expr> > contain_pair_idx_map;
+        //obj_map<expr, obj_pair_set<expr, expr> > contain_pair_idx_map;
+        // TODO Find a better data structure, this is 100% a hack right now
+        std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
 
         char * char_set;
         std::map<char, int> charSetLookupTable;