From 3d9139f6efaf9f6fb4a2f6226384a5824ae986a6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 10 Mar 2018 12:07:55 -0800
Subject: [PATCH 01/15] bump revision

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 CMakeLists.txt        | 2 +-
 scripts/mk_project.py | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 62045016a..4d8c15493 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 1)
+set(Z3_VERSION_PATCH 2)
 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 8f75e97ed..2f7402760 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, 1, 0)
+    set_version(4, 6, 2, 0)
     add_lib('util', [])
     add_lib('lp', ['util'], 'util/lp')
     add_lib('polynomial', ['util'], 'math/polynomial')

From 5651d00751a1eb40b94db86f00cb7d3ec9711c4d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 12 Mar 2018 13:21:31 -0700
Subject: [PATCH 02/15] fix #1534

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polynomial/upolynomial.cpp | 18 ++++++++----------
 src/smt/theory_str.cpp              | 18 ++++++++++--------
 src/smt/theory_str.h                |  9 +++++----
 3 files changed, 23 insertions(+), 22 deletions(-)

diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp
index f7cc16de2..cc2442981 100644
--- a/src/math/polynomial/upolynomial.cpp
+++ b/src/math/polynomial/upolynomial.cpp
@@ -781,17 +781,15 @@ namespace upolynomial {
                 set(q.size(), q.c_ptr(), C);
                 m().set(bound, p);
             }
+            else if (q.size() < C.size() || m().m().is_even(p) || m().m().is_even(bound)) {
+                // discard accumulated image, it was affected by unlucky primes
+                TRACE("mgcd", tout << "discarding image\n";);
+                set(q.size(), q.c_ptr(), C);
+                m().set(bound, p);
+            }
             else {
-                if (q.size() < C.size()) {
-                    // discard accumulated image, it was affected by unlucky primes
-                    TRACE("mgcd", tout << "discarding image\n";);
-                    set(q.size(), q.c_ptr(), C);
-                    m().set(bound, p);
-                }
-                else {
-                    CRA_combine_images(q, p, C, bound);
-                    TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";);
-                }
+                CRA_combine_images(q, p, C, bound);
+                TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";);
             }
             numeral_vector & candidate = q;
             get_primitive(C, candidate);
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 3335370eb..0016b8f36 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -5553,7 +5553,8 @@ namespace smt {
         return node;
     }
 
