From 73f7e301c3f60924a8d7e1518e714711eeb5f059 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 12 Mar 2018 17:09:55 -0400
Subject: [PATCH 01/34] preliminary refactoring to use obj_map

---
 src/smt/theory_str.cpp | 19 ++++++++++---------
 src/smt/theory_str.h   | 21 ++++++++++-----------
 2 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 3335370eb..90eb01fa8 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -4582,8 +4582,9 @@ namespace smt {
 
         std::pair<expr*, expr*> key = std::make_pair(concat, unroll);
         expr_ref toAssert(mgr);
+        expr * _toAssert;
 
-        if (concat_eq_unroll_ast_map.find(key) == concat_eq_unroll_ast_map.end()) {
+        if (!concat_eq_unroll_ast_map.find(concat, unroll, _toAssert)) {
             expr_ref arg1(to_app(concat)->get_arg(0), mgr);
             expr_ref arg2(to_app(concat)->get_arg(1), mgr);
             expr_ref r1(to_app(unroll)->get_arg(0), mgr);
@@ -4634,9 +4635,9 @@ namespace smt {
 
             toAssert = mgr.mk_and(opAnd1, opAnd2);
             m_trail.push_back(toAssert);
-            concat_eq_unroll_ast_map[key] = toAssert;
+            concat_eq_unroll_ast_map.insert(concat, unroll, toAssert);
         } else {
-            toAssert = concat_eq_unroll_ast_map[key];
+            toAssert = _toAssert;
         }
 
         assert_axiom(toAssert);
@@ -4920,7 +4921,7 @@ namespace smt {
 
         expr_ref_vector litems(m);
 
-        if (contain_pair_idx_map.find(varNode) != contain_pair_idx_map.end()) {
+        if (contain_pair_idx_map.contains(varNode)) {
             std::set<std::pair<expr*, expr*> >::iterator itor1 = contain_pair_idx_map[varNode].begin();
             for (; itor1 != contain_pair_idx_map[varNode].end(); ++itor1) {
                 expr * strAst = itor1->first;
@@ -5057,7 +5058,7 @@ namespace smt {
         ast_manager & m = get_manager();
         expr_ref_vector litems(m);
 
-        if (contain_pair_idx_map.find(varNode) != contain_pair_idx_map.end()) {
+        if (contain_pair_idx_map.contains(varNode)) {
             std::set<std::pair<expr*, expr*> >::iterator itor1 = contain_pair_idx_map[varNode].begin();
             for (; itor1 != contain_pair_idx_map[varNode].end(); ++itor1) {
                 expr * strAst = itor1->first;
@@ -5125,7 +5126,7 @@ namespace smt {
     }
 
     bool theory_str::in_contain_idx_map(expr * n) {
-        return contain_pair_idx_map.find(n) != contain_pair_idx_map.end();
+        return contain_pair_idx_map.contains(n);
     }
 
     void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) {
@@ -6456,7 +6457,7 @@ namespace smt {
         } else {
             expr_ref_vector::iterator itor = eqNodeSet.begin();
             for (; itor != eqNodeSet.end(); itor++) {
-                if (regex_in_var_reg_str_map.find(*itor) != regex_in_var_reg_str_map.end()) {
+                if (regex_in_var_reg_str_map.contains(*itor)) {
                     std::set<zstring>::iterator strItor = regex_in_var_reg_str_map[*itor].begin();
                     for (; strItor != regex_in_var_reg_str_map[*itor].end(); strItor++) {
                         zstring regStr = *strItor;
@@ -6469,7 +6470,7 @@ namespace smt {
                             expr * regexTerm = a_regexIn->get_arg(1);
 
                             // TODO figure out regex NFA stuff
-                            if (regex_nfa_cache.find(regexTerm) == regex_nfa_cache.end()) {
+                            if (!regex_nfa_cache.contains(regexTerm)) {
                                 TRACE("str", tout << "regex_nfa_cache: cache miss" << std::endl;);
                                 regex_nfa_cache[regexTerm] = nfa(u, regexTerm);
                             } else {
@@ -9596,7 +9597,7 @@ namespace smt {
             if (low.is_neg()) {
                 toAssert = m_autil.mk_ge(cntInUnr, mk_int(0));
             } else {
-                if (unroll_var_map.find(unrFunc) == unroll_var_map.end()) {
+                if (!unroll_var_map.contains(unrFunc)) {
 
                     expr_ref newVar1(mk_regex_rep_var(), mgr);
                     expr_ref newVar2(mk_regex_rep_var(), mgr);
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 9288bac7c..5a249f5dc 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -312,30 +312,29 @@ protected:
     obj_hashtable<expr> input_var_in_len;
 
     obj_map<expr, unsigned int> fvar_len_count_map;
-    std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
+    obj_map<expr, ptr_vector<expr> > fvar_lenTester_map;
     obj_map<expr, expr*> lenTester_fvar_map;
 
-    std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
-    std::map<expr*, expr*> valueTester_fvar_map;
+    obj_map<expr, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
+    obj_map<expr, expr*> valueTester_fvar_map;
 
-    std::map<expr*, int_vector> val_range_map;
+    obj_map<expr, int_vector> val_range_map;
 
     // This can't be an expr_ref_vector because the constructor is wrong,
     // we would need to modify the allocator so we pass in ast_manager
-    std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
-    std::map<expr*, expr*> unroll_var_map;
-    std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
+    obj_map<expr, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
+    obj_map<expr, expr*> unroll_var_map;
+    obj_pair_map<expr, expr, expr*> concat_eq_unroll_ast_map;
 
     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;
-    std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
+    obj_map<expr, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
 
     std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
-    std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
+    obj_map<expr, std::set<zstring> > regex_in_var_reg_str_map;
 
-    std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
+    obj_map<expr, nfa> regex_nfa_cache; // Regex term --> NFA
 
     svector<char> char_set;
     std::map<char, int>  charSetLookupTable;

From b5471e7fe06a2b7a14ccbcdb4273221f54fa8353 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 12 Mar 2018 20:04:04 -0400
Subject: [PATCH 02/34] refactor: use c++11 for (part 1)

---
 src/smt/theory_str.cpp | 167 ++++++++++++++++++-----------------------
 1 file changed, 72 insertions(+), 95 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 90eb01fa8..139e25740 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -289,9 +289,8 @@ namespace smt {
     }
 
     static void cut_vars_map_copy(std::map<expr*, int> & dest, std::map<expr*, int> & src) {
-        std::map<expr*, int>::iterator itor = src.begin();
-        for (; itor != src.end(); itor++) {
-            dest[itor->first] = 1;
+        for (auto entry : src) {
+            dest[entry.first] = 1;
         }
     }
 
@@ -306,9 +305,8 @@ namespace smt {
             return false;
         }
 
-        std::map<expr*, int>::iterator itor = cut_var_map[n1].top()->vars.begin();
-        for (; itor != cut_var_map[n1].top()->vars.end(); ++itor) {
-            if (cut_var_map[n2].top()->vars.find(itor->first) != cut_var_map[n2].top()->vars.end()) {
+        for (auto entry : cut_var_map[n1].top()->vars) {
+            if (cut_var_map[n2].top()->vars.find(entry.first) != cut_var_map[n2].top()->vars.end()) {
                 return true;
             }
         }
@@ -781,8 +779,8 @@ namespace smt {
             ptr_vector<expr> childrenVector;
             get_nodes_in_concat(concatAst, childrenVector);
             expr_ref_vector items(m);
-            for (unsigned int i = 0; i < childrenVector.size(); i++) {
-                items.push_back(mk_strlen(childrenVector.get(i)));
+            for (auto el : childrenVector) {
+                items.push_back(mk_strlen(el));
             }
             expr_ref lenAssert(ctx.mk_eq_atom(concat_length, m_autil.mk_add(items.size(), items.c_ptr())), m);
             assert_axiom(lenAssert);
@@ -802,32 +800,30 @@ namespace smt {
         context & ctx = get_context();
         while (can_propagate()) {
             TRACE("str", tout << "propagating..." << std::endl;);
-            for (unsigned i = 0; i < m_basicstr_axiom_todo.size(); ++i) {
-                instantiate_basic_string_axioms(m_basicstr_axiom_todo[i]);
+            for (auto el : m_basicstr_axiom_todo) {
+                instantiate_basic_string_axioms(el);
             }
             m_basicstr_axiom_todo.reset();
             TRACE("str", tout << "reset m_basicstr_axiom_todo" << std::endl;);
 
-            for (unsigned i = 0; i < m_str_eq_todo.size(); ++i) {
-                std::pair<enode*,enode*> pair = m_str_eq_todo[i];
+            for (auto pair : m_str_eq_todo) {
                 enode * lhs = pair.first;
                 enode * rhs = pair.second;
                 handle_equality(lhs->get_owner(), rhs->get_owner());
             }
             m_str_eq_todo.reset();
 
-            for (unsigned i = 0; i < m_concat_axiom_todo.size(); ++i) {
-                instantiate_concat_axiom(m_concat_axiom_todo[i]);
+            for (auto el : m_concat_axiom_todo) {
+                instantiate_concat_axiom(el);
             }
             m_concat_axiom_todo.reset();
 
-            for (unsigned i = 0; i < m_concat_eval_todo.size(); ++i) {
-                try_eval_concat(m_concat_eval_todo[i]);
+            for (auto el : m_concat_eval_todo) {
+                try_eval_concat(el);
             }
             m_concat_eval_todo.reset();
 
-            for (unsigned i = 0; i < m_library_aware_axiom_todo.size(); ++i) {
-                enode * e = m_library_aware_axiom_todo[i];
+            for (enode * e : m_library_aware_axiom_todo) {
                 app * a = e->get_owner();
                 if (u.str.is_stoi(a)) {
                     instantiate_axiom_str_to_int(e);
@@ -856,10 +852,10 @@ namespace smt {
             }
             m_library_aware_axiom_todo.reset();
 
-            for (unsigned i = 0; i < m_delayed_axiom_setup_terms.size(); ++i) {
+            for (auto el : m_delayed_axiom_setup_terms) {
                 // I think this is okay
-                ctx.internalize(m_delayed_axiom_setup_terms[i].get(), false);
-                set_up_axioms(m_delayed_axiom_setup_terms[i].get());
+                ctx.internalize(el, false);
+                set_up_axioms(el);
             }
             m_delayed_axiom_setup_terms.reset();
         }
@@ -2380,9 +2376,8 @@ namespace smt {
             } else {
                 expr_ref_vector items(m);
                 int pos = 0;
-                std::map<expr*, expr*>::iterator itor = resolvedMap.begin();
-                for (; itor != resolvedMap.end(); ++itor) {
-                    items.push_back(ctx.mk_eq_atom(itor->first, itor->second));
+                for (auto itor : resolvedMap) {
+                    items.push_back(ctx.mk_eq_atom(itor.first, itor.second));
                     pos += 1;
                 }
                 expr_ref premise(mk_and(items), m);
@@ -2558,8 +2553,7 @@ namespace smt {
         context & ctx = get_context();
         // pull each literal out of the arrangement disjunction
         literal_vector ls;
-        for (unsigned i = 0; i < terms.size(); ++i) {
-            expr * e = terms.get(i);
+        for (expr * e : terms) {
             literal l = ctx.get_literal(e);
             ls.push_back(l);
         }
@@ -2572,9 +2566,8 @@ namespace smt {
         if (cut_var_map.contains(node)) {
             if (!cut_var_map[node].empty()) {
                 xout << "[" << cut_var_map[node].top()->level << "] ";
-                std::map<expr*, int>::iterator itor = cut_var_map[node].top()->vars.begin();
-                for (; itor != cut_var_map[node].top()->vars.end(); ++itor) {
-                    xout << mk_pp(itor->first, m) << ", ";
+                for (auto entry : cut_var_map[node].top()->vars) {
+                    xout << mk_pp(entry.first, m) << ", ";
                 }
                 xout << std::endl;
             }
@@ -4498,8 +4491,7 @@ namespace smt {
             }
         }
 
-        for (std::list<unsigned int>::iterator itor = overlapLen.begin(); itor != overlapLen.end(); itor++) {
-            unsigned int overLen = *itor;
+        for (unsigned int overLen : overlapLen) {
             zstring prefix = str1Value.extract(0, str1Len - overLen);
             zstring suffix = str2Value.extract(overLen, str2Len - overLen);
 
@@ -4580,7 +4572,6 @@ namespace smt {
 
         TRACE("str", tout << "concat = " << mk_pp(concat, mgr) << ", unroll = " << mk_pp(unroll, mgr) << std::endl;);
 
-        std::pair<expr*, expr*> key = std::make_pair(concat, unroll);
         expr_ref toAssert(mgr);
         expr * _toAssert;
 
@@ -4922,10 +4913,9 @@ namespace smt {
         expr_ref_vector litems(m);
 
         if (contain_pair_idx_map.contains(varNode)) {
-            std::set<std::pair<expr*, expr*> >::iterator itor1 = contain_pair_idx_map[varNode].begin();
-            for (; itor1 != contain_pair_idx_map[varNode].end(); ++itor1) {
-                expr * strAst = itor1->first;
-                expr * substrAst = itor1->second;
+            for (auto entry : contain_pair_idx_map[varNode]) {
+                expr * strAst = entry.first;
+                expr * substrAst = entry.second;
 
                 expr * boolVar = nullptr;
                 if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) {
@@ -4983,23 +4973,19 @@ namespace smt {
                         // collect eqc concat
                         std::set<expr*> eqcConcats;
                         get_concats_in_eqc(substrAst, eqcConcats);
-                        for (std::set<expr*>::iterator concatItor = eqcConcats.begin();
-                             concatItor != eqcConcats.end(); concatItor++) {
+                        for (expr * aConcat : eqcConcats) {
                             expr_ref_vector constList(m);
                             bool counterEgFound = false;
-                            // get constant strings in concat
-                            expr * aConcat = *concatItor;
                             get_const_str_asts_in_node(aConcat, constList);
-                            for (expr_ref_vector::iterator cstItor = constList.begin();
-                                 cstItor != constList.end(); cstItor++) {
+                            //for (expr_ref_vector::iterator cstItor = constList.begin(); cstItor != constList.end(); cstItor++) {
+                            for (auto cst : constList) {
                                 zstring pieceStr;
-                                u.str.is_string(*cstItor, pieceStr);
+                                u.str.is_string(cst, pieceStr);
                                 if (!strConst.contains(pieceStr)) {
                                     counterEgFound = true;
                                     if (aConcat != substrAst) {
                                         litems.push_back(ctx.mk_eq_atom(substrAst, aConcat));
                                     }
-                                    //implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
                                     implyR = mk_not(m, boolVar);
                                     break;
                                 }
@@ -5059,10 +5045,9 @@ namespace smt {
         expr_ref_vector litems(m);
 
         if (contain_pair_idx_map.contains(varNode)) {
-            std::set<std::pair<expr*, expr*> >::iterator itor1 = contain_pair_idx_map[varNode].begin();
-            for (; itor1 != contain_pair_idx_map[varNode].end(); ++itor1) {
-                expr * strAst = itor1->first;
-                expr * substrAst = itor1->second;
+            for (auto entry : contain_pair_idx_map[varNode]) {
+                expr * strAst = entry.first;
+                expr * substrAst = entry.second;
 
                 expr * boolVar = nullptr;
                 if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) {
@@ -5091,17 +5076,16 @@ namespace smt {
                         zstring strConst;
                         u.str.is_string(strValue, strConst);
                         // iterate eqc (also eqc-to-be) of substr
-                        for (expr_ref_vector::iterator itAst = willEqClass.begin(); itAst != willEqClass.end(); itAst++) {
+                        for (auto itAst : willEqClass) {
                             bool counterEgFound = false;
-                            if (u.str.is_concat(to_app(*itAst))) {
+                            if (u.str.is_concat(to_app(itAst))) {
                                 expr_ref_vector constList(m);
                                 // get constant strings in concat
-                                app * aConcat = to_app(*itAst);
+                                app * aConcat = to_app(itAst);
                                 get_const_str_asts_in_node(aConcat, constList);
-                                for (expr_ref_vector::iterator cstItor = constList.begin();
-                                     cstItor != constList.end(); cstItor++) {
+                                for (auto cst : constList) {
                                     zstring pieceStr;
-                                    u.str.is_string(*cstItor, pieceStr);
+                                    u.str.is_string(cst, pieceStr);
                                     if (!strConst.contains(pieceStr)) {
                                         TRACE("str", tout << "Inconsistency found!" << std::endl;);
                                         counterEgFound = true;
@@ -5134,12 +5118,13 @@ namespace smt {
         ast_manager & m = get_manager();
 
         if (in_contain_idx_map(n1) && in_contain_idx_map(n2)) {
-            std::set<std::pair<expr*, expr*> >::iterator keysItor1 = contain_pair_idx_map[n1].begin();
-            std::set<std::pair<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++) {
+            //for (; keysItor1 != contain_pair_idx_map[n1].end(); keysItor1++) {
+            for (auto key1 : contain_pair_idx_map[n1]) {
                 // keysItor1 is on set {<.., n1>, ..., <n1, ...>, ...}
-                std::pair<expr*, expr*> key1 = *keysItor1;
+                //std::pair<expr*, expr*> key1 = *keysItor1;
                 if (key1.first == n1 && key1.second == n2) {
                     expr_ref implyL(m);
                     expr_ref implyR(contain_pair_bool_map[key1], m);
@@ -5151,10 +5136,10 @@ namespace smt {
                     }
                 }
 
-                for (keysItor2 = contain_pair_idx_map[n2].begin();
-                     keysItor2 != contain_pair_idx_map[n2].end(); keysItor2++) {
+                //for (keysItor2 = contain_pair_idx_map[n2].begin(); keysItor2 != contain_pair_idx_map[n2].end(); keysItor2++) {
+                for (auto key2 : contain_pair_idx_map[n2]) {
                     // keysItor2 is on set {<.., n2>, ..., <n2, ...>, ...}
-                    std::pair<expr*, expr*> key2 = *keysItor2;
+                    //std::pair<expr*, expr*> key2 = *keysItor2;
                     // skip if the pair is eq
                     if (key1 == key2) {
                         continue;
@@ -5248,10 +5233,12 @@ namespace smt {
                                 // * key1.first = key2.first
                                 //   check eqc(key1.second) and eqc(key2.second)
                                 // -----------------------------------------------------------
-                                expr_ref_vector::iterator eqItorSub1 = subAst1Eqc.begin();
-                                for (; eqItorSub1 != subAst1Eqc.end(); eqItorSub1++) {
-                                    expr_ref_vector::iterator eqItorSub2 = subAst2Eqc.begin();
-                                    for (; eqItorSub2 != subAst2Eqc.end(); eqItorSub2++) {
+                                //expr_ref_vector::iterator eqItorSub1 = subAst1Eqc.begin();
+                                //for (; eqItorSub1 != subAst1Eqc.end(); eqItorSub1++) {
+                                for (auto eqSubVar1 : subAst1Eqc) {
+                                    //expr_ref_vector::iterator eqItorSub2 = subAst2Eqc.begin();
+                                    //for (; eqItorSub2 != subAst2Eqc.end(); eqItorSub2++) {
+                                    for (auto eqSubVar2 : subAst2Eqc) {
                                         // ------------
                                         // key1.first = key2.first /\ containPairBoolMap[<eqc(key1.second), eqc(key2.second)>]
                                         // ==>  (containPairBoolMap[key1] --> containPairBoolMap[key2])
@@ -5261,11 +5248,11 @@ namespace smt {
                                             if (n1 != n2) {
                                                 litems3.push_back(ctx.mk_eq_atom(n1, n2));
                                             }
-                                            expr * eqSubVar1 = *eqItorSub1;
+
                                             if (eqSubVar1 != subAst1) {
                                                 litems3.push_back(ctx.mk_eq_atom(subAst1, eqSubVar1));
                                             }
-                                            expr * eqSubVar2 = *eqItorSub2;
+
                                             if (eqSubVar2 != subAst2) {
                                                 litems3.push_back(ctx.mk_eq_atom(subAst2, eqSubVar2));
                                             }
@@ -5286,11 +5273,11 @@ namespace smt {
                                             if (n1 != n2) {
                                                 litems4.push_back(ctx.mk_eq_atom(n1, n2));
                                             }
-                                            expr * eqSubVar1 = *eqItorSub1;
+
                                             if (eqSubVar1 != subAst1) {
                                                 litems4.push_back(ctx.mk_eq_atom(subAst1, eqSubVar1));
                                             }
-                                            expr * eqSubVar2 = *eqItorSub2;
+
                                             if (eqSubVar2 != subAst2) {
                                                 litems4.push_back(ctx.mk_eq_atom(subAst2, eqSubVar2));
                                             }
@@ -5398,20 +5385,18 @@ namespace smt {
                                 // * key1.second = key2.second
                                 //   check eqc(key1.first) and eqc(key2.first)
                                 // -----------------------------------------------------------
-                                expr_ref_vector::iterator eqItorStr1 = str1Eqc.begin();
-                                for (; eqItorStr1 != str1Eqc.end(); eqItorStr1++) {
-                                    expr_ref_vector::iterator eqItorStr2 = str2Eqc.begin();
-                                    for (; eqItorStr2 != str2Eqc.end(); eqItorStr2++) {
+                                for (auto eqStrVar1 : str1Eqc) {
+                                    for (auto eqStrVar2 : str2Eqc) {
                                         {
                                             expr_ref_vector litems3(m);
                                             if (n1 != n2) {
                                                 litems3.push_back(ctx.mk_eq_atom(n1, n2));
                                             }
-                                            expr * eqStrVar1 = *eqItorStr1;
+
                                             if (eqStrVar1 != str1) {
                                                 litems3.push_back(ctx.mk_eq_atom(str1, eqStrVar1));
                                             }
-                                            expr * eqStrVar2 = *eqItorStr2;
+
                                             if (eqStrVar2 != str2) {
                                                 litems3.push_back(ctx.mk_eq_atom(str2, eqStrVar2));
                                             }
@@ -5434,11 +5419,9 @@ namespace smt {
                                             if (n1 != n2) {
                                                 litems4.push_back(ctx.mk_eq_atom(n1, n2));
                                             }
-                                            expr * eqStrVar1 = *eqItorStr1;
                                             if (eqStrVar1 != str1) {
                                                 litems4.push_back(ctx.mk_eq_atom(str1, eqStrVar1));
                                             }
-                                            expr *eqStrVar2 = *eqItorStr2;
                                             if (eqStrVar2 != str2) {
                                                 litems4.push_back(ctx.mk_eq_atom(str2, eqStrVar2));
                                             }
@@ -5484,8 +5467,7 @@ namespace smt {
         expr * constStrAst = (constStrAst_1 != nullptr) ? constStrAst_1 : constStrAst_2;
 
         TRACE("str", tout << "eqc of n1 is {";
-              for (expr_ref_vector::iterator it = willEqClass.begin(); it != willEqClass.end(); ++it) {
-                  expr * el = *it;
+              for (expr * el : willEqClass) {
                   tout << " " << mk_pp(el, m);
               }
               tout << std::endl;
@@ -5498,12 +5480,11 @@ namespace smt {
 
         // step 1: we may have constant values for Contains checks now
         if (constStrAst != nullptr) {
-            expr_ref_vector::iterator itAst = willEqClass.begin();
-            for (; itAst != willEqClass.end(); itAst++) {
-                if (*itAst == constStrAst) {
+            for (auto a : willEqClass) {
+                if (a == constStrAst) {
                     continue;
                 }
-                check_contain_by_eqc_val(*itAst, constStrAst);
+                check_contain_by_eqc_val(a, constStrAst);
             }
         } else {
             // no concrete value to be put in eqc, solely based on context
@@ -5515,9 +5496,8 @@ namespace smt {
             //   * "EQC(M) U EQC(concat(..., "jio", ...))" as substr and
             //   * If strAst registered has an eqc constant in the context
             // -------------------------------------------------------------
-            expr_ref_vector::iterator itAst = willEqClass.begin();
-            for (; itAst != willEqClass.end(); ++itAst) {
-                check_contain_by_substr(*itAst, willEqClass);
+            for (auto a : willEqClass) {
+                check_contain_by_substr(a, willEqClass);
             }
         }
 
@@ -5534,12 +5514,8 @@ namespace smt {
         //         (9) containPairBoolMap[<eqc(y), eqc(x)>] /\ m = n  ==>  (b1 -> b2)
         // ------------------------------------------
 
-        expr_ref_vector::iterator varItor1 = willEqClass.begin();
-        for (; varItor1 != willEqClass.end(); ++varItor1) {
-            expr * varAst1 = *varItor1;
-            expr_ref_vector::iterator varItor2 = varItor1;
-            for (; varItor2 != willEqClass.end(); ++varItor2) {
-                expr * varAst2 = *varItor2;
+        for (auto varAst1 : willEqClass) {
+            for (auto varAst2 : willEqClass) {
                 check_contain_by_eq_nodes(varAst1, varAst2);
             }
         }
@@ -7947,11 +7923,12 @@ namespace smt {
         // Step 1: get variables / concat AST appearing in the context
         // the thing we iterate over should just be variable_set - internal_variable_set
         // so we avoid computing the set difference (but this might be slower)
-        for(obj_hashtable<expr>::iterator it = variable_set.begin(); it != variable_set.end(); ++it) {
-            expr* var = *it;
+        for (expr* var : variable_set) {
+        //for(obj_hashtable<expr>::iterator it = variable_set.begin(); it != variable_set.end(); ++it) {
+            //expr* var = *it;
             if (internal_variable_set.find(var) == internal_variable_set.end()) {
                 TRACE("str", tout << "new variable: " << mk_pp(var, m) << std::endl;);
-                strVarMap[*it] = 1;
+                strVarMap[var] = 1;
             }
         }
         classify_ast_by_type_in_positive_context(strVarMap, concatMap, unrollMap);

From 72f8e408fc39afca1f5c690b20fd86e3518ac687 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 17 Mar 2018 11:25:07 -0700
Subject: [PATCH 03/34] fix #1538

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context_pp.cpp | 6 +++---
 src/smt/theory_seq.cpp     | 8 ++++----
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index f072a1d13..f4f56df5d 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -580,20 +580,20 @@ namespace smt {
         case b_justification::BIN_CLAUSE: {
             literal l2 = j.get_literal();
             out << "bin-clause ";
-            display_literal(out, l2);
+            display_literal_verbose(out, l2);
             break;
         }
         case b_justification::CLAUSE: {
             clause * cls = j.get_clause();
             out << "clause ";
-            if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals());
+            if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals());
             break;
         }
         case b_justification::JUSTIFICATION: {
             out << "justification " << j.get_justification()->get_from_theory() << ": ";
             literal_vector lits;
             const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
-            display_literals(out, lits);
+            display_literals_verbose(out, lits);
             break;
         }
         default:
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index b90735a07..94841603d 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2404,8 +2404,7 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
             lits.push_back(~is_digit(ith_char));
             nums.push_back(digit2int(ith_char));
         }        
-        for (unsigned i = sz-1, c = 1; i > 0; c *= 10) {
-            --i;
+        for (unsigned i = sz, c = 1; i-- > 0; c *= 10) {
             coeff = m_autil.mk_int(c);
             nums[i] = m_autil.mk_mul(coeff, nums[i].get());
         }
@@ -2414,9 +2413,10 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
         lits.push_back(mk_eq(e, num, false));
         ++m_stats.m_add_axiom;
         m_new_propagation = true;
-        for (unsigned i = 0; i < lits.size(); ++i) {
-            ctx.mark_as_relevant(lits[i]);
+        for (literal lit : lits) {
+            ctx.mark_as_relevant(lit);
         }
+        TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";);
         ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
         m_stoi_axioms.insert(val);
         m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_stoi_axioms, val));

From b572639fcdfc622a7615cea821a945f5499a4f08 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 17 Mar 2018 17:49:33 -0700
Subject: [PATCH 04/34] fix #1545

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/python/z3/z3.py        | 27 ++++++++++++++++++++-------
 src/api/python/z3/z3printer.py |  4 +++-
 src/smt/smt_quantifier.cpp     |  2 +-
 3 files changed, 24 insertions(+), 9 deletions(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index d4ff556fe..36283356d 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -114,15 +114,26 @@ def _symbol2py(ctx, s):
 
 # Hack for having nary functions that can receive one argument that is the
 # list of arguments.
+# Use this when function takes a single list of arguments
 def _get_args(args):
-    try:
-        if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
+     try:
+       if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
             return args[0]
-        elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)):
+       elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)):
             return [arg for arg in args[0]]
+       else:
+            return args
+     except:  # len is not necessarily defined when args is not a sequence (use reflection?)
+        return args
+
+# Use this when function takes multiple arguments
+def _get_args_ast_list(args):
+    try:
+        if isinstance(args, set) or isinstance(args, AstVector) or isinstance(args, tuple):
+            return [arg for arg in args]
         else:
             return args
-    except:  # len is not necessarily defined when args is not a sequence (use reflection?)
+    except:
         return args
 
 def _to_param_value(val):
@@ -7943,8 +7954,10 @@ def AtLeast(*args):
     return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
 
 
-def _pb_args_coeffs(args):
-    args  = _get_args(args)
+def _pb_args_coeffs(args, default_ctx = None):
+    args  = _get_args_ast_list(args)
+    if len(args) == 0:
+       return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
     args, coeffs = zip(*args)
     if __debug__:
         _z3_assert(len(args) > 0, "Non empty list of arguments expected")
@@ -7976,7 +7989,7 @@ def PbGe(args, k):
     ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
     return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
-def PbEq(args, k):
+def PbEq(args, k, ctx = None):
     """Create a Pseudo-Boolean inequality k constraint.
 
     >>> a, b, c = Bools('a b c')
diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py
index 3a6b7269e..8fd0c182e 100644
--- a/src/api/python/z3/z3printer.py
+++ b/src/api/python/z3/z3printer.py
@@ -36,7 +36,7 @@ _z3_op_to_str = {
     Z3_OP_CONCAT : 'Concat', Z3_OP_EXTRACT : 'Extract', Z3_OP_BV2INT : 'BV2Int',
     Z3_OP_ARRAY_MAP : 'Map', Z3_OP_SELECT : 'Select', Z3_OP_STORE : 'Store', 
     Z3_OP_CONST_ARRAY : 'K', Z3_OP_ARRAY_EXT : 'Ext', 
-    Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe'
+    Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe', Z3_OP_PB_EQ : 'PbEq'
     }
 
 # List of infix operators
@@ -930,6 +930,8 @@ class Formatter:
                 return self.pp_pbcmp(a, d, f, xs)
             elif k == Z3_OP_PB_GE:
                 return self.pp_pbcmp(a, d, f, xs)
+            elif k == Z3_OP_PB_EQ:
+                return self.pp_pbcmp(a, d, f, xs)
             elif z3.is_pattern(a):
                 return self.pp_pattern(a, d, xs)
             elif self.is_infix(k):
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 0ca244185..1f6811a0f 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -222,7 +222,7 @@ namespace smt {
 
         final_check_status final_check_eh(bool full) {
             if (full) {
-                IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
+                IF_VERBOSE(100, if (!m_quantifiers.empty()) verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
                 final_check_status result  = m_qi_queue.final_check_eh() ? FC_DONE : FC_CONTINUE;
                 final_check_status presult = m_plugin->final_check_eh(full);
                 if (presult != FC_DONE)

From a988d015374869c91302b45f43ff01877817d016 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 19 Mar 2018 12:25:44 -0400
Subject: [PATCH 05/34] add const to iterator loops where it can be used

---
 src/smt/theory_str.cpp | 25 ++++++++++---------------
 1 file changed, 10 insertions(+), 15 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 144ddb9c9..a985ca678 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -800,25 +800,25 @@ namespace smt {
         context & ctx = get_context();
         while (can_propagate()) {
             TRACE("str", tout << "propagating..." << std::endl;);
-            for (auto el : m_basicstr_axiom_todo) {
+            for (auto const& el : m_basicstr_axiom_todo) {
                 instantiate_basic_string_axioms(el);
             }
             m_basicstr_axiom_todo.reset();
             TRACE("str", tout << "reset m_basicstr_axiom_todo" << std::endl;);
 
-            for (auto pair : m_str_eq_todo) {
+            for (auto const& pair : m_str_eq_todo) {
                 enode * lhs = pair.first;
                 enode * rhs = pair.second;
                 handle_equality(lhs->get_owner(), rhs->get_owner());
             }
             m_str_eq_todo.reset();
 
-            for (auto el : m_concat_axiom_todo) {
+            for (auto const& el : m_concat_axiom_todo) {
                 instantiate_concat_axiom(el);
             }
             m_concat_axiom_todo.reset();
 
-            for (auto el : m_concat_eval_todo) {
+            for (auto const& el : m_concat_eval_todo) {
                 try_eval_concat(el);
             }
             m_concat_eval_todo.reset();
@@ -4977,8 +4977,7 @@ namespace smt {
                             expr_ref_vector constList(m);
                             bool counterEgFound = false;
                             get_const_str_asts_in_node(aConcat, constList);
-                            //for (expr_ref_vector::iterator cstItor = constList.begin(); cstItor != constList.end(); cstItor++) {
-                            for (auto cst : constList) {
+                            for (auto const& cst : constList) {
                                 zstring pieceStr;
                                 u.str.is_string(cst, pieceStr);
                                 if (!strConst.contains(pieceStr)) {
@@ -5118,11 +5117,7 @@ namespace smt {
         ast_manager & m = get_manager();
 
         if (in_contain_idx_map(n1) && in_contain_idx_map(n2)) {
-            //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++) {
-            for (auto key1 : contain_pair_idx_map[n1]) {
+            for (auto const& key1 : contain_pair_idx_map[n1]) {
                 // keysItor1 is on set {<.., n1>, ..., <n1, ...>, ...}
                 //std::pair<expr*, expr*> key1 = *keysItor1;
                 if (key1.first == n1 && key1.second == n2) {
@@ -5137,7 +5132,7 @@ namespace smt {
                 }
 
                 //for (keysItor2 = contain_pair_idx_map[n2].begin(); keysItor2 != contain_pair_idx_map[n2].end(); keysItor2++) {
-                for (auto key2 : contain_pair_idx_map[n2]) {
+                for (auto const& key2 : contain_pair_idx_map[n2]) {
                     // keysItor2 is on set {<.., n2>, ..., <n2, ...>, ...}
                     //std::pair<expr*, expr*> key2 = *keysItor2;
                     // skip if the pair is eq
@@ -5385,8 +5380,8 @@ namespace smt {
                                 // * key1.second = key2.second
                                 //   check eqc(key1.first) and eqc(key2.first)
                                 // -----------------------------------------------------------
-                                for (auto eqStrVar1 : str1Eqc) {
-                                    for (auto eqStrVar2 : str2Eqc) {
+                                for (auto const& eqStrVar1 : str1Eqc) {
+                                    for (auto const& eqStrVar2 : str2Eqc) {
                                         {
                                             expr_ref_vector litems3(m);
                                             if (n1 != n2) {
@@ -6944,7 +6939,7 @@ namespace smt {
                         }
                         // now create a fake length tester over this finite disjunction of lengths
 
-                        fvar_len_count_map[v] = 1;
+                        fvar_len_count_map.insert(v, 1);
                         unsigned int testNum = fvar_len_count_map[v];
 
                         expr_ref indicator(mk_internal_lenTest_var(v, testNum), m);

From ebc6ec2eb5348b438b154f531791e8cab5deeb07 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 19 Mar 2018 13:33:58 -0700
Subject: [PATCH 06/34] fix #1547 by rewriting legacy recognizers to SMT-LIB2.6
 style recognizers which are assumed by theory_datatype

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/datatype_decl_plugin.cpp       |  4 ++++
 src/ast/datatype_decl_plugin.h         |  1 +
 src/ast/rewriter/datatype_rewriter.cpp |  3 +++
 src/interp/iz3interp.cpp               | 12 ++++++------
 src/interp/iz3translate.cpp            |  4 ++--
 5 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 44f824959..f685c70d5 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -821,6 +821,10 @@ namespace datatype {
         return d;
     }
 
+    app* util::mk_is(func_decl * c, expr *f) {
+        return m.mk_app(get_constructor_is(c), 1, &f);
+    }
+
     func_decl * util::get_recognizer_constructor(func_decl * recognizer) const {
         SASSERT(is_recognizer(recognizer));
         return to_func_decl(recognizer->get_parameter(0).get_ast());
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index e644ccbda..f32e9990d 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -362,6 +362,7 @@ namespace datatype {
         bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); }
         bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); }
         bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); }
+        app* mk_is(func_decl * c, expr *f);
         ptr_vector<func_decl> const * get_datatype_constructors(sort * ty);
         unsigned get_datatype_num_constructors(sort * ty);
         unsigned get_datatype_num_parameter_sorts(sort * ty);
diff --git a/src/ast/rewriter/datatype_rewriter.cpp b/src/ast/rewriter/datatype_rewriter.cpp
index f0a95929b..194668b9c 100644
--- a/src/ast/rewriter/datatype_rewriter.cpp
+++ b/src/ast/rewriter/datatype_rewriter.cpp
@@ -23,6 +23,9 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
     switch(f->get_decl_kind()) {
     case OP_DT_CONSTRUCTOR: return BR_FAILED;
     case OP_DT_RECOGNISER:
+        SASSERT(num_args == 1);
+        result = m_util.mk_is(m_util.get_recognizer_constructor(f), args[0]);
+        return BR_REWRITE1;
     case OP_DT_IS:
         //
         // simplify is_cons(cons(x,y)) -> true
diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp
index 3d1d84f3c..41c968bd8 100644
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@@ -255,12 +255,12 @@ public:
         catch (const char *msg) {
             throw interpolation_failure(msg);
         }
-        catch (const iz3translation::unsupported &) {
-            TRACE("iz3", tout << "unsupported\n";);
+        catch (const iz3translation::unsupported & ex) {
+            TRACE("iz3", tout << "unsupported " << "\n";);
             throw interpolation_error();
         }
-        catch (const iz3proof::proof_error &) {
-            TRACE("iz3", tout << "proof error\n";);
+        catch (const iz3proof::proof_error & ex) {
+            TRACE("iz3", tout << "proof error " << "\n";);
             throw interpolation_error();
         }
         profiling::timer_stop("Proof translation");
@@ -306,8 +306,8 @@ public:
             catch (const char *msg) {
                 throw interpolation_failure(msg);
             }
-            catch (const iz3translation::unsupported &) {
-                TRACE("iz3", tout << "unsupported\n";);
+            catch (const iz3translation::unsupported & ex) {
+                TRACE("iz3", tout << "unsupported " << "\n";);
                 throw interpolation_error();
             }
             catch (const iz3proof::proof_error &) {
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 9680ec95e..44bac0643 100644
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -2029,8 +2029,8 @@ public:
             case PR_IFF_FALSE: { // turns ~p into p <-> false, noop for us
                 if(is_local(con))
                     res = args[0];
-                else
-                    throw_unsupported(con);
+                else 
+                    throw_unsupported(proof);
                 break;
             }
             case PR_COMMUTATIVITY: {

From 84c30e0b60e795c212bdafa41c18d1609112fb32 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 19 Mar 2018 17:03:01 -0400
Subject: [PATCH 07/34] theory_str fixups for new collections

---
 src/smt/theory_str.cpp | 85 ++++++++++++++++++++++++++++++------------
 1 file changed, 62 insertions(+), 23 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index a985ca678..ec7406d8a 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -967,6 +967,15 @@ namespace smt {
 
         TRACE("str", tout << "set up basic string axioms on " << mk_pp(str->get_owner(), m) << std::endl;);
 
+        {
+            sort * a_sort = m.get_sort(str->get_owner());
+            sort * str_sort = u.str.mk_string_sort();
+            if (a_sort != str_sort) {
+                TRACE("str", tout << "WARNING: not setting up string axioms on non-string term " << mk_pp(str->get_owner(), m) << std::endl;);
+                return;
+            }
+        }
+
         // TESTING: attempt to avoid a crash here when a variable goes out of scope
         if (str->get_iscope_lvl() > ctx.get_scope_level()) {
             TRACE("str", tout << "WARNING: skipping axiom setup on out-of-scope string term" << std::endl;);
@@ -975,6 +984,7 @@ namespace smt {
 
         // generate a stronger axiom for constant strings
         app * a_str = str->get_owner();
+
         if (u.str.is_string(a_str)) {
             expr_ref len_str(m);
             len_str = mk_strlen(a_str);
@@ -1202,6 +1212,12 @@ namespace smt {
             contains_map.push_back(ex);
             std::pair<expr*, expr*> key = std::pair<expr*, expr*>(str, substr);
             contain_pair_bool_map.insert(str, substr, ex);
+            if (!contain_pair_idx_map.contains(str)) {
+                contain_pair_idx_map.insert(str, std::set<std::pair<expr*, expr*>>());
+            }
+            if (!contain_pair_idx_map.contains(substr)) {
+                contain_pair_idx_map.insert(substr, std::set<std::pair<expr*, expr*>>());
+            }
             contain_pair_idx_map[str].insert(key);
             contain_pair_idx_map[substr].insert(key);
         }
@@ -5824,11 +5840,10 @@ namespace smt {
                                       std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
                                       std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap) {
         std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > groundedMap;
-        theory_str_contain_pair_bool_map_t::iterator containItor = contain_pair_bool_map.begin();
-        for (; containItor != contain_pair_bool_map.end(); containItor++) {
-            expr* containBoolVar = containItor->get_value();
-            expr* str = containItor->get_key1();
-            expr* subStr = containItor->get_key2();
+        for (auto const& kv : contain_pair_bool_map) {
+            expr* containBoolVar = kv.get_value();
+            expr* str = kv.get_key1();
+            expr* subStr = kv.get_key2();
 
             expr* strDeAlias = dealias_node(str, varAliasMap, concatAliasMap);
             expr* subStrDeAlias = dealias_node(subStr, varAliasMap, concatAliasMap);
@@ -6889,12 +6904,14 @@ namespace smt {
 
                     if (!map_effectively_empty) {
                         map_effectively_empty = true;
-                        ptr_vector<expr> indicator_set = fvar_lenTester_map[v];
-                        for (ptr_vector<expr>::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) {
-                            expr * indicator = *it;
-                            if (internal_variable_set.find(indicator) != internal_variable_set.end()) {
-                                map_effectively_empty = false;
-                                break;
+                        if (fvar_lenTester_map.contains(v)) {
+                            ptr_vector<expr> indicator_set = fvar_lenTester_map[v];
+                            for (ptr_vector<expr>::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) {
+                                expr * indicator = *it;
+                                if (internal_variable_set.find(indicator) != internal_variable_set.end()) {
+                                    map_effectively_empty = false;
+                                    break;
+                                }
                             }
                         }
                     }
@@ -6946,9 +6963,12 @@ namespace smt {
                         SASSERT(indicator);
                         m_trail.push_back(indicator);
 
+                        if (!fvar_lenTester_map.contains(v)) {
+                            fvar_lenTester_map.insert(v, ptr_vector<expr>());
+                        }
                         fvar_lenTester_map[v].shrink(0);
                         fvar_lenTester_map[v].push_back(indicator);
-                        lenTester_fvar_map[indicator] = v;
+                        lenTester_fvar_map.insert(indicator, v);
 
                         expr_ref_vector orList(m);
                         expr_ref_vector andList(m);
@@ -7015,7 +7035,12 @@ namespace smt {
                 }
             }
         } else {
-            int lenTesterCount = fvar_lenTester_map[fVar].size();
+            int lenTesterCount;
+            if (fvar_lenTester_map.contains(fVar)) {
+                lenTesterCount = fvar_lenTester_map[fVar].size();
+            } else {
+                lenTesterCount = 0;
+            }
 
             expr * effectiveLenInd = nullptr;
             zstring effectiveLenIndiStr = "";
@@ -9336,7 +9361,8 @@ namespace smt {
         // check whether any value tester is actually in scope
         TRACE("str", tout << "checking scope of previous value testers" << std::endl;);
         bool map_effectively_empty = true;
-        if (fvar_valueTester_map[freeVar].find(len) != fvar_valueTester_map[freeVar].end()) {
+        if (fvar_valueTester_map.contains(freeVar) &&
+                fvar_valueTester_map[freeVar].find(len) != fvar_valueTester_map[freeVar].end()) {
             // there's *something* in the map, but check its scope
             svector<std::pair<int, expr*> > entries = fvar_valueTester_map[freeVar][len];
             for (svector<std::pair<int,expr*> >::iterator it = entries.begin(); it != entries.end(); ++it) {
@@ -9357,6 +9383,9 @@ namespace smt {
             int tries = 0;
             expr * val_indicator = mk_internal_valTest_var(freeVar, len, tries);
             valueTester_fvar_map.insert(val_indicator, freeVar);
+            if (!fvar_valueTester_map.contains(freeVar)) {
+                fvar_valueTester_map.insert(freeVar, std::map<int, svector<std::pair<int, expr*> > >());
+            }
             fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, val_indicator));
             print_value_tester_list(fvar_valueTester_map[freeVar][len]);
             return gen_val_options(freeVar, len_indicator, val_indicator, len_valueStr, tries);
@@ -10240,14 +10269,16 @@ namespace smt {
 
                 // assume empty and find a counterexample
                 map_effectively_empty = true;
-                ptr_vector<expr> indicator_set = fvar_lenTester_map[freeVar];
-                for (ptr_vector<expr>::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) {
-                    expr * indicator = *it;
-                    if (internal_variable_set.find(indicator) != internal_variable_set.end()) {
-                        TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m)
-                              << " in fvar_lenTester_map[freeVar]" << std::endl;);
-                        map_effectively_empty = false;
-                        break;
+                if (fvar_lenTester_map.contains(freeVar)) {
+                    ptr_vector<expr> indicator_set = fvar_lenTester_map[freeVar];
+                    for (ptr_vector<expr>::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) {
+                        expr * indicator = *it;
+                        if (internal_variable_set.find(indicator) != internal_variable_set.end()) {
+                            TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m)
+                                    << " in fvar_lenTester_map[freeVar]" << std::endl;);
+                            map_effectively_empty = false;
+                            break;
+                        }
                     }
                 }
                 CTRACE("str", map_effectively_empty, tout << "all variables in fvar_lenTester_map[freeVar] out of scope" << std::endl;);
@@ -10264,6 +10295,9 @@ namespace smt {
                 SASSERT(indicator);
 
                 // since the map is "effectively empty", we can remove those variables that have left scope...
+                if (!fvar_lenTester_map.contains(freeVar)) {
+                    fvar_lenTester_map.insert(freeVar, ptr_vector<expr>());
+                }
                 fvar_lenTester_map[freeVar].shrink(0);
                 fvar_lenTester_map[freeVar].push_back(indicator);
                 lenTester_fvar_map.insert(indicator, freeVar);
@@ -10276,7 +10310,12 @@ namespace smt {
 
                 expr * effectiveLenInd = nullptr;
                 zstring effectiveLenIndiStr("");
-                int lenTesterCount = (int) fvar_lenTester_map[freeVar].size();
+                int lenTesterCount;
+                if (fvar_lenTester_map.contains(freeVar)) {
+                    lenTesterCount = fvar_lenTester_map[freeVar].size();
+                } else {
+                    lenTesterCount = 0;
+                }
 
                 TRACE("str",
                       tout << lenTesterCount << " length testers in fvar_lenTester_map[" << mk_pp(freeVar, m) << "]:" << std::endl;

From 5c692dc79dccb1866e5c2a402128ffe33ec14c7e Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 19 Mar 2018 18:06:42 -0400
Subject: [PATCH 08/34] fixups to theory_str indexof and axiom handling loop

---
 src/smt/theory_str.cpp | 190 ++++++++++++++++++++++++-----------------
 1 file changed, 110 insertions(+), 80 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index ec7406d8a..534acf785 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -638,6 +638,7 @@ namespace smt {
         return contains;
     }
 
+    // note, this invokes "special-case" handling for the start index being 0
     app * theory_str::mk_indexof(expr * haystack, expr * needle) {
         app * indexof = u.str.mk_index(haystack, needle, mk_int(0));
         m_trail.push_back(indexof);
@@ -823,31 +824,49 @@ namespace smt {
             }
             m_concat_eval_todo.reset();
 
-            for (enode * e : m_library_aware_axiom_todo) {
-                app * a = e->get_owner();
-                if (u.str.is_stoi(a)) {
-                    instantiate_axiom_str_to_int(e);
-                } else if (u.str.is_itos(a)) {
-                    instantiate_axiom_int_to_str(e);
-                } else if (u.str.is_at(a)) {
-                    instantiate_axiom_CharAt(e);
-                } else if (u.str.is_prefix(a)) {
-                    instantiate_axiom_prefixof(e);
-                } else if (u.str.is_suffix(a)) {
-                    instantiate_axiom_suffixof(e);
-                } else if (u.str.is_contains(a)) {
-                    instantiate_axiom_Contains(e);
-                } else if (u.str.is_index(a)) {
-                    instantiate_axiom_Indexof(e);
-                } else if (u.str.is_extract(a)) {
-                    instantiate_axiom_Substr(e);
-                } else if (u.str.is_replace(a)) {
-                    instantiate_axiom_Replace(e);
-                } else if (u.str.is_in_re(a)) {
-                    instantiate_axiom_RegexIn(e);
+            while(true) {
+                // Special handling: terms can recursively set up other terms
+                // (e.g. indexof can instantiate other indexof terms).
+                // - Copy the list so it can potentially be modified during setup.
+                // - Don't clear this list if new ones are added in the process;
+                //   instead, set up all the new terms before proceeding.
+                // TODO see if any other propagate() worklists need this kind of handling
+                // TODO we really only need to check the new ones on each pass
+                unsigned start_count = m_library_aware_axiom_todo.size();
+                ptr_vector<enode> axioms_tmp(m_library_aware_axiom_todo);
+                for (auto const& e : axioms_tmp) {
+                    app * a = e->get_owner();
+                    if (u.str.is_stoi(a)) {
+                        instantiate_axiom_str_to_int(e);
+                    } else if (u.str.is_itos(a)) {
+                        instantiate_axiom_int_to_str(e);
+                    } else if (u.str.is_at(a)) {
+                        instantiate_axiom_CharAt(e);
+                    } else if (u.str.is_prefix(a)) {
+                        instantiate_axiom_prefixof(e);
+                    } else if (u.str.is_suffix(a)) {
+                        instantiate_axiom_suffixof(e);
+                    } else if (u.str.is_contains(a)) {
+                        instantiate_axiom_Contains(e);
+                    } else if (u.str.is_index(a)) {
+                        instantiate_axiom_Indexof(e);
+                    } else if (u.str.is_extract(a)) {
+                        instantiate_axiom_Substr(e);
+                    } else if (u.str.is_replace(a)) {
+                        instantiate_axiom_Replace(e);
+                    } else if (u.str.is_in_re(a)) {
+                        instantiate_axiom_RegexIn(e);
+                    } else {
+                        TRACE("str", tout << "BUG: unhandled library-aware term " << mk_pp(e->get_owner(), get_manager()) << std::endl;);
+                        NOT_IMPLEMENTED_YET();
+                    }
+                }
+                unsigned end_count = m_library_aware_axiom_todo.size();
+                if (end_count > start_count) {
+                    TRACE("str", tout << "new library-aware terms added during axiom setup -- checking again" << std::endl;);
+                    continue;
                 } else {
-                    TRACE("str", tout << "BUG: unhandled library-aware term " << mk_pp(e->get_owner(), get_manager()) << std::endl;);
-                    NOT_IMPLEMENTED_YET();
+                    break;
                 }
             }
             m_library_aware_axiom_todo.reset();
@@ -1313,74 +1332,85 @@ namespace smt {
         }
     }
 
-    void theory_str::instantiate_axiom_Indexof_extended(enode * e) {
+    void theory_str::instantiate_axiom_Indexof_extended(enode * _e) {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
-        app * expr = e->get_owner();
-        if (axiomatized_terms.contains(expr)) {
-            TRACE("str", tout << "already set up extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;);
+        app * e = _e->get_owner();
+        if (axiomatized_terms.contains(e)) {
+            TRACE("str", tout << "already set up extended str.indexof axiom for " << mk_pp(e, m) << std::endl;);
             return;
         }
-        SASSERT(expr->get_num_args() == 3);
-        axiomatized_terms.insert(expr);
+        SASSERT(e->get_num_args() == 3);
+        axiomatized_terms.insert(e);
 
-        TRACE("str", tout << "instantiate extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;);
+        TRACE("str", tout << "instantiate extended str.indexof axiom for " << mk_pp(e, m) << std::endl;);
 
-        // -------------------------------------------------------------------------------
-        //   if (arg[2] >= length(arg[0]))                          // ite2
-        //     resAst = -1
-        //   else
-        //     args[0] = prefix . suffix
-        //     /\ indexAst = indexof(suffix, arg[1])
-        //     /\ args[2] = len(prefix)
-        //     /\ if (indexAst == -1)  resAst = indexAst            // ite3
-        //        else   resAst = args[2] + indexAst
-        // -------------------------------------------------------------------------------
+        // str.indexof(H, N, i):
+        // i < 0 --> -1
+        // i == 0 --> str.indexof(H, N, 0)
+        // i >= len(H) --> -1
+        // 0 < i < len(H) -->
+        //     H = hd ++ tl
+        //     len(hd) = i
+        //     str.indexof(tl, N, 0)
 
-        expr_ref resAst(mk_int_var("res"), m);
-        expr_ref indexAst(mk_int_var("index"), m);
-        expr_ref prefix(mk_str_var("prefix"), m);
-        expr_ref suffix(mk_str_var("suffix"), m);
-        expr_ref prefixLen(mk_strlen(prefix), m);
-        expr_ref zeroAst(mk_int(0), m);
-        expr_ref negOneAst(mk_int(-1), m);
+        expr * H; // "haystack"
+        expr * N; // "needle"
+        expr * i; // start index
+        u.str.is_index(e, H, N, i);
 
-        expr_ref ite3(m.mk_ite(
-                          ctx.mk_eq_atom(indexAst, negOneAst),
-                          ctx.mk_eq_atom(resAst, negOneAst),
-                          ctx.mk_eq_atom(resAst, m_autil.mk_add(expr->get_arg(2), indexAst))
-                               ),m);
+        expr_ref minus_one(m_autil.mk_numeral(rational::minus_one(), true), m);
+        expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m);
 
-        expr_ref_vector ite2ElseItems(m);
-        ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(prefix, suffix)));
-        ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1))));
-        ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen));
-        ite2ElseItems.push_back(ite3);
-        expr_ref ite2Else(mk_and(ite2ElseItems), m);
-        SASSERT(ite2Else);
+        // case split
 
-        expr_ref ite2(m.mk_ite(
-                          //m_autil.mk_ge(expr->get_arg(2), mk_strlen(expr->get_arg(0))),
-                          m_autil.mk_ge(m_autil.mk_add(expr->get_arg(2), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))), zeroAst),
-                          ctx.mk_eq_atom(resAst, negOneAst),
-                          ite2Else
-                               ), m);
-        SASSERT(ite2);
+        // case 1: i < 0
+        {
+            expr_ref premise(m_autil.mk_le(i, minus_one), m);
+            expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m);
+            assert_implication(premise, conclusion);
+        }
 
-        expr_ref ite1(m.mk_ite(
-                          //m_autil.mk_lt(expr->get_arg(2), zeroAst),
-                          mk_not(m, m_autil.mk_ge(expr->get_arg(2), zeroAst)),
-                          ctx.mk_eq_atom(resAst, mk_indexof(expr->get_arg(0), expr->get_arg(1))),
-                          ite2
-                               ), m);
-        SASSERT(ite1);
-        assert_axiom(ite1);
+        // case 2: i = 0
+        {
+            expr_ref premise(ctx.mk_eq_atom(i, zero), m);
+            // reduction to simpler case
+            expr_ref conclusion(ctx.mk_eq_atom(e, mk_indexof(H, N)), m);
+            assert_implication(premise, conclusion);
+        }
+        // case 3: i >= len(H)
+        {
+            //expr_ref _premise(m_autil.mk_ge(i, mk_strlen(H)), m);
+            //expr_ref premise(_premise);
+            //th_rewriter rw(m);
+            //rw(premise);
+            expr_ref premise(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero), m);
+            expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m);
+            assert_implication(premise, conclusion);
+        }
+        // case 4: 0 < i < len(H)
+        {
+            expr_ref premise1(m_autil.mk_gt(i, zero), m);
+            expr_ref premise2(m_autil.mk_lt(i, mk_strlen(H)), m);
+            expr_ref _premise(m.mk_and(premise1, premise2), m);
+            expr_ref premise(_premise);
+            th_rewriter rw(m);
+            rw(premise);
 
-        expr_ref reduceTerm(ctx.mk_eq_atom(expr, resAst), m);
-        SASSERT(reduceTerm);
-        assert_axiom(reduceTerm);
+            expr_ref hd(mk_str_var("hd"), m);
+            expr_ref tl(mk_str_var("tl"), m);
 
+            expr_ref_vector conclusion_terms(m);
+            conclusion_terms.push_back(ctx.mk_eq_atom(H, mk_concat(hd, tl)));
+            conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(hd), i));
+            conclusion_terms.push_back(ctx.mk_eq_atom(e, mk_indexof(tl, N)));
+
+            expr_ref conclusion(mk_and(conclusion_terms), m);
+            assert_implication(premise, conclusion);
+        }
+
+        /*
         {
             // heuristic: integrate with str.contains information
             // (but don't introduce it if it isn't already in the instance)
@@ -1394,6 +1424,7 @@ namespace smt {
             // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
             m_delayed_axiom_setup_terms.push_back(containsAxiom);
         }
+        */
     }
 
     void theory_str::instantiate_axiom_LastIndexof(enode * e) {
@@ -7411,8 +7442,7 @@ namespace smt {
 
             if (is_app(ex)) {
                 app * ap = to_app(ex);
-                // TODO indexof2/lastindexof
-                if (u.str.is_index(ap) /* || is_Indexof2(ap) || is_LastIndexof(ap) */) {
+                if (u.str.is_index(ap)) {
                     m_library_aware_axiom_todo.push_back(n);
                 } else if (u.str.is_stoi(ap)) {
                     TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;);

From 1f4bfcb4e5a6dee0e4e5df70f288c6b9a44fd3a1 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 19 Mar 2018 18:10:06 -0400
Subject: [PATCH 09/34] fix indexof subterm

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 534acf785..16fd28d79 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1392,7 +1392,8 @@ namespace smt {
         // case 4: 0 < i < len(H)
         {
             expr_ref premise1(m_autil.mk_gt(i, zero), m);
-            expr_ref premise2(m_autil.mk_lt(i, mk_strlen(H)), m);
+            //expr_ref premise2(m_autil.mk_lt(i, mk_strlen(H)), m);
+            expr_ref premise2(m.mk_not(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero)), m);
             expr_ref _premise(m.mk_and(premise1, premise2), m);
             expr_ref premise(_premise);
             th_rewriter rw(m);

From d26eddf77671dfefb4832c7455077a191751736d Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 19 Mar 2018 18:31:26 -0400
Subject: [PATCH 10/34] re-add indexof-contains heuristic

---
 src/smt/theory_str.cpp | 23 +++++++++++++++--------
 src/smt/theory_str.h   |  1 +
 2 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 16fd28d79..ec554df7b 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -50,6 +50,7 @@ namespace smt {
         m_factory(nullptr),
         m_unused_id(0),
         m_delayed_axiom_setup_terms(m),
+        m_delayed_assertions_todo(m),
         tmpStringVarCount(0),
         tmpXorVarCount(0),
         tmpLenTestVarCount(0),
@@ -793,7 +794,8 @@ namespace smt {
         return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty()
             || !m_concat_axiom_todo.empty() || !m_concat_eval_todo.empty()
             || !m_library_aware_axiom_todo.empty()
-            || !m_delayed_axiom_setup_terms.empty();
+            || !m_delayed_axiom_setup_terms.empty()
+            || (search_started && !m_delayed_assertions_todo.empty())
         ;
     }
 
@@ -877,6 +879,13 @@ namespace smt {
                 set_up_axioms(el);
             }
             m_delayed_axiom_setup_terms.reset();
+
+            if (search_started) {
+                for (auto const& el : m_delayed_assertions_todo) {
+                    assert_axiom(el);
+                }
+                m_delayed_assertions_todo.reset();
+            }
         }
     }
 
@@ -1327,8 +1336,9 @@ namespace smt {
             expr_ref conclusion(m_autil.mk_ge(ex, zeroAst), m);
             expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
             SASSERT(containsAxiom);
+
             // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
-            m_delayed_axiom_setup_terms.push_back(containsAxiom);
+            //m_delayed_axiom_setup_terms.push_back(containsAxiom);
         }
     }
 
@@ -1411,21 +1421,18 @@ namespace smt {
             assert_implication(premise, conclusion);
         }
 
-        /*
         {
             // heuristic: integrate with str.contains information
             // (but don't introduce it if it isn't already in the instance)
-            expr_ref haystack(expr->get_arg(0), m), needle(expr->get_arg(1), m), startIdx(expr->get_arg(2), m);
             // (H contains N) <==> (H indexof N, i) >= 0
-            expr_ref premise(u.str.mk_contains(haystack, needle), m);
+            expr_ref premise(u.str.mk_contains(H, N), m);
             ctx.internalize(premise, false);
-            expr_ref conclusion(m_autil.mk_ge(expr, zeroAst), m);
+            expr_ref conclusion(m_autil.mk_ge(e, zero), m);
             expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
             SASSERT(containsAxiom);
             // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
-            m_delayed_axiom_setup_terms.push_back(containsAxiom);
+            m_delayed_assertions_todo.push_back(containsAxiom);
         }
-        */
     }
 
     void theory_str::instantiate_axiom_LastIndexof(enode * e) {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index cd491ac55..5378b05f3 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -262,6 +262,7 @@ protected:
     ptr_vector<enode> m_concat_axiom_todo;
     ptr_vector<enode> m_string_constant_length_todo;
     ptr_vector<enode> m_concat_eval_todo;
+    expr_ref_vector m_delayed_assertions_todo;
 
     // enode lists for library-aware/high-level string terms (e.g. substr, contains)
     ptr_vector<enode> m_library_aware_axiom_todo;

From 7759d05efee280bd2360584cab43ec33a1d328ba Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 19 Mar 2018 23:09:07 -0400
Subject: [PATCH 11/34] fix use-after-free

---
 src/smt/theory_str.cpp | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index ec554df7b..5a39659e8 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -803,8 +803,20 @@ namespace smt {
         context & ctx = get_context();
         while (can_propagate()) {
             TRACE("str", tout << "propagating..." << std::endl;);
-            for (auto const& el : m_basicstr_axiom_todo) {
-                instantiate_basic_string_axioms(el);
+            while(true) {
+                // this can potentially recursively activate itself
+                unsigned start_count = m_basicstr_axiom_todo.size();
+                ptr_vector<enode> axioms_tmp(m_basicstr_axiom_todo);
+                for (auto const& el : axioms_tmp) {
+                    instantiate_basic_string_axioms(el);
+                }
+                unsigned end_count = m_basicstr_axiom_todo.size();
+                if (end_count > start_count) {
+                    TRACE("str", tout << "new basic string axiom terms added -- checking again" << std::endl;);
+                    continue;
+                } else {
+                    break;
+                }
             }
             m_basicstr_axiom_todo.reset();
             TRACE("str", tout << "reset m_basicstr_axiom_todo" << std::endl;);

From eb6bbd390a93b125a70e4b554b83357dca31e05d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Mar 2018 08:33:09 -0700
Subject: [PATCH 12/34] vsts script

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/vsts-vs2017.cmd | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 scripts/vsts-vs2017.cmd

diff --git a/scripts/vsts-vs2017.cmd b/scripts/vsts-vs2017.cmd
new file mode 100644
index 000000000..3b3a60231
--- /dev/null
+++ b/scripts/vsts-vs2017.cmd
@@ -0,0 +1,40 @@
+echo "Build"
+md build
+cd build
+call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"
+cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -G "NMake Makefiles" ../
+nmake
+rem TBD: test error level
+
+echo "Test python bindings"
+pushd python
+python z3test.py z3
+python z3test.py z3num
+popd
+
+echo "Build and run examples"
+nmake cpp_example
+examples\cpp_example_build_dir\cpp_example.exe
+
+nmake c_example
+examples\c_example_build_dir\c_example.exe
+
+rem nmake java_example
+rem java_example.exe
+
+rem nmake dotnet_example
+rem dotnet_example.exe
+
+echo "Build and run unit tests"
+nmake test-z3
+rem TBD: test error level
+rem test-z3.exe -a
+
+
+cd ..
+echo "Run regression tests"
+git clone https://github.com/z3prover/z3test z3test
+echo "test-benchmarks"
+python z3test\scripts\test_benchmarks.py build\z3.exe z3test\regressions\smt2
+echo "benchmarks tested"
+

From 0d13a2812ee06d2cf3c489e3b40434f5f3e0ec55 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Mar 2018 09:26:39 -0700
Subject: [PATCH 13/34] add error checking and command argument

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/vsts-vs2017.cmd | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/scripts/vsts-vs2017.cmd b/scripts/vsts-vs2017.cmd
index 3b3a60231..d4c1e34b4 100644
--- a/scripts/vsts-vs2017.cmd
+++ b/scripts/vsts-vs2017.cmd
@@ -1,29 +1,37 @@
+rem Supply argument x64 or x86
+
 echo "Build"
 md build
 cd build
-call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars64.bat"
+call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars.bat" %1
 cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -G "NMake Makefiles" ../
 nmake
-rem TBD: test error level
+if ERRORLEVEL 1 exit 1
 
 echo "Test python bindings"
 pushd python
 python z3test.py z3
+if ERRORLEVEL 1 exit 1
 python z3test.py z3num
+if ERRORLEVEL 1 exit 1
 popd
 
 echo "Build and run examples"
 nmake cpp_example
 examples\cpp_example_build_dir\cpp_example.exe
+if ERRORLEVEL 1 exit 1
 
 nmake c_example
 examples\c_example_build_dir\c_example.exe
+if ERRORLEVEL 1 exit 1
 
 rem nmake java_example
 rem java_example.exe
+if ERRORLEVEL 1 exit 1
 
 rem nmake dotnet_example
 rem dotnet_example.exe
+if ERRORLEVEL 1 exit 1
 
 echo "Build and run unit tests"
 nmake test-z3
@@ -36,5 +44,6 @@ echo "Run regression tests"
 git clone https://github.com/z3prover/z3test z3test
 echo "test-benchmarks"
 python z3test\scripts\test_benchmarks.py build\z3.exe z3test\regressions\smt2
+if ERRORLEVEL 1 exit 1
 echo "benchmarks tested"
 

From db7844bef733d3f225d90988034f974945983c91 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Mar 2018 09:33:23 -0700
Subject: [PATCH 14/34] adding build definition

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 README.md               | 6 +++---
 scripts/vsts-vs2017.cmd | 2 +-
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index 70956d439..899d23385 100644
--- a/README.md
+++ b/README.md
@@ -12,9 +12,9 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z
 
 ## Build status
 
-| Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | OSX | TravisCI |
-| ----------- | ----------- | ---------- | ---------- | --- | -------- |
-[![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)
+| Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | OSX | TravisCI |
+| ----------- | ----------- | ----------- | ---------- | ---------- | --- | -------- |
+[![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=2) [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)
 
 [1]: #building-z3-on-windows-using-visual-studio-command-prompt
 [2]: #building-z3-using-make-and-gccclang
diff --git a/scripts/vsts-vs2017.cmd b/scripts/vsts-vs2017.cmd
index d4c1e34b4..fe2f55bca 100644
--- a/scripts/vsts-vs2017.cmd
+++ b/scripts/vsts-vs2017.cmd
@@ -3,7 +3,7 @@ rem Supply argument x64 or x86
 echo "Build"
 md build
 cd build
-call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvars.bat" %1
+call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" %1
 cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -G "NMake Makefiles" ../
 nmake
 if ERRORLEVEL 1 exit 1

From d8462807c3bae35368f07f954189e279ca7a3f2a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Mar 2018 09:35:51 -0700
Subject: [PATCH 15/34] add missin bar

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 899d23385..d501c5d5c 100644
--- a/README.md
+++ b/README.md
@@ -14,7 +14,7 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z
 
 | Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | OSX | TravisCI |
 | ----------- | ----------- | ----------- | ---------- | ---------- | --- | -------- |
-[![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=2) [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)
+[![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=2) | [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)
 
 [1]: #building-z3-on-windows-using-visual-studio-command-prompt
 [2]: #building-z3-using-make-and-gccclang

From f7dfc39984f2f86ea31e719d2de5a371a08c8777 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Mar 2018 12:20:40 -0700
Subject: [PATCH 16/34] add vstsvs2013 outline

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/vsts-vs2013.cmd | 49 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)
 create mode 100644 scripts/vsts-vs2013.cmd

diff --git a/scripts/vsts-vs2013.cmd b/scripts/vsts-vs2013.cmd
new file mode 100644
index 000000000..baf9f4bb4
--- /dev/null
+++ b/scripts/vsts-vs2013.cmd
@@ -0,0 +1,49 @@
+
+set
+echo "Build"
+md build
+cd build
+call "C:\Program Files (x86)\Microsoft Visual Studio\2013\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" x64
+cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -G "NMake Makefiles" ../
+nmake
+if ERRORLEVEL 1 exit 1
+
+echo "Test python bindings"
+pushd python
+python z3test.py z3
+if ERRORLEVEL 1 exit 1
+python z3test.py z3num
+if ERRORLEVEL 1 exit 1
+popd
+
+echo "Build and run examples"
+nmake cpp_example
+examples\cpp_example_build_dir\cpp_example.exe
+if ERRORLEVEL 1 exit 1
+
+nmake c_example
+examples\c_example_build_dir\c_example.exe
+if ERRORLEVEL 1 exit 1
+
+rem nmake java_example
+rem java_example.exe
+if ERRORLEVEL 1 exit 1
+
+rem nmake dotnet_example
+rem dotnet_example.exe
+if ERRORLEVEL 1 exit 1
+
+echo "Build and run unit tests"
+nmake test-z3
+rem TBD: test error level
+rem test-z3.exe -a
+
+
+cd ..
+echo "Run regression tests"
+git clone https://github.com/z3prover/z3test z3test
+echo "test-benchmarks"
+python z3test\scripts\test_benchmarks.py build\z3.exe z3test\regressions\smt2
+if ERRORLEVEL 1 exit 1
+echo "benchmarks tested"
+

From 6ee4efe93a027abc705c9cd756f2c3e4ea308602 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Mar 2018 12:48:21 -0700
Subject: [PATCH 17/34] remove python tests from x86 build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/vsts-vs2017.cmd | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/scripts/vsts-vs2017.cmd b/scripts/vsts-vs2017.cmd
index fe2f55bca..4ec4deca9 100644
--- a/scripts/vsts-vs2017.cmd
+++ b/scripts/vsts-vs2017.cmd
@@ -8,6 +8,7 @@ cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BIN
 nmake
 if ERRORLEVEL 1 exit 1
 
+if %1 == "x86" goto :BUILD_EXAMPLES
 echo "Test python bindings"
 pushd python
 python z3test.py z3
@@ -16,6 +17,7 @@ python z3test.py z3num
 if ERRORLEVEL 1 exit 1
 popd
 
+:BUILD_EXAMPLES
 echo "Build and run examples"
 nmake cpp_example
 examples\cpp_example_build_dir\cpp_example.exe

From 8c4ea7983f5acc24204daab2658f6fc9d45a6015 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Mar 2018 12:59:42 -0700
Subject: [PATCH 18/34] use vc path in 2013

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/vsts-vs2013.cmd | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/vsts-vs2013.cmd b/scripts/vsts-vs2013.cmd
index baf9f4bb4..203c2668e 100644
--- a/scripts/vsts-vs2013.cmd
+++ b/scripts/vsts-vs2013.cmd
@@ -3,7 +3,7 @@ set
 echo "Build"
 md build
 cd build
-call "C:\Program Files (x86)\Microsoft Visual Studio\2013\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" x64
+call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" amd64
 cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -G "NMake Makefiles" ../
 nmake
 if ERRORLEVEL 1 exit 1

From 931dbd5933d77ba4a63b63259a339fa03410f661 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Mar 2018 13:37:04 -0700
Subject: [PATCH 19/34] remove python doc test

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/vsts-vs2013.cmd  | 14 +++----
 src/smt/theory_str.cpp   | 87 +++++++++++++++++-----------------------
 src/smt/theory_str.h     |  3 +-
 src/util/hashtable.h     | 17 ++++----
 src/util/obj_hashtable.h |  3 ++
 5 files changed, 55 insertions(+), 69 deletions(-)

diff --git a/scripts/vsts-vs2013.cmd b/scripts/vsts-vs2013.cmd
index 203c2668e..1676f3e2d 100644
--- a/scripts/vsts-vs2013.cmd
+++ b/scripts/vsts-vs2013.cmd
@@ -8,13 +8,13 @@ cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BIN
 nmake
 if ERRORLEVEL 1 exit 1
 
-echo "Test python bindings"
-pushd python
-python z3test.py z3
-if ERRORLEVEL 1 exit 1
-python z3test.py z3num
-if ERRORLEVEL 1 exit 1
-popd
+rem echo "Test python bindings"
+rem pushd python
+rem python z3test.py z3
+rem if ERRORLEVEL 1 exit 1
+rem python z3test.py z3num
+rem if ERRORLEVEL 1 exit 1
+rem popd
 
 echo "Build and run examples"
 nmake cpp_example
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 69cf80de6..f61293a5f 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -169,6 +169,8 @@ namespace smt {
     }
 
     void theory_str::assert_axiom(expr * _e) {
+        if (_e == nullptr) 
+            return;
         if (opt_VerifyFinalCheckProgress) {
             finalCheckProgressIndicator = true;
         }
@@ -6914,10 +6916,8 @@ namespace smt {
 
                     if (!map_effectively_empty) {
                         map_effectively_empty = true;
-                        ptr_vector<expr> indicator_set = fvar_lenTester_map[v];
-                        for (ptr_vector<expr>::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) {
-                            expr * indicator = *it;
-                            if (internal_variable_set.find(indicator) != internal_variable_set.end()) {
+                        for (expr * indicator : fvar_lenTester_map[v]) {
+                            if (internal_variable_set.contains(indicator)) {
                                 map_effectively_empty = false;
                                 break;
                             }
@@ -8977,12 +8977,12 @@ namespace smt {
 
         CTRACE("str", needToAssignFreeVars,
                tout << "Need to assign values to the following free variables:" << std::endl;
-               for (std::set<expr*>::iterator itx = free_variables.begin(); itx != free_variables.end(); ++itx) {
-                   tout << mk_ismt2_pp(*itx, m) << std::endl;
+               for (expr* v : free_variables) {
+                   tout << mk_ismt2_pp(v, m) << std::endl;
                }
                tout << "freeVar_map has the following entries:" << std::endl;
-               for (std::map<expr*, int>::iterator fvIt = freeVar_map.begin(); fvIt != freeVar_map.end(); fvIt++) {
-                   expr * var = fvIt->first;
+               for (auto const& kv : freeVar_map) {
+                   expr * var = kv.first;
                    tout << mk_ismt2_pp(var, m) << std::endl;
                }
                );
@@ -9360,7 +9360,7 @@ namespace smt {
         // check whether any value tester is actually in scope
         TRACE("str", tout << "checking scope of previous value testers" << std::endl;);
         bool map_effectively_empty = true;
-        if (fvar_valueTester_map[freeVar].find(len) != fvar_valueTester_map[freeVar].end()) {
+        if (fvar_valueTester_map[freeVar].find(len) !=  fvar_valueTester_map[freeVar].end()) {
             // there's *something* in the map, but check its scope
             svector<std::pair<int, expr*> > entries = fvar_valueTester_map[freeVar][len];
             for (svector<std::pair<int,expr*> >::iterator it = entries.begin(); it != entries.end(); ++it) {
@@ -9721,8 +9721,8 @@ namespace smt {
         int dist = opt_LCMUnrollStep;
         expr_ref_vector litems(mgr);
         expr_ref moreAst(mk_string("more"), mgr);
-        for (std::set<expr*>::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) {
-            expr_ref item(ctx.mk_eq_atom(var, *itor), mgr);
+        for (expr * e : unrolls) {
+            expr_ref item(ctx.mk_eq_atom(var, e), mgr);
             TRACE("str", tout << "considering unroll " << mk_pp(item, mgr) << std::endl;);
             litems.push_back(item);
         }
@@ -9731,10 +9731,8 @@ namespace smt {
 
         ptr_vector<expr> outOfScopeTesters;
 
-        for (ptr_vector<expr>::iterator it = unroll_tries_map[var][unrolls].begin();
-             it != unroll_tries_map[var][unrolls].end(); ++it) {
-            expr * tester = *it;
-            bool inScope = (internal_unrollTest_vars.find(tester) != internal_unrollTest_vars.end());
+        for (expr * tester : unroll_tries_map[var][unrolls]) {
+            bool inScope = internal_unrollTest_vars.contains(tester);
             TRACE("str", tout << "unroll test var " << mk_pp(tester, mgr)
                   << (inScope ? " in scope" : " out of scope")
                   << std::endl;);
@@ -9743,12 +9741,10 @@ namespace smt {
             }
         }
 
-        for (ptr_vector<expr>::iterator it = outOfScopeTesters.begin();
-             it != outOfScopeTesters.end(); ++it) {
-            unroll_tries_map[var][unrolls].erase(*it);
+        for (expr* e : outOfScopeTesters) {
+            unroll_tries_map[var][unrolls].erase(e);
         }
 
-
         if (unroll_tries_map[var][unrolls].size() == 0) {
             unroll_tries_map[var][unrolls].push_back(mk_unroll_test_var());
         }
@@ -10265,9 +10261,8 @@ namespace smt {
                 // assume empty and find a counterexample
                 map_effectively_empty = true;
                 ptr_vector<expr> indicator_set = fvar_lenTester_map[freeVar];
-                for (ptr_vector<expr>::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) {
-                    expr * indicator = *it;
-                    if (internal_variable_set.find(indicator) != internal_variable_set.end()) {
+                for (expr * indicator : indicator_set) {
+                    if (internal_variable_set.contains(indicator)) {
                         TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m)
                               << " in fvar_lenTester_map[freeVar]" << std::endl;);
                         map_effectively_empty = false;
@@ -10437,14 +10432,14 @@ namespace smt {
     void theory_str::process_free_var(std::map<expr*, int> & freeVar_map) {
         context & ctx = get_context();
 
-        std::set<expr*> eqcRepSet;
-        std::set<expr*> leafVarSet;
-        std::map<int, std::set<expr*> > aloneVars;
+        obj_hashtable<expr> eqcRepSet;
+        obj_hashtable<expr> leafVarSet;
+        std::map<int, obj_hashtable<expr> > aloneVars;
 
-        for (std::map<expr*, int>::iterator fvIt = freeVar_map.begin(); fvIt != freeVar_map.end(); fvIt++) {
-            expr * freeVar = fvIt->first;
+        for (auto const& kv : freeVar_map) {
+            expr * freeVar = kv.first;
             // skip all regular expression vars
-            if (regex_variable_set.find(freeVar) != regex_variable_set.end()) {
+            if (regex_variable_set.contains(freeVar)) {
                 continue;
             }
 
@@ -10454,10 +10449,10 @@ namespace smt {
             get_var_in_eqc(freeVar, eqVarSet);
             bool duplicated = false;
             expr * dupVar = nullptr;
-            for (std::set<expr*>::iterator itorEqv = eqVarSet.begin(); itorEqv != eqVarSet.end(); itorEqv++) {
-                if (eqcRepSet.find(*itorEqv) != eqcRepSet.end()) {
+            for (expr* eq : eqVarSet) {
+                if (eqcRepSet.contains(eq)) {
                     duplicated = true;
-                    dupVar = *itorEqv;
+                    dupVar = eq;
                     break;
                 }
             }
@@ -10470,13 +10465,9 @@ namespace smt {
             }
         }
 
-        for (std::set<expr*>::iterator fvIt = eqcRepSet.begin(); fvIt != eqcRepSet.end(); fvIt++) {
-            bool standAlone = true;
-            expr * freeVar = *fvIt;
+        for (expr * freeVar : eqcRepSet) {
             // has length constraint initially
-            if (input_var_in_len.find(freeVar) != input_var_in_len.end()) {
-                standAlone = false;
-            }
+            bool standAlone = !input_var_in_len.contains(freeVar);
             // iterate parents
             if (standAlone) {
                 // I hope this works!
@@ -10507,25 +10498,19 @@ namespace smt {
             }
         }
 
-        for(std::set<expr*>::iterator itor1 = leafVarSet.begin();
-            itor1 != leafVarSet.end(); ++itor1) {
-            expr * toAssert = gen_len_val_options_for_free_var(*itor1, nullptr, "");
+        for (expr* lv : leafVarSet) {
+            expr * toAssert = gen_len_val_options_for_free_var(lv, nullptr, "");
             // gen_len_val_options_for_free_var() can legally return NULL,
             // as methods that it calls may assert their own axioms instead.
-            if (toAssert != nullptr) {
-                assert_axiom(toAssert);
-            }
+            if (toAssert) assert_axiom(toAssert);
+            
         }
 
-        for (std::map<int, std::set<expr*> >::iterator mItor = aloneVars.begin();
-             mItor != aloneVars.end(); ++mItor) {
-            std::set<expr*>::iterator itor2 = mItor->second.begin();
-            for(; itor2 != mItor->second.end(); ++itor2) {
-                expr * toAssert = gen_len_val_options_for_free_var(*itor2, nullptr, "");
+        for (auto const& kv : aloneVars) {
+            for (expr* av : kv.second) {
+                expr * toAssert = gen_len_val_options_for_free_var(av, nullptr, "");
                 // same deal with returning a NULL axiom here
-                if(toAssert != nullptr) {
-                    assert_axiom(toAssert);
-                }
+                if (toAssert) assert_axiom(toAssert);                
             }
         }
     }
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 508a1c905..0a8495b14 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -295,7 +295,8 @@ protected:
     obj_hashtable<expr> input_var_in_len;
 
     obj_map<expr, unsigned int> fvar_len_count_map;
-    std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
+    // std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
+    obj_map<expr, ptr_vector<expr> > fvar_lenTester_map;
     obj_map<expr, expr*> lenTester_fvar_map;
 
     // TBD: need to replace by obj_map for determinism
diff --git a/src/util/hashtable.h b/src/util/hashtable.h
index 742438814..4dc05fe4d 100644
--- a/src/util/hashtable.h
+++ b/src/util/hashtable.h
@@ -600,9 +600,8 @@ public:
 
     core_hashtable& operator|=(core_hashtable const& other) {
         if (this == &other) return *this;
-        iterator i = other.begin(), e = other.end();
-        for (; i != e; ++i) {
-            insert(*i);
+        for (const data& d : other) {
+            insert(d);
         }
         return *this;
     }
@@ -610,10 +609,9 @@ public:
     core_hashtable& operator&=(core_hashtable const& other) {
         if (this == &other) return *this;
         core_hashtable copy(*this);
-        iterator i = copy.begin(), e = copy.end();
-        for (; i != e; ++i) {
-            if (!other.contains(*i)) {
-                remove(*i);
+        for (const data& d : copy) {
+            if (!other.contains(d)) {
+                remove(d);
             }
         }
         return *this;
@@ -622,9 +620,8 @@ public:
     core_hashtable& operator=(core_hashtable const& other) {
         if (this == &other) return *this;
         reset();
-        iterator i = other.begin(), e = other.end();
-        for (; i != e; ++i) {
-            insert(*i);
+        for (const data& d : e) {
+            insert(d);
         }
         return *this;
     }
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index 8826e8b76..d042779a8 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -174,6 +174,9 @@ public:
 
     value & find(key * k)  {
         obj_map_entry * e = find_core(k);
+        if (!e) {
+            e = insert_if_not_there2(k, value());
+        }
         SASSERT(e);
         return e->get_data().m_value;
     }

From 4529ad933ac92737e51fb90fbd3b9bdb9e100840 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Mar 2018 15:19:05 -0700
Subject: [PATCH 20/34] add vstsmac

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/vsts-mac.sh | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 scripts/vsts-mac.sh

diff --git a/scripts/vsts-mac.sh b/scripts/vsts-mac.sh
new file mode 100644
index 000000000..807631bba
--- /dev/null
+++ b/scripts/vsts-mac.sh
@@ -0,0 +1,9 @@
+#!/bin/sh
+
+mkdir build
+CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil CXX=clang++ CC=clang python scripts/mk_make.py -x --dotnet --java --python
+cd build
+make
+
+
+

From 3765bde5e993d78cfbcf43a2999b45b18ed7866d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 22 Mar 2018 20:19:08 -0700
Subject: [PATCH 21/34] updated OSX build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/vsts-mac.sh | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/scripts/vsts-mac.sh b/scripts/vsts-mac.sh
index 807631bba..9be53967f 100644
--- a/scripts/vsts-mac.sh
+++ b/scripts/vsts-mac.sh
@@ -1,9 +1,19 @@
 #!/bin/sh
 
+cd ..
 mkdir build
-CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil CXX=clang++ CC=clang python scripts/mk_make.py -x --dotnet --java --python
+CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil CXX=clang++ CC=clang python scripts/mk_make.py  --java --python
 cd build
 make
+make test-z3
+make cpp_example
+make c_example
+# make java_example
+# make python_example
+./cpp_example
+./test_capi
 
-
+git clone https://github.com/z3prover/z3test.git z3test
+ls
+python z3test/scripts/test_benchmarks.py ./z3 ./z3test/regressions/smt2
 

From 705439cb85d00453a2f3ed446d965de34393688e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 22 Mar 2018 20:22:42 -0700
Subject: [PATCH 22/34] update build definition to 4

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index d501c5d5c..e3ef58b70 100644
--- a/README.md
+++ b/README.md
@@ -14,7 +14,7 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z
 
 | Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | OSX | TravisCI |
 | ----------- | ----------- | ----------- | ---------- | ---------- | --- | -------- |
-[![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=2) | [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)
+[![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=4) | [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)
 
 [1]: #building-z3-on-windows-using-visual-studio-command-prompt
 [2]: #building-z3-using-make-and-gccclang

From 966a8f73d33d9ed011286c6fb62fbf6f5449112f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 23 Mar 2018 16:26:20 -0700
Subject: [PATCH 23/34] add eval feature #1553

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_context.h   |  3 +++
 src/api/api_parsers.cpp | 27 +++++++++++++++++++++++++++
 src/api/z3_api.h        | 11 +++++++++++
 3 files changed, 41 insertions(+)

diff --git a/src/api/api_context.h b/src/api/api_context.h
index 7009250cc..185eb9e0f 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -34,6 +34,7 @@ Revision History:
 #include "util/event_handler.h"
 #include "cmd_context/tactic_manager.h"
 #include "cmd_context/context_params.h"
+#include "cmd_context/cmd_context.h"
 #include "api/api_polynomial.h"
 #include "util/hashtable.h"
 
@@ -53,6 +54,7 @@ namespace api {
         context_params             m_params;
         bool                       m_user_ref_count; //!< if true, the user is responsible for managing reference counters.
         scoped_ptr<ast_manager>    m_manager;
+        scoped_ptr<cmd_context>    m_cmd;
         add_plugins                m_plugins;
 
         arith_util                 m_arith_util;
@@ -114,6 +116,7 @@ namespace api {
         ast_manager & m() const { return *(m_manager.get()); }
 
         context_params & params() { return m_params; }
+        scoped_ptr<cmd_context>& cmd() { return m_cmd; }
         bool produce_proofs() const { return m().proofs_enabled(); }
         bool produce_models() const { return m_params.m_model; }
         bool produce_unsat_cores() const { return m_params.m_unsat_core; }
diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index 2e33c1a13..830bef7a8 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -117,4 +117,31 @@ extern "C" {
         RETURN_Z3(r);
         Z3_CATCH_RETURN(nullptr);
     }
+
+    Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str) {
+        Z3_TRY;
+        LOG_Z3_eval_smtlib2_string(c, str);
+        if (!mk_c(c)->cmd()) {
+            mk_c(c)->cmd() = alloc(cmd_context, false, &(mk_c(c)->m()));
+        }
+        scoped_ptr<cmd_context>& ctx = mk_c(c)->cmd();
+        std::string s(str);
+        std::istringstream is(s);
+        std::stringstream ous;
+        ctx->set_regular_stream(ous);
+        try {
+            if (!parse_smt2_commands(*ctx.get(), is)) {
+                mk_c(c)->m_parser_error_buffer = ous.str();
+                SET_ERROR_CODE(Z3_PARSER_ERROR);
+                RETURN_Z3(nullptr);
+            }
+        }
+        catch (z3_exception& e) {
+            mk_c(c)->m_parser_error_buffer = e.msg();
+            SET_ERROR_CODE(Z3_PARSER_ERROR);
+            RETURN_Z3(nullptr);
+        }
+        RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
+        Z3_CATCH_RETURN(nullptr);
+    }
 };
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 87bb4d818..50ed85c70 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -5209,6 +5209,17 @@ extern "C" {
                                         Z3_func_decl const decls[]);
 
 
+    /**
+       \brief Parse and evaluate and SMT-LIB2 command sequence. The state from a previous call is saved so the next
+              evaluation builds on top of the previous call.
+
+       \returns output generated from processing commands.
+
+       def_API('Z3_eval_smtlib2_string', STRING, (_in(CONTEXT), _in(STRING),))
+    */
+
+    Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str);
+    
     /**
        \brief Retrieve that last error message information generated from parsing.
 

From 753f2c89ef70890253b930ec74220aafc209dcbd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 23 Mar 2018 18:54:06 -0700
Subject: [PATCH 24/34] initialize solvers to ensure that eval mode has a
 solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

---
 src/api/api_parsers.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index 830bef7a8..3af2e567c 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -21,8 +21,11 @@ Revision History:
 #include "api/api_context.h"
 #include "api/api_util.h"
 #include "cmd_context/cmd_context.h"
+#include "smt/smt_solver.h"
 #include "parsers/smt2/smt2parser.h"
 #include "solver/solver_na2as.h"
+#include "tactic/portfolio/smt_strategic_solver.h"
+
 
 extern "C" {
 
@@ -123,6 +126,7 @@ extern "C" {
         LOG_Z3_eval_smtlib2_string(c, str);
         if (!mk_c(c)->cmd()) {
             mk_c(c)->cmd() = alloc(cmd_context, false, &(mk_c(c)->m()));
+            mk_c(c)->cmd()->set_solver_factory(mk_smt_strategic_solver_factory());
         }
         scoped_ptr<cmd_context>& ctx = mk_c(c)->cmd();
         std::string s(str);

From fc719a5ee82361ffedb9ef46793e3401fdc32cc5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 24 Mar 2018 10:37:05 -0700
Subject: [PATCH 25/34] fix diagnostic output #1553

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_parsers.cpp       | 12 +++++++-----
 src/cmd_context/cmd_context.h |  1 +
 2 files changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index 3af2e567c..28db62cc3 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -122,6 +122,7 @@ extern "C" {
     }
 
     Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str) {
+        std::stringstream ous;
         Z3_TRY;
         LOG_Z3_eval_smtlib2_string(c, str);
         if (!mk_c(c)->cmd()) {
@@ -131,21 +132,22 @@ extern "C" {
         scoped_ptr<cmd_context>& ctx = mk_c(c)->cmd();
         std::string s(str);
         std::istringstream is(s);
-        std::stringstream ous;
         ctx->set_regular_stream(ous);
+        ctx->set_diagnostic_stream(ous);
         try {
             if (!parse_smt2_commands(*ctx.get(), is)) {
                 mk_c(c)->m_parser_error_buffer = ous.str();
                 SET_ERROR_CODE(Z3_PARSER_ERROR);
-                RETURN_Z3(nullptr);
+                RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
             }
         }
         catch (z3_exception& e) {
-            mk_c(c)->m_parser_error_buffer = e.msg();
+            if (ous.str().empty()) ous << e.msg();
+            mk_c(c)->m_parser_error_buffer = ous.str();
             SET_ERROR_CODE(Z3_PARSER_ERROR);
-            RETURN_Z3(nullptr);
+            RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
         }
         RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
-        Z3_CATCH_RETURN(nullptr);
+        Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str()));
     }
 };
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index d1e470c3b..90b3f6c56 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -406,6 +406,7 @@ public:
     void reset_user_tactics();
     void set_regular_stream(char const * name) { m_regular.set(name); }
     void set_regular_stream(std::ostream& out) { m_regular.set(out); }
+    void set_diagnostic_stream(std::ostream& out) { m_diagnostic.set(out); }
     void set_diagnostic_stream(char const * name);
     std::ostream & regular_stream() override { return *m_regular; }
     std::ostream & diagnostic_stream() override { return *m_diagnostic; }

From bd2ed196e3afde3d575affd127c42503dfde04c2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 25 Mar 2018 19:36:21 -0700
Subject: [PATCH 26/34] add correct badge

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 README.md              | 2 +-
 src/opt/opt_solver.cpp | 3 +++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index e3ef58b70..8ebf6a078 100644
--- a/README.md
+++ b/README.md
@@ -14,7 +14,7 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z
 
 | Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | OSX | TravisCI |
 | ----------- | ----------- | ----------- | ---------- | ---------- | --- | -------- |
-[![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=4) | [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)
+[![win64-badge](https://z3build.visualstudio.com/_apis/public/build/definitions/2e0aa542-a22c-4b1a-8dcd-3ebae8e12db4/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=4) | [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3)
 
 [1]: #building-z3-on-windows-using-visual-studio-command-prompt
 [2]: #building-z3-using-make-and-gccclang
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index c5363816a..785836f56 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -229,6 +229,7 @@ namespace opt {
         inf_eps val = get_optimizer().maximize(v, blocker, has_shared);
         get_model(m_model);
         inf_eps val2;
+        std::cout << m_valid_objectives.size() << " " << i << "\n";
         m_valid_objectives[i] = true;
         TRACE("opt", tout << (has_shared?"has shared":"non-shared") << "\n";);
         if (!m_models[i]) {
@@ -341,6 +342,7 @@ namespace opt {
         
     smt::theory_var opt_solver::add_objective(app* term) {
         smt::theory_var v = get_optimizer().add_objective(term);
+        std::cout << "add objective " << v << "\n";
         m_objective_vars.push_back(v);
         m_objective_values.push_back(inf_eps(rational(-1), inf_rational()));
         m_objective_terms.push_back(term);
@@ -436,6 +438,7 @@ namespace opt {
     } 
 
     void opt_solver::reset_objectives() {
+        std::cout << "reset-objectives\n";
         m_objective_vars.reset();
         m_objective_values.reset();
         m_objective_terms.reset();

From 88e777748ad94c097ff8d2e00359107a9f4aba76 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 25 Mar 2018 19:37:19 -0700
Subject: [PATCH 27/34] remove stdout

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_solver.cpp | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 785836f56..c5363816a 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -229,7 +229,6 @@ namespace opt {
         inf_eps val = get_optimizer().maximize(v, blocker, has_shared);
         get_model(m_model);
         inf_eps val2;
-        std::cout << m_valid_objectives.size() << " " << i << "\n";
         m_valid_objectives[i] = true;
         TRACE("opt", tout << (has_shared?"has shared":"non-shared") << "\n";);
         if (!m_models[i]) {
@@ -342,7 +341,6 @@ namespace opt {
         
     smt::theory_var opt_solver::add_objective(app* term) {
         smt::theory_var v = get_optimizer().add_objective(term);
-        std::cout << "add objective " << v << "\n";
         m_objective_vars.push_back(v);
         m_objective_values.push_back(inf_eps(rational(-1), inf_rational()));
         m_objective_terms.push_back(term);
@@ -438,7 +436,6 @@ namespace opt {
     } 
 
     void opt_solver::reset_objectives() {
-        std::cout << "reset-objectives\n";
         m_objective_vars.reset();
         m_objective_values.reset();
         m_objective_terms.reset();

From 78744e589c5a3213929b09174fb19bfb0abf6ee0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Mar 2018 12:19:24 -0700
Subject: [PATCH 28/34] add stdbool.h

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

diff --git a/src/api/z3.h b/src/api/z3.h
index e08b0c073..b29f1d6ba 100644
--- a/src/api/z3.h
+++ b/src/api/z3.h
@@ -22,6 +22,7 @@ Notes:
 #define Z3_H_
 
 #include <stdio.h>
+#include <stdbool.h>
 #include "z3_macros.h"
 #include "z3_api.h"
 #include "z3_ast_containers.h"

From 76dec85c93233922d4c79eb98c2b6c237e8c3b15 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Mar 2018 15:41:53 -0700
Subject: [PATCH 29/34] use stdbool #1526 instead of int

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/update_api.py   |  7 ++++++-
 src/api/z3_api.h        |  2 +-
 src/api/z3_replayer.cpp | 10 ++++++++++
 src/api/z3_replayer.h   |  1 +
 4 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/scripts/update_api.py b/scripts/update_api.py
index 18878d6ea..0a86db18d 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -957,11 +957,16 @@ def def_API(name, result, params):
                 log_c.write(" }\n")
                 log_c.write("  Au(a%s);\n" % sz)
                 exe_c.write("in.get_uint_array(%s)" % i)
-            elif ty == INT or ty == BOOL:
+            elif ty == INT:
                 log_c.write("U(a%s[i]);" % i)
                 log_c.write(" }\n")
                 log_c.write("  Au(a%s);\n" % sz)
                 exe_c.write("in.get_int_array(%s)" % i)
+            elif ty == BOOL:
+                log_c.write("U(a%s[i]);" % i)
+                log_c.write(" }\n")
+                log_c.write("  Au(a%s);\n" % sz)
+                exe_c.write("in.get_bool_array(%s)" % i)
             else:
                 error ("unsupported parameter for %s, %s, %s" % (ty, name, p))
         elif kind == OUT_ARRAY:
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 50ed85c70..ab570581b 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -82,7 +82,7 @@ DEFINE_TYPE(Z3_rcf_num);
 /**
    \brief Z3 Boolean type. It is just an alias for \c int.
 */
-typedef int Z3_bool;
+typedef bool Z3_bool;
 
 /**
    \brief Z3 string type. It is just an alias for \ccode{const char *}.
diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp
index 1515e6df7..fde9b1f48 100644
--- a/src/api/z3_replayer.cpp
+++ b/src/api/z3_replayer.cpp
@@ -630,6 +630,12 @@ struct z3_replayer::imp {
         return m_int_arrays[idx].c_ptr();
     }
 
+    bool * get_bool_array(unsigned pos) const {
+        check_arg(pos, UINT_ARRAY);
+        unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
+        return reinterpret_cast<bool*>(m_unsigned_arrays[idx].c_ptr());
+    }
+
     Z3_symbol * get_symbol_array(unsigned pos) const {
         check_arg(pos, SYMBOL_ARRAY);
         unsigned idx = static_cast<unsigned>(m_args[pos].m_uint);
@@ -761,6 +767,10 @@ int * z3_replayer::get_int_array(unsigned pos) const {
     return m_imp->get_int_array(pos);
 }
 
+bool * z3_replayer::get_bool_array(unsigned pos) const {
+    return m_imp->get_bool_array(pos);
+}
+
 Z3_symbol * z3_replayer::get_symbol_array(unsigned pos) const {
     return m_imp->get_symbol_array(pos);
 }
diff --git a/src/api/z3_replayer.h b/src/api/z3_replayer.h
index e1b32af75..b81659945 100644
--- a/src/api/z3_replayer.h
+++ b/src/api/z3_replayer.h
@@ -51,6 +51,7 @@ public:
 
     unsigned * get_uint_array(unsigned pos) const;
     int * get_int_array(unsigned pos) const;
+    bool * get_bool_array(unsigned pos) const;
     Z3_symbol * get_symbol_array(unsigned pos) const;
     void ** get_obj_array(unsigned pos) const;
 

From 32c9af5e5a4b119dc09eaae2bd05acf5ec7859db Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Mar 2018 16:16:25 -0700
Subject: [PATCH 30/34] fix use of Z3_bool -> Z3_lbool

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/c/test_capi.c | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
index b947928a7..c2b1f0af9 100644
--- a/examples/c/test_capi.c
+++ b/examples/c/test_capi.c
@@ -2452,7 +2452,6 @@ Z3_lbool ext_check(Z3_ext_context ctx) {
         }
         printf("\n");
     }
-
     return result;
 }
 
@@ -2464,7 +2463,7 @@ void incremental_example1() {
     Z3_context     ctx     = ext_ctx->m_context;
     Z3_ast x, y, z, two, one;
     unsigned c1, c2, c3, c4;
-    Z3_bool result;
+    Z3_lbool result;
 
     printf("\nincremental_example1\n");
     LOG_MSG("incremental_example1");
@@ -2485,7 +2484,7 @@ void incremental_example1() {
     c4 = assert_retractable_cnstr(ext_ctx, Z3_mk_lt(ctx, y, one));
 
     result = ext_check(ext_ctx);
-    if (result != Z3_L_FALSE)
+    if (result != Z3_L_FALSE) 
         exitf("bug in Z3");
     printf("unsat\n");
 

From b9f2188fc02c0e171103b383a8684a5199a3c232 Mon Sep 17 00:00:00 2001
From: Bruce Mitchener <bruce.mitchener@gmail.com>
Date: Fri, 30 Mar 2018 22:34:07 +0700
Subject: [PATCH 31/34] Update Z3_bool doc.

---
 src/api/z3_api.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index ab570581b..2b46127fa 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -80,7 +80,7 @@ DEFINE_TYPE(Z3_rcf_num);
 */
 
 /**
-   \brief Z3 Boolean type. It is just an alias for \c int.
+   \brief Z3 Boolean type. It is just an alias for \c bool.
 */
 typedef bool Z3_bool;
 

From 21a3b9c8e2d61af7b0b71260430402c68bbf2585 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 31 Mar 2018 05:20:47 -0700
Subject: [PATCH 32/34] increment version number due to ABI/API breaking change
 #1556

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 CMakeLists.txt                 | 2 +-
 scripts/mk_project.py          | 2 +-
 src/api/dotnet/AlgebraicNum.cs | 4 ++--
 src/api/dotnet/BitVecNum.cs    | 4 ++--
 4 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index c11c272be..bd3774ac7 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -34,7 +34,7 @@ endif()
 ################################################################################
 set(Z3_VERSION_MAJOR 4)
 set(Z3_VERSION_MINOR 6)
-set(Z3_VERSION_PATCH 2)
+set(Z3_VERSION_PATCH 3)
 set(Z3_VERSION_TWEAK 0)
 set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
 set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 2f7402760..b77975dfa 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -9,7 +9,7 @@ from mk_util import *
 
 # Z3 Project definition
 def init_project_def():
-    set_version(4, 6, 2, 0)
+    set_version(4, 6, 3, 0)
     add_lib('util', [])
     add_lib('lp', ['util'], 'util/lp')
     add_lib('polynomial', ['util'], 'math/polynomial')
diff --git a/src/api/dotnet/AlgebraicNum.cs b/src/api/dotnet/AlgebraicNum.cs
index 66552f1a0..3687e1f83 100644
--- a/src/api/dotnet/AlgebraicNum.cs
+++ b/src/api/dotnet/AlgebraicNum.cs
@@ -3,11 +3,11 @@ Copyright (c) 2012 Microsoft Corporation
 
 Module Name:
 
-    IntNum.cs
+    AlgebraicNum.cs
 
 Abstract:
 
-    Z3 Managed API: Int Numerals
+    Z3 Managed API: Algebraic Numerals
 
 Author:
 
diff --git a/src/api/dotnet/BitVecNum.cs b/src/api/dotnet/BitVecNum.cs
index c6ac471f6..66054761a 100644
--- a/src/api/dotnet/BitVecNum.cs
+++ b/src/api/dotnet/BitVecNum.cs
@@ -3,11 +3,11 @@ Copyright (c) 2012 Microsoft Corporation
 
 Module Name:
 
-    IntNum.cs
+    BitVecNum.cs
 
 Abstract:
 
-    Z3 Managed API: Int Numerals
+    Z3 Managed API: BitVec Numerals
 
 Author:
 

From 6b38edf102a84e9b6da62f8700107276a9791502 Mon Sep 17 00:00:00 2001
From: Moritz Kiefer <moritz.kiefer@purelyfunctional.org>
Date: Tue, 3 Apr 2018 11:57:31 +0200
Subject: [PATCH 33/34] Fix buffering issue in print_success for
 declare-datatype

---
 src/parsers/smt2/smt2parser.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 9265312d4..e72b9ad79 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -949,8 +949,9 @@ namespace smt2 {
             check_duplicate(d, line, pos);
 
             d->commit(pm());
-            check_rparen_next("invalid end of datatype declaration, ')' expected");
+            check_rparen("invalid end of datatype declaration, ')' expected");
             m_ctx.print_success();
+            next();
         }
 
 

From 5ba939ad5eabac44317ecd24867b00d0a632be9a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Apr 2018 12:40:18 -0700
Subject: [PATCH 34/34] add tuple shortcut and example to C++ API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/c++/example.cpp | 11 +++++++++++
 src/api/c++/z3++.h       | 22 ++++++++++++++++++++++
 2 files changed, 33 insertions(+)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index df977268a..ed5bf7086 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -920,6 +920,16 @@ void enum_sort_example() {
     std::cout << "2: " << result_goal.as_expr() << std::endl;
 }
 
+void tuple_example() {
+    std::cout << "tuple example\n";
+    context ctx;
+    const char * names[] = { "first", "second" };
+    sort sorts[2] = { ctx.int_sort(), ctx.bool_sort() };
+    func_decl_vector projs(ctx);
+    func_decl pair = ctx.tuple_sort("pair", 2, names, sorts, projs);
+    std::cout << pair << "\n";
+}
+
 void expr_vector_example() {
     std::cout << "expr_vector example\n";
     context c;
@@ -1179,6 +1189,7 @@ int main() {
         incremental_example2(); std::cout << "\n";
         incremental_example3(); std::cout << "\n";
         enum_sort_example(); std::cout << "\n";
+        tuple_example(); std::cout << "\n";
         expr_vector_example(); std::cout << "\n";
         exists_expr_vector_example(); std::cout << "\n";
         substitute_example(); std::cout << "\n";
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 42467cb22..6f46f9440 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -267,6 +267,15 @@ namespace z3 {
            and in \c ts the predicates for testing if terms of the enumeration sort correspond to an enumeration.
         */
         sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
+
+        /**
+           \brief Return a tuple constructor.
+           \c name is the name of the returned constructor,
+           \c n are the number of arguments, \c names and \c sorts are their projected sorts.
+           \c projs is an output paramter. It contains the set of projection functions.
+        */
+        func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
+
         /**
            \brief create an uninterpreted sort with the name given by the string or symbol.
          */
@@ -2432,6 +2441,19 @@ namespace z3 {
         for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
         return s;
     }
+    inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
+        array<Z3_symbol> _names(n);
+        array<Z3_sort> _sorts(n);
+        for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
+        array<Z3_func_decl> _projs(n);
+        Z3_symbol _name = Z3_mk_string_symbol(*this, name);
+        Z3_func_decl tuple;
+        sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
+        check_error();
+        for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
+        return func_decl(*this, tuple);
+    }
+
     inline sort context::uninterpreted_sort(char const* name) {
         Z3_symbol _name = Z3_mk_string_symbol(*this, name);
         return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));