From e9ed3af45587900ea179d0393635a0509a5669dc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 1 Jun 2017 09:35:35 -0700
Subject: [PATCH] fix regression in str

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_str.cpp | 2 --
 src/smt/theory_str.h   | 2 +-
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 156e097fe..c2171b9bf 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -100,7 +100,6 @@ namespace smt {
             // valid C strings can't contain the null byte ('\0')
             charSetSize = 255;
             char_set.resize(256, 0);            
-            charSetLookupTable.resize(256, 0);
             int idx = 0;
             // small letters
             for (int i = 97; i < 123; i++) {
@@ -160,7 +159,6 @@ namespace smt {
             const char setset[] = { 'a', 'b', 'c' };
             int fSize = sizeof(setset) / sizeof(char);
             char_set.resize(fSize, 0);
-            charSetLookupTable.resize(fSize, 0);
             charSetSize = fSize;
             for (int i = 0; i < charSetSize; i++) {
                 char_set[i] = setset[i];
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index c56ea8ba2..ae659f0f0 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -331,7 +331,7 @@ protected:
     std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
 
     svector<char> char_set;
-    svector<int>  charSetLookupTable;
+    std::map<char, int>  charSetLookupTable;
     int           charSetSize;
 
     obj_pair_map<expr, expr, expr*> concat_astNode_map;