-    void theory_str::get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
+    void theory_str::get_grounded_concats(unsigned depth,
+                                          expr* node, std::map<expr*, expr*> & varAliasMap,
                                           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) {
@@ -5568,6 +5569,9 @@ namespace smt {
         if (groundedMap.find(node) != groundedMap.end()) {
             return;
         }
+        IF_VERBOSE(100, verbose_stream() << "concats " << depth << "\n";
+                   if (depth > 100) verbose_stream() << mk_pp(node, get_manager()) << "\n";
+                   );
 
         // haven't computed grounded concats for "node" (de-aliased)
         // ---------------------------------------------------------
@@ -5595,12 +5599,10 @@ namespace smt {
                 // merge arg0 and arg1
                 expr * arg0 = to_app(node)->get_arg(0);
                 expr * arg1 = to_app(node)->get_arg(1);
-				SASSERT(arg0 != node);
-				SASSERT(arg1 != node);
                 expr * arg0DeAlias = dealias_node(arg0, varAliasMap, concatAliasMap);
                 expr * arg1DeAlias = dealias_node(arg1, varAliasMap, concatAliasMap);
-                get_grounded_concats(arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
-                get_grounded_concats(arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+                get_grounded_concats(depth + 1, arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+                get_grounded_concats(depth + 1, arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
 
                 std::map<std::vector<expr*>, std::set<expr*> >::iterator arg0_grdItor = groundedMap[arg0DeAlias].begin();
                 std::map<std::vector<expr*>, std::set<expr*> >::iterator arg1_grdItor;
@@ -5650,7 +5652,7 @@ namespace smt {
             else if (varEqConcatMap.find(node) != varEqConcatMap.end()) {
                 expr * eqConcat = varEqConcatMap[node].begin()->first;
                 expr * deAliasedEqConcat = dealias_node(eqConcat, varAliasMap, concatAliasMap);
-                get_grounded_concats(deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+                get_grounded_concats(depth + 1, deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
 
                 std::map<std::vector<expr*>, std::set<expr*> >::iterator grdItor = groundedMap[deAliasedEqConcat].begin();
                 for (; grdItor != groundedMap[deAliasedEqConcat].end(); grdItor++) {
@@ -5859,8 +5861,8 @@ namespace smt {
             expr* strDeAlias = dealias_node(str, varAliasMap, concatAliasMap);
             expr* subStrDeAlias = dealias_node(subStr, varAliasMap, concatAliasMap);
 
-            get_grounded_concats(strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
-            get_grounded_concats(subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+            get_grounded_concats(0, strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
+            get_grounded_concats(0, subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
 
             // debugging
             print_grounded_concat(strDeAlias, groundedMap);
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 9288bac7c..64ede71b5 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -495,10 +495,11 @@ protected:
             std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr *> & varConstMap,
             std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap);
     expr * dealias_node(expr * node, std::map<expr*, expr*> & varAliasMap, std::map<expr*, expr*> & concatAliasMap);
-    void get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
-            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);
+    void get_grounded_concats(unsigned depth,
+                              expr* node, std::map<expr*, expr*> & varAliasMap,
+                              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);
     void print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
     void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar,
             std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);

From 5f7bd993de4b83d95e22921d424a7902d0480f83 Mon Sep 17 00:00:00 2001
From: Pierre Pronchery <khorben@defora.org>
Date: Tue, 13 Mar 2018 21:37:22 +0100
Subject: [PATCH 03/15] Add support for NetBSD

Originally from David Holland <dholland@NetBSD.org>.
---
 CMakeLists.txt            |  3 +++
 scripts/mk_util.py        | 17 ++++++++++++++++-
 src/util/scoped_timer.cpp | 18 +++++++++---------
 src/util/stopwatch.h      |  5 +++++
 4 files changed, 33 insertions(+), 10 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 4d8c15493..c11c272be 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -240,6 +240,9 @@ elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
 elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD")
   message(STATUS "Platform: FreeBSD")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_")
+elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "NetBSD")
+  message(STATUS "Platform: NetBSD")
+  list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NetBSD_")
 elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD")
   message(STATUS "Platform: OpenBSD")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_")
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index fecc207d8..99de61703 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -69,6 +69,7 @@ IS_WINDOWS=False
 IS_LINUX=False
 IS_OSX=False
 IS_FREEBSD=False
+IS_NETBSD=False
 IS_OPENBSD=False
 IS_CYGWIN=False
 IS_CYGWIN_MINGW=False
@@ -141,6 +142,9 @@ def is_linux():
 def is_freebsd():
     return IS_FREEBSD
 
+def is_netbsd():
+    return IS_NETBSD
+
 def is_openbsd():
     return IS_OPENBSD
 
@@ -604,6 +608,8 @@ elif os.name == 'posix':
         IS_LINUX=True
     elif os.uname()[0] == 'FreeBSD':
         IS_FREEBSD=True
+    elif os.uname()[0] == 'NetBSD':
+        IS_NETBSD=True
     elif os.uname()[0] == 'OpenBSD':
         IS_OPENBSD=True
     elif os.uname()[0][:6] == 'CYGWIN':
@@ -1245,7 +1251,7 @@ def get_so_ext():
     sysname = os.uname()[0]
     if sysname == 'Darwin':
         return 'dylib'
-    elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD':
+    elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'NetBSD' or sysname == 'OpenBSD':
         return 'so'
     elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
         return 'dll'
@@ -1795,6 +1801,8 @@ class JavaDLLComponent(Component):
                 t = t.replace('PLATFORM', 'linux')
             elif IS_FREEBSD:
                 t = t.replace('PLATFORM', 'freebsd')
+            elif IS_NETBSD:
+                t = t.replace('PLATFORM', 'netbsd')
             elif IS_OPENBSD:
                 t = t.replace('PLATFORM', 'openbsd')
             elif IS_CYGWIN:
@@ -2504,6 +2512,13 @@ def mk_config():
             LDFLAGS        = '%s -lrt' % LDFLAGS
             SLIBFLAGS      = '-shared'
             SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
+        elif sysname == 'NetBSD':
+            CXXFLAGS       = '%s -D_NETBSD_' % CXXFLAGS
+            OS_DEFINES     = '-D_NETBSD_'
+            SO_EXT         = '.so'
+            LDFLAGS        = '%s -lrt' % LDFLAGS
+            SLIBFLAGS      = '-shared'
+            SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
         elif sysname == 'OpenBSD':
             CXXFLAGS       = '%s -D_OPENBSD_' % CXXFLAGS
             OS_DEFINES     = '-D_OPENBSD_'
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index 1ecca8ffe..a2a0cc269 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -33,8 +33,8 @@ Revision History:
 #include<sys/time.h>
 #include<sys/errno.h>
 #include<pthread.h>
-#elif defined(_LINUX_) || defined(_FREEBSD_)
-// Linux
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NetBSD_)
+// Linux & FreeBSD & NetBSD
 #include<errno.h>
 #include<pthread.h>
 #include<sched.h>
@@ -66,8 +66,8 @@ struct scoped_timer::imp {
     pthread_mutex_t  m_mutex;
     pthread_cond_t   m_condition_var;
     struct timespec  m_end_time;
-#elif defined(_LINUX_) || defined(_FREEBSD_)
-    // Linux & FreeBSD
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
+    // Linux & FreeBSD & NetBSD
     pthread_t       m_thread_id;
     pthread_mutex_t m_mutex;
     pthread_cond_t  m_cond;
@@ -104,7 +104,7 @@ struct scoped_timer::imp {
 
         return st;
     }
-#elif defined(_LINUX_) || defined(_FREEBSD_)
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
     static void* thread_func(void *arg) {
         scoped_timer::imp *st = static_cast<scoped_timer::imp*>(arg);
 
@@ -175,8 +175,8 @@ struct scoped_timer::imp {
 
         if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0)
             throw default_exception("failed to start timer thread");
-#elif defined(_LINUX_) || defined(_FREEBSD_)
-        // Linux & FreeBSD
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
+        // Linux & FreeBSD & NetBSD
         m_ms = ms;
         m_initialized = false;
         m_signal_sent = false;
@@ -216,8 +216,8 @@ struct scoped_timer::imp {
             throw default_exception("failed to destroy pthread condition variable");
         if (pthread_attr_destroy(&m_attributes) != 0)
             throw default_exception("failed to destroy pthread attributes object");
-#elif defined(_LINUX_) || defined(_FREEBSD_)
-        // Linux & FreeBSD
+#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
+        // Linux & FreeBSD & NetBSD
         bool init = false;
 
         // spin until timer thread has been created
diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h
index 9ba707af0..83e03a2f7 100644
--- a/src/util/stopwatch.h
+++ b/src/util/stopwatch.h
@@ -134,6 +134,11 @@ public:
 
 #include<ctime>
 
+#ifndef CLOCK_PROCESS_CPUTIME_ID
+/* BSD */
+# define CLOCK_PROCESS_CPUTIME_ID CLOCK_MONOTONIC
+#endif
+
 class stopwatch {
     unsigned long long m_time; // elapsed time in ns
     bool               m_running;

From 2b2aee3c18bee27bee94908d650596e7e5424b64 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 14 Mar 2018 07:29:26 -0700
Subject: [PATCH 04/15] remove unused operators #1530

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

diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 120b0ddfd..5766c79f9 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -1402,7 +1402,6 @@ struct
   let is_rewrite (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE)
   let is_rewrite_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE_STAR)
   let is_pull_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT)
-  let is_pull_quant_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT_STAR)
   let is_push_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PUSH_QUANT)
   let is_elim_unused_vars (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_ELIM_UNUSED_VARS)
   let is_der (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_DER)
@@ -1419,8 +1418,6 @@ struct
   let is_iff_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_IFF_OEQ)
   let is_nnf_pos (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_POS)
   let is_nnf_neg (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_NEG)
-  let is_nnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_STAR)
-  let is_cnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_CNF_STAR)
   let is_skolemize (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_SKOLEMIZE)
   let is_modus_ponens_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_MODUS_PONENS_OEQ)
   let is_theory_lemma (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_TH_LEMMA)

From 5e2723a16ebf1603dc5a048ef98528e40d75d682 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 14 Mar 2018 09:04:08 -0700
Subject: [PATCH 05/15] java

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/java/Context.java | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index ba96209b3..8720fd975 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2543,14 +2543,15 @@ public class Context implements AutoCloseable {
     /**
      * Parse the given string using the SMT-LIB2 parser. 
      * 
-     * @return A conjunction of assertions in the scope (up to push/pop) at the
-     *         end of the string.
+     * @return A conjunction of assertions.
+     *         
+     * If the string contains push/pop commands, the
+     * set of assertions returned are the ones in the 
+     * last scope level.
      **/
     public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
-            Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
-           
+            Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)           
     {
-
         int csn = Symbol.arrayLength(sortNames);
         int cs = Sort.arrayLength(sorts);
         int cdn = Symbol.arrayLength(declNames);

From 46048d51502c749e8a230e9a43e1afdeb439d2dd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 14 Mar 2018 12:15:13 -0700
Subject: [PATCH 06/15] change lemma display utility to use updated pretty
 printer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context_pp.cpp | 52 ++++++++++++++++++++++----------------
 1 file changed, 30 insertions(+), 22 deletions(-)

diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index f5ba52128..e883e0a09 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -19,7 +19,7 @@ Revision History:
 #include "smt/smt_context.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
-#include "ast/ast_smt_pp.h"
+#include "ast/ast_pp_util.h"
 #include "util/stats.h"
 
 namespace smt {
@@ -413,19 +413,23 @@ namespace smt {
     }
 
     void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
-        ast_smt_pp pp(m_manager);
-        pp.set_benchmark_name("lemma");
-        pp.set_status("unsat");
-        pp.set_logic(logic);
+        ast_pp_util visitor(m_manager);
+        expr_ref_vector fmls(m_manager);
+        visitor.collect(fmls);
+        expr_ref n(m_manager);
         for (unsigned i = 0; i < num_antecedents; i++) {
             literal l = antecedents[i];
-            expr_ref n(m_manager);
             literal2expr(l, n);
-            pp.add_assumption(n);
+            fmls.push_back(n);
         }
-        expr_ref n(m_manager);
-        literal2expr(~consequent, n);
-        pp.display_smt2(out, n);
+        if (consequent != false_literal) {
+            literal2expr(~consequent, n);
+            fmls.push_back(n);
+        }
+        if (logic != symbol::null) out << "(set-logic " << logic << ")\n";
+        visitor.collect(fmls);
+        visitor.display_decls(out);
+        visitor.display_asserts(out, fmls, true);
     }
 
     static unsigned g_lemma_id = 0;
@@ -448,25 +452,29 @@ namespace smt {
     void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
                                                unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
                                                literal consequent, symbol const& logic) const {
-        ast_smt_pp pp(m_manager);
-        pp.set_benchmark_name("lemma");
-        pp.set_status("unsat");
-        pp.set_logic(logic);
+        ast_pp_util visitor(m_manager);
+        expr_ref_vector fmls(m_manager);
+        visitor.collect(fmls);
+        expr_ref n(m_manager);
         for (unsigned i = 0; i < num_antecedents; i++) {
             literal l = antecedents[i];
-            expr_ref n(m_manager);
             literal2expr(l, n);
-            pp.add_assumption(n);
+            fmls.push_back(n);
         }
         for (unsigned i = 0; i < num_eq_antecedents; i++) {
             enode_pair const & p = eq_antecedents[i];
-            expr_ref eq(m_manager);
-            eq = m_manager.mk_eq(p.first->get_owner(), p.second->get_owner());
-            pp.add_assumption(eq);
+            n = m_manager.mk_eq(p.first->get_owner(), p.second->get_owner());
+            fmls.push_back(n);
         }
-        expr_ref n(m_manager);
-        literal2expr(~consequent, n);
-        pp.display_smt2(out, n);
+        if (consequent != false_literal) {
+            literal2expr(~consequent, n);
+            fmls.push_back(n);
+        }
+
+        if (logic != symbol::null) out << "(set-logic " << logic << ")\n";
+        visitor.collect(fmls);
+        visitor.display_decls(out);
+        visitor.display_asserts(out, fmls, true);
     }
 
     void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,

From b1f05d8271e1773bb560c58daa2bf3180dacb419 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 14 Mar 2018 18:14:29 -0700
Subject: [PATCH 07/15] fix #1539

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/ml/z3.mli | 23 -----------------------
 1 file changed, 23 deletions(-)

diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 20a1e9c10..14d2ceac4 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -2458,13 +2458,6 @@ sig
       A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. *)
   val is_pull_quant : Expr.expr -> bool
 
-  (** Indicates whether the term is a proof for pulling quantifiers out.
-
-      A proof for (iff P Q) where Q is in prenex normal form.
-      This proof object is only used if the parameter PROOF_MODE is 1.
-      This proof object has no antecedents *)
-  val is_pull_quant_star : Expr.expr -> bool
-
   (** Indicates whether the term is a proof for pushing quantifiers in.
 
       A proof for:
@@ -2658,22 +2651,6 @@ sig
       (and (or r_1 r_2) (or r_1' r_2'))) *)
   val is_nnf_neg : Expr.expr -> bool
 
-  (** Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
-
-      A proof for (~ P Q) where Q is in negation normal form.
-
-      This proof object is only used if the parameter PROOF_MODE is 1.
-
-      This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *)
-  val is_nnf_star : Expr.expr -> bool
-
-  (** Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
-
-      A proof for (~ P Q) where Q is in conjunctive normal form.
-      This proof object is only used if the parameter PROOF_MODE is 1.
-      This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.           *)
-  val is_cnf_star : Expr.expr -> bool
-
   (** Indicates whether the term is a proof for a Skolemization step
 
       Proof for:

From e4cab7bc834b81c8f4d0dcf3fd62668f61e916a0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Filipe=20Gon=C3=A7alves?=
 <fmgoncalves@users.noreply.github.com>
Date: Fri, 16 Mar 2018 22:04:39 +1000
Subject: [PATCH 08/15] Fix #1540 Remove extraneous function

Remove extra __deepcopy__ function definition that shadows working implementation.
---
 src/api/python/z3/z3.py | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index e68d7280d..d4ff556fe 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -368,9 +368,6 @@ class AstRef(Z3PPObject):
     def __copy__(self):
         return self.translate(self.ctx)
 
-    def __deepcopy__(self):
-        return self.translate(self.ctx)
-
     def hash(self):
         """Return a hashcode for the `self`.
 

From 0a0b7a9635d416d117b488639666d25d6b5491be Mon Sep 17 00:00:00 2001
From: Bruce Mitchener <bruce.mitchener@gmail.com>
Date: Fri, 16 Mar 2018 20:56:06 +0700
Subject: [PATCH 09/15] Fix minor issues in docs.

---
 src/api/z3_algebraic.h | 2 +-
 src/api/z3_api.h       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/api/z3_algebraic.h b/src/api/z3_algebraic.h
index faa41bfea..49c61afef 100644
--- a/src/api/z3_algebraic.h
+++ b/src/api/z3_algebraic.h
@@ -31,7 +31,7 @@ extern "C" {
     /** @name Algebraic Numbers */
     /*@{*/
     /**
-       \brief Return Z3_TRUE if \c can be used as value in the Z3 real algebraic
+       \brief Return Z3_TRUE if \c a can be used as value in the Z3 real algebraic
        number package.
 
        def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST)))
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 88d6aa1cf..87bb4d818 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -4350,7 +4350,7 @@ extern "C" {
     Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
 
     /**
-       \brief Return true if the give AST is a real algebraic number.
+       \brief Return true if the given AST is a real algebraic number.
 
        def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST)))
     */

From 86d3bbe6cb8815a20bee5ee29caff12dac9f5202 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 16 Mar 2018 07:46:27 -0700
Subject: [PATCH 10/15] added TODO markers in theory_str.h for moving to
 obj_map, remove include of stdbool for now

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/z3.h                  |  1 -
 src/smt/smt_context_pp.cpp    | 50 ++++++++++++-----------------------
 src/smt/theory_str.cpp        | 17 +++++-------
 src/smt/theory_str.h          | 34 ++++++++----------------
 src/util/obj_pair_hashtable.h | 13 +++++++++
 5 files changed, 48 insertions(+), 67 deletions(-)

diff --git a/src/api/z3.h b/src/api/z3.h
index b29f1d6ba..e08b0c073 100644
--- a/src/api/z3.h
+++ b/src/api/z3.h
@@ -22,7 +22,6 @@ Notes:
 #define Z3_H_
 
 #include <stdio.h>
-#include <stdbool.h>
 #include "z3_macros.h"
 #include "z3_api.h"
 #include "z3_ast_containers.h"
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index e883e0a09..f072a1d13 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -43,11 +43,10 @@ namespace smt {
             return out << "RESOURCE_LIMIT";
         case THEORY:
             if (!m_incomplete_theories.empty()) {
-                ptr_vector<theory>::const_iterator it  = m_incomplete_theories.begin();
-                ptr_vector<theory>::const_iterator end = m_incomplete_theories.end();
-                for (bool first = true; it != end; ++it) {
+                bool first = true;
+                for (theory* th : m_incomplete_theories) {
                     if (first) first = false; else out << " ";
-                    out << (*it)->get_name();
+                    out << th->get_name();
                 }
             }
             else {
@@ -173,12 +172,10 @@ namespace smt {
 
     void context::display_binary_clauses(std::ostream & out) const {
         bool first = true;
-        vector<watch_list>::const_iterator it  = m_watches.begin();
-        vector<watch_list>::const_iterator end = m_watches.end();
-        for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
-            literal l1 = to_literal(l_idx);
+        unsigned l_idx = 0;
+        for (watch_list const& wl : m_watches) {
+            literal l1 = to_literal(l_idx++);
             literal neg_l1 = ~l1;
-            watch_list const & wl = *it;
             literal const * it2  = wl.begin_literals();
             literal const * end2 = wl.end_literals();
             for (; it2 != end2; ++it2) {
@@ -291,10 +288,7 @@ namespace smt {
     }
 
     void context::display_theories(std::ostream & out) const {
-        ptr_vector<theory>::const_iterator it  = m_theory_set.begin();
-        ptr_vector<theory>::const_iterator end = m_theory_set.end();
-        for (; it != end; ++it) {
-            theory * th = *it;
+        for (theory* th : m_theory_set) {
             th->display(out);
         }
     }
@@ -393,10 +387,8 @@ namespace smt {
 #endif
         m_qmanager->collect_statistics(st);
         m_asserted_formulas.collect_statistics(st);
-        ptr_vector<theory>::const_iterator it  = m_theory_set.begin();
-        ptr_vector<theory>::const_iterator end = m_theory_set.end();
-        for (; it != end; ++it) {
-            (*it)->collect_statistics(st);
+        for (theory* th : m_theory_set) {
+            th->collect_statistics(st);
         }
     }
 
@@ -498,10 +490,7 @@ namespace smt {
      */
     void context::display_normalized_enodes(std::ostream & out) const {
         out << "normalized enodes:\n";
-        ptr_vector<enode>::const_iterator it  = m_enodes.begin();
-        ptr_vector<enode>::const_iterator end = m_enodes.end();
-        for (; it != end; ++it) {
-            enode * n = *it;
+        for (enode * n : m_enodes) {
             out << "#";
             out.width(5);
             out << std::left << n->get_owner_id() << " #";
@@ -532,28 +521,23 @@ namespace smt {
     }
 
     void context::display_enodes_lbls(std::ostream & out) const {
-        ptr_vector<enode>::const_iterator it  = m_enodes.begin();
-        ptr_vector<enode>::const_iterator end = m_enodes.end();
-        for (; it != end; ++it) {
-            enode * n = *it;
+        for (enode* n : m_enodes) {
             n->display_lbls(out);
         }
     }
 
     void context::display_decl2enodes(std::ostream & out) const {
         out << "decl2enodes:\n";
-        vector<enode_vector>::const_iterator it1  = m_decl2enodes.begin();
-        vector<enode_vector>::const_iterator end1 = m_decl2enodes.end();
-        for (unsigned id = 0; it1 != end1; ++it1, ++id) {
-            enode_vector const & v = *it1;
+        unsigned id = 0;
+        for (enode_vector const& v : m_decl2enodes) {
             if (!v.empty()) {
                 out << "id " << id << " ->";
-                enode_vector::const_iterator it2  = v.begin();
-                enode_vector::const_iterator end2 = v.end();
-                for (; it2 != end2; ++it2)
-                    out << " #" << (*it2)->get_owner_id();
+                for (enode* n : v) {
+                    out << " #" << n->get_owner_id();
+                }
                 out << "\n";
             }
+            ++id;
         }
     }
 
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 0016b8f36..30092097a 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -288,10 +288,9 @@ 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;
+    static void cut_vars_map_copy(obj_map<expr, int> & dest, obj_map<expr, int> & src) {
+        for (auto const& kv : src) {
+            dest.insert(kv.m_key, 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 const& kv : cut_var_map[n1].top()->vars) {
+            if (cut_var_map[n2].top()->vars.contains(kv.m_key)) {
                 return true;
             }
         }
@@ -2572,9 +2570,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 const& kv : cut_var_map[node].top()->vars) {
+                    xout << mk_pp(kv.m_key, m) << ", ";
                 }
                 xout << std::endl;
             }
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 64ede71b5..09d6498a4 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -77,25 +77,8 @@ public:
     void register_value(expr * n) override { /* Ignore */ }
 };
 
-// rather than modify obj_pair_map I inherit from it and add my own helper methods
-class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {
-public:
-    expr * operator[](std::pair<expr*, expr*> key) const {
-        expr * value;
-        bool found = this->find(key.first, key.second, value);
-        if (found) {
-            return value;
-        } else {
-            TRACE("t_str", tout << "WARNING: lookup miss in contain_pair_bool_map!" << std::endl;);
-            return nullptr;
-        }
-    }
-
-    bool contains(std::pair<expr*, expr*> key) const {
-        expr * unused;
-        return this->find(key.first, key.second, unused);
-    }
-};
+// NSB: added operator[] and contains to obj_pair_hashtable
+class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {};
 
 template<typename Ctx>
 class binary_search_trail : public trail<Ctx> {
@@ -169,7 +152,7 @@ class theory_str : public theory {
     struct T_cut
     {
         int level;
-        std::map<expr*, int> vars;
+        obj_map<expr, int> vars;
 
         T_cut() {
             level = -100;
@@ -292,8 +275,8 @@ protected:
     int tmpXorVarCount;
     int tmpLenTestVarCount;
     int tmpValTestVarCount;
-    std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat;
-
+    // obj_pair_map<expr, expr, std::map<int, expr*> > varForBreakConcat;
+    std::map<std::pair<expr*,expr*>, std::map<int, expr*> > varForBreakConcat;
     bool avoidLoopCut;
     bool loopDetected;
     obj_map<expr, std::stack<T_cut*> > cut_var_map;
@@ -312,9 +295,11 @@ protected:
     obj_hashtable<expr> input_var_in_len;
 
     obj_map<expr, unsigned int> fvar_len_count_map;
+    // TBD: need to replace by obj_map for determinism
     std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
     obj_map<expr, expr*> lenTester_fvar_map;
 
+    // TBD: need to replace by obj_map for determinism
     std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
     std::map<expr*, expr*> valueTester_fvar_map;
 
@@ -322,8 +307,10 @@ protected:
 
     // 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
+    // TBD: need to replace by obj_map for determinism
     std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
     std::map<expr*, expr*> unroll_var_map;
+    // TBD: need to replace by obj_pair_map for determinism
     std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
 
     expr_ref_vector contains_map;
@@ -332,9 +319,10 @@ protected:
     //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;
 
+    // TBD: do a curried map for determinism.
     std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
+    // TBD: need to replace by obj_map for determinism
     std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
-
     std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
 
     svector<char> char_set;
diff --git a/src/util/obj_pair_hashtable.h b/src/util/obj_pair_hashtable.h
index f002a7807..2b8924e9f 100644
--- a/src/util/obj_pair_hashtable.h
+++ b/src/util/obj_pair_hashtable.h
@@ -160,10 +160,23 @@ public:
         }
         return (nullptr != e);
     }
+
+    Value const & find(Key1 * k1, Key2 * k2) const {
+        entry * e = find_core(k1, k2);
+        return e->get_data().get_value();
+    }
+
+    Value const& operator[](std::pair<Key1 *, Key2 *> const& key) const {
+        return find(key.first, key.second);
+    }
   
     bool contains(Key1 * k1, Key2 * k2) const { 
         return find_core(k1, k2) != nullptr;
     }
+
+    bool contains(std::pair<Key1 *, Key2 *> const& key) const {
+        return contains(key.first, key.second);
+    }
     
     void erase(Key1 * k1, Key2 * k2) {
         m_table.remove(key_data(k1, k2));

From b12a1caa0759052380d60fbd1f71a5d8436ac047 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 16 Mar 2018 09:05:44 -0700
Subject: [PATCH 11/15] fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_str.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 30092097a..e1340c301 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -321,7 +321,7 @@ namespace smt {
             T_cut * varInfo = alloc(T_cut);
             m_cut_allocs.push_back(varInfo);
             varInfo->level = slevel;
-            varInfo->vars[node] = 1;
+            varInfo->vars.insert(node, 1);
             cut_var_map.insert(baseNode, std::stack<T_cut*>());
             cut_var_map[baseNode].push(varInfo);
             TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
@@ -330,7 +330,7 @@ namespace smt {
                 T_cut * varInfo = alloc(T_cut);
                 m_cut_allocs.push_back(varInfo);
                 varInfo->level = slevel;
-                varInfo->vars[node] = 1;
+                varInfo->vars.insert(node, 1);
                 cut_var_map[baseNode].push(varInfo);
                 TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
             } else {
@@ -339,11 +339,11 @@ namespace smt {
                     m_cut_allocs.push_back(varInfo);
                     varInfo->level = slevel;
                     cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars);
-                    varInfo->vars[node] = 1;
+                    varInfo->vars.insert(node, 1);
                     cut_var_map[baseNode].push(varInfo);
                     TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
                 } else if (cut_var_map[baseNode].top()->level == slevel) {
-                    cut_var_map[baseNode].top()->vars[node] = 1;
+                    cut_var_map[baseNode].top()->vars.insert(node, 1);
                     TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
                 } else {
                     get_manager().raise_exception("entered illegal state during add_cut_info_one_node()");

From 5dd7e2c520b37c75bfe3c22f1e81911373e1dfed Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 16 Mar 2018 19:30:13 -0700
Subject: [PATCH 12/15] fix #1544

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/z3.h                    |  1 -
 src/ast/rewriter/rewriter_def.h |  2 ++
 src/model/model_evaluator.cpp   | 11 +++++------
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/api/z3.h b/src/api/z3.h
index b29f1d6ba..e08b0c073 100644
--- a/src/api/z3.h
+++ b/src/api/z3.h
@@ -22,7 +22,6 @@ Notes:
 #define Z3_H_
 
 #include <stdio.h>
-#include <stdbool.h>
 #include "z3_macros.h"
 #include "z3_api.h"
 #include "z3_ast_containers.h"
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 878f4ef4c..dfb6542d6 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -194,12 +194,14 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
             result_stack().shrink(fr.m_spos);
             result_stack().push_back(arg);
             fr.m_state = REWRITE_BUILTIN;
+            TRACE("rewriter_step", tout << "step\n" << mk_ismt2_pp(t, m()) << "\n";);
             if (visit<false>(arg, fr.m_max_depth)) {
                 m_r = result_stack().back();
                 result_stack().pop_back();
                 result_stack().pop_back();
                 result_stack().push_back(m_r);
                 cache_result<false>(t, m_r, m_pr, fr.m_cache_result);
+                TRACE("rewriter_step", tout << "step 1\n" << mk_ismt2_pp(m_r, m()) << "\n";);
                 frame_stack().pop_back();
                 set_new_child_flag(t);
             }
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index fd2dc7656..227e14ca6 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -187,14 +187,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
             TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
                   for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n";
                   tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";);
-            return BR_DONE;
+            return BR_REWRITE1;
         }
         if (st == BR_FAILED && !m.is_builtin_family_id(fid))
             st = evaluate_partial_theory_func(f, num, args, result, result_pr);
         if (st == BR_DONE && is_app(result)) {
             app* a = to_app(result);
             if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) {
-                return BR_DONE;
+                return BR_REWRITE1;
             }
         }
         CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
@@ -399,12 +399,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 }
             }
         }
-        args_table::iterator it = table1.begin(), end = table1.end();
-        for (; it != end; ++it) {
-            switch (compare((*it)[arity], else2)) {
+        for (auto const& t : table1) {
+            switch (compare((t)[arity], else2)) {
             case l_true: break;
             case l_false: result = m.mk_false(); return BR_DONE;
-            default: conj.push_back(m.mk_eq((*it)[arity], else2)); break;
+            default: conj.push_back(m.mk_eq((t)[arity], else2)); break;
             }
         }
         result = mk_and(conj);

From aa913c564c7b41fc1a2bb3a198b91f18ff717892 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 17 Mar 2018 04:21:28 -0700
Subject: [PATCH 13/15] moving more std::map std::set to obj_*, #1529

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index e1340c301..69cf80de6 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -441,7 +441,7 @@ namespace smt {
 
     void theory_str::track_variable_scope(expr * var) {
         if (internal_variable_scope_levels.find(sLevel) == internal_variable_scope_levels.end()) {
-            internal_variable_scope_levels[sLevel] = std::set<expr*>();
+            internal_variable_scope_levels[sLevel] = obj_hashtable<expr>();
         }
         internal_variable_scope_levels[sLevel].insert(var);
     }
@@ -6468,9 +6468,9 @@ 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);
+                                regex_nfa_cache.insert(regexTerm, nfa(u, regexTerm));
                             } else {
                                 TRACE("str", tout << "regex_nfa_cache: cache hit" << std::endl;);
                             }
@@ -9286,7 +9286,7 @@ namespace smt {
             h++;
             coverAll = get_next_val_encode(options[options.size() - 1], base);
         }
-        val_range_map[val_indicator] = options[options.size() - 1];
+        val_range_map.insert(val_indicator, options[options.size() - 1]);
 
         TRACE("str",
               tout << "value tester encoding " << "{" << std::endl;
@@ -9380,7 +9380,7 @@ namespace smt {
             TRACE("str", tout << "no previous value testers, or none of them were in scope" << std::endl;);
             int tries = 0;
             expr * val_indicator = mk_internal_valTest_var(freeVar, len, tries);
-            valueTester_fvar_map[val_indicator] = freeVar;
+            valueTester_fvar_map.insert(val_indicator, freeVar);
             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);
@@ -9430,7 +9430,7 @@ namespace smt {
                     refresh_theory_var(valTester);
                 } else {
                     valTester = mk_internal_valTest_var(freeVar, len, i + 1);
-                    valueTester_fvar_map[valTester] = freeVar;
+                    valueTester_fvar_map.insert(valTester, freeVar);
                     fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester));
                     print_value_tester_list(fvar_valueTester_map[freeVar][len]);
                 }
@@ -9595,7 +9595,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);
@@ -9627,8 +9627,9 @@ namespace smt {
                     // put together
                     toAssert = mgr.mk_and(ctx.mk_eq_atom(op0, and1), toAssert);
 
-                    unroll_var_map[unrFunc] = toAssert;
-                } else {
+                    unroll_var_map.insert(unrFunc, toAssert);
+                } 
+                else {
                     toAssert = unroll_var_map[unrFunc];
                 }
             }
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 09d6498a4..508a1c905 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -286,7 +286,7 @@ protected:
     obj_hashtable<expr> variable_set;
     obj_hashtable<expr> internal_variable_set;
     obj_hashtable<expr> regex_variable_set;
-    std::map<int, std::set<expr*> > internal_variable_scope_levels;
+    std::map<int, obj_hashtable<expr> > internal_variable_scope_levels;
 
     obj_hashtable<expr> internal_lenTest_vars;
     obj_hashtable<expr> internal_valTest_vars;
@@ -295,21 +295,20 @@ protected:
     obj_hashtable<expr> input_var_in_len;
 
     obj_map<expr, unsigned int> fvar_len_count_map;
-    // TBD: need to replace by obj_map for determinism
     std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
     obj_map<expr, expr*> lenTester_fvar_map;
 
     // TBD: need to replace by obj_map for determinism
     std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
-    std::map<expr*, expr*> valueTester_fvar_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
     // TBD: need to replace by obj_map for determinism
     std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
-    std::map<expr*, expr*> unroll_var_map;
+    obj_map<expr, expr*> unroll_var_map;
     // TBD: need to replace by obj_pair_map for determinism
     std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
 
@@ -323,7 +322,7 @@ protected:
     std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
     // TBD: need to replace by obj_map for determinism
     std::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 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 14/15] 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 15/15] 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)