From 3ca85913476fc71d515518e178dd2ae8787b386c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 28 Jul 2014 09:59:35 -0700
Subject: [PATCH 01/14] take theory explanation into account

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 02ee06985..4f3c73ce6 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3945,7 +3945,7 @@ namespace smt {
               m_fingerprints.display(tout); 
               );
         failure fl = get_last_search_failure();
-        if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS) {
+        if (fl == TIMEOUT || fl == MEMOUT || fl == CANCELED || fl == NUM_CONFLICTS || fl == THEORY) {
             // don't generate model.
             return;
         }

From 0cf1f9c2106ee7110465809f0fd000946c9d0e9a Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 14 Aug 2014 12:15:58 +0100
Subject: [PATCH 02/14] .NET API context refcounting; changed int to long to be
 on the safe side on 64-bit platforms.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/api/dotnet/Context.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 5436fe0a0..2b88cbab7 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3646,7 +3646,7 @@ namespace Microsoft.Z3
         internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
 
 
-        internal int refCount = 0;
+        internal long refCount = 0;
 
         /// <summary>
         /// Finalizer.

From 37ed4b04d078d6d1e35db2799d769e8d4b87f775 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Thu, 14 Aug 2014 12:18:00 +0100
Subject: [PATCH 03/14] Bugfix: param_refs didn't make it through to
 smt::solver (smt_params) in some cases.

Thanks to user xor88 for pointing us in the right direction!

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/api/api_solver.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index ac30a0c21..c8b1723f1 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -40,6 +40,7 @@ extern "C" {
         params_ref p = s->m_params;
         mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled);
         s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
+        s->m_solver->updt_params(p);
     }
 
     static void init_solver(Z3_context c, Z3_solver s) {

From 60054ce469c3e2bc8c34e7b9285c8450e4232812 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 17 Aug 2014 21:20:56 -0700
Subject: [PATCH 04/14] fix cache bug in PDR reported by Phillip Ruemmer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/pdr/pdr_context.cpp | 38 +++++++++++++++++++++++++------------
 src/muz/pdr/pdr_context.h   | 13 ++++++++-----
 2 files changed, 34 insertions(+), 17 deletions(-)

diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index b09280d35..94dd5d0a0 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -736,6 +736,11 @@ namespace pdr {
         m_closed = true; 
     }
 
+    void model_node::reopen() {
+        SASSERT(m_closed);
+        m_closed = false;
+    }
+
     static bool is_ini(datalog::rule const& r) {
         return r.get_uninterpreted_tail_size() == 0;
     }
@@ -745,6 +750,7 @@ namespace pdr {
             return const_cast<datalog::rule*>(m_rule);
         }
         // only initial states are not set by the PDR search.
+        SASSERT(m_model.get());
         datalog::rule const& rl1 = pt().find_rule(*m_model);
         if (is_ini(rl1)) {
             set_rule(&rl1);
@@ -864,9 +870,10 @@ namespace pdr {
     }
 
     void model_search::add_leaf(model_node& n) {
-        unsigned& count = cache(n).insert_if_not_there2(n.state(), 0)->get_data().m_value;
-        ++count;
-        if (count == 1 || is_repeated(n)) {
+        model_nodes ns;
+        model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value;
+        nodes.push_back(&n);
+        if (nodes.size() == 1 || is_repeated(n)) {
             set_leaf(n);
         }
         else {
@@ -875,7 +882,7 @@ namespace pdr {
     }
 
     void model_search::set_leaf(model_node& n) {
-        erase_children(n);
+        erase_children(n, true);
         SASSERT(n.is_open());      
         enqueue_leaf(n);
     }
@@ -897,7 +904,7 @@ namespace pdr {
         set_leaf(*root);
     }
 
-    obj_map<expr, unsigned>& model_search::cache(model_node const& n) {
+    obj_map<expr, ptr_vector<model_node> >& model_search::cache(model_node const& n) {
         unsigned l = n.orig_level();
         if (l >= m_cache.size()) {
             m_cache.resize(l + 1);
@@ -905,7 +912,7 @@ namespace pdr {
         return m_cache[l];
     }
 
-    void model_search::erase_children(model_node& n) {
+    void model_search::erase_children(model_node& n, bool backtrack) {
         ptr_vector<model_node> todo, nodes;
         todo.append(n.children());
         erase_leaf(n);
@@ -916,13 +923,20 @@ namespace pdr {
             nodes.push_back(m);
             todo.append(m->children());
             erase_leaf(*m);
-            remove_node(*m);
+            remove_node(*m, backtrack);
         }
         std::for_each(nodes.begin(), nodes.end(), delete_proc<model_node>());
     }
 
-    void model_search::remove_node(model_node& n) {
-        if (0 == --cache(n).find(n.state())) {
+    void model_search::remove_node(model_node& n, bool backtrack) {
+        model_nodes& nodes = cache(n).find(n.state());
+        nodes.erase(&n);
+        if (nodes.size() > 0 && n.is_open() && backtrack) {
+            for (unsigned i = 0; i < nodes.size(); ++i) {
+                nodes[i]->reopen();
+            }
+        }
+        if (nodes.empty()) {            
             cache(n).remove(n.state());
         }
     }
@@ -1203,8 +1217,8 @@ namespace pdr {
 
     void model_search::reset() {
         if (m_root) {
-            erase_children(*m_root);
-            remove_node(*m_root);
+            erase_children(*m_root, false);
+            remove_node(*m_root, false);
             dealloc(m_root);
             m_root = 0;
         }
@@ -1240,7 +1254,7 @@ namespace pdr {
           m_pm(m_fparams, params.max_num_contexts(), m),
           m_query_pred(m),
           m_query(0),
-          m_search(m_params.bfs_model_search()),
+          m_search(m_params.bfs_model_search(), m),
           m_last_result(l_undef),
           m_inductive_lvl(0),
           m_expanded_lvl(0),
diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h
index 8a4f3e438..a85011600 100644
--- a/src/muz/pdr/pdr_context.h
+++ b/src/muz/pdr/pdr_context.h
@@ -231,6 +231,7 @@ namespace pdr {
         }
 
         void set_closed();     
+        void reopen();
         void set_pre_closed() { m_closed = true; }
         void reset() { m_children.reset(); }
 
@@ -243,19 +244,21 @@ namespace pdr {
     };
 
     class model_search {
+        typedef ptr_vector<model_node> model_nodes;
+        ast_manager&       m;
         bool               m_bfs;
         model_node*        m_root;
         std::deque<model_node*> m_leaves;
-        vector<obj_map<expr, unsigned> > m_cache;
+        vector<obj_map<expr, model_nodes > > m_cache;
         
-        obj_map<expr, unsigned>& cache(model_node const& n);
-        void erase_children(model_node& n);
+        obj_map<expr, model_nodes>& cache(model_node const& n);
+        void erase_children(model_node& n, bool backtrack);
         void erase_leaf(model_node& n);
-        void remove_node(model_node& n);
+        void remove_node(model_node& n, bool backtrack);
         void enqueue_leaf(model_node& n); // add leaf to priority queue.
         void update_models();
     public:
-        model_search(bool bfs): m_bfs(bfs), m_root(0) {}
+        model_search(bool bfs, ast_manager& m): m(m), m_bfs(bfs), m_root(0) {}
         ~model_search();
 
         void reset();

From 70a1155d711e38895174ada51d6568ae3af3b7ce Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Mon, 18 Aug 2014 17:13:16 -0700
Subject: [PATCH 05/14] fixed duality bug and added some code for returning
 bounded status (not yet used)

---
 src/duality/duality.h                    |  7 +++
 src/duality/duality_solver.cpp           | 24 +++++++++++
 src/muz/base/dl_context.h                |  3 ++
 src/muz/duality/duality_dl_interface.cpp | 55 +++++++++++++++++++++++-
 src/muz/fp/dl_cmds.cpp                   |  5 +++
 5 files changed, 93 insertions(+), 1 deletion(-)

diff --git a/src/duality/duality.h b/src/duality/duality.h
index c315c5431..c1c9797f3 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -1152,6 +1152,13 @@ protected:
 
       virtual void LearnFrom(Solver *old_solver) = 0;
 
+      /** Return true if the solution be incorrect due to recursion bounding.
+	  That is, the returned "solution" might contain all derivable facts up to the
+	  given recursion bound, but not be actually a fixed point.
+       */
+
+      virtual bool IsResultRecursionBounded() = 0;
+
       virtual ~Solver(){}
 
       static Solver *Create(const std::string &solver_class, RPFP *rpfp);
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index 59611c814..681582415 100755
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -768,6 +768,29 @@ namespace Duality {
       annot.Simplify();
     }    
 
+    bool recursionBounded;
+
+    /** See if the solution might be bounded. */
+    void TestRecursionBounded(){
+      recursionBounded = false;
+      if(RecursionBound == -1)
+	return;
+      for(unsigned i = 0; i < nodes.size(); i++){
+	Node *node = nodes[i];
+	std::vector<Node *> &insts = insts_of_node[node];
+	for(unsigned j = 0; j < insts.size(); j++)
+	  if(indset->Contains(insts[j]))
+	    if(NodePastRecursionBound(insts[j])){
+	      recursionBounded = true;
+	      return;
+	    }
+      }
+    }    
+
+    bool IsResultRecursionBounded(){
+      return recursionBounded;
+    }
+
     /** Generate a proposed solution of the input RPFP from
 	the unwinding, by unioning the instances of each node. */
     void GenSolutionFromIndSet(bool with_markers = false){
@@ -1026,6 +1049,7 @@ namespace Duality {
 	timer_stop("ProduceCandidatesForExtension");
 	if(candidates.empty()){
 	  GenSolutionFromIndSet();
+	  TestRecursionBounded();
 	  return true;
 	}
 	Candidate cand = candidates.front();
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 1952cc42f..7349fa889 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -53,6 +53,7 @@ namespace datalog {
         MEMOUT,
         INPUT_ERROR,
         APPROX,
+	BOUNDED,
         CANCELED
     };
 
@@ -304,6 +305,8 @@ namespace datalog {
            \brief Retrieve predicates
         */
         func_decl_set const& get_predicates() const { return m_preds; }
+	ast_ref_vector const &get_pinned() const {return m_pinned; }
+
         bool is_predicate(func_decl* pred) const { return m_preds.contains(pred); }
         bool is_predicate(expr * e) const { return is_app(e) && is_predicate(to_app(e)->get_decl()); }
 
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 0584e6b58..849cf94ea 100755
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -36,6 +36,7 @@ Revision History:
 #include "model_v2_pp.h"
 #include "fixedpoint_params.hpp"
 #include "used_vars.h"
+#include "func_decl_dependencies.h"
 
 // template class symbol_table<family_id>;
 
@@ -207,6 +208,46 @@ lbool dl_interface::query(::expr * query) {
     _d->rpfp->AssertAxiom(e);
   }
   
+  // make sure each predicate is the head of at least one clause
+  func_decl_set heads;
+  for(unsigned i = 0; i < clauses.size(); i++){
+    expr cl = clauses[i];
+
+    while(true){
+      if(cl.is_app()){
+	decl_kind k = cl.decl().get_decl_kind();
+	if(k == Implies)
+	  cl = cl.arg(1);
+	else {
+	  heads.insert(cl.decl());
+	  break;
+	}
+      }
+      else if(cl.is_quantifier())
+	cl = cl.body();
+      else break;
+    }
+  }
+  ast_ref_vector const &pinned = m_ctx.get_pinned();
+  for(unsigned i = 0; i < pinned.size(); i++){
+    ::ast *fa = pinned[i];
+    if(is_func_decl(fa)){
+      ::func_decl *fd = to_func_decl(fa);
+      if(m_ctx.is_predicate(fd)) {
+	func_decl f(_d->ctx,fd);
+	if(!heads.contains(fd)){
+	  int arity = f.arity();
+	  std::vector<expr> args;
+	  for(int j = 0; j < arity; j++)
+	    args.push_back(_d->ctx.fresh_func_decl("X",f.domain(j))());
+	  expr c = implies(_d->ctx.bool_val(false),f(args));
+	  c = _d->ctx.make_quant(Forall,args,c);
+	  clauses.push_back(c);
+	}
+      }
+    }
+  }
+
   // creates 1-1 map between clauses and rpfp edges
   _d->rpfp->FromClauses(clauses);
 
@@ -265,7 +306,19 @@ lbool dl_interface::query(::expr * query) {
   // dealloc(rs); this is now owned by data
 
   // true means the RPFP problem is SAT, so the query is UNSAT
-  return ans ? l_false : l_true;
+  // but we return undef if the UNSAT result is bounded
+  if(ans){
+    if(rs->IsResultRecursionBounded()){
+#if 0
+      m_ctx.set_status(datalog::BOUNDED);
+      return l_undef;
+#else
+      return l_false;
+#endif
+    }
+    return l_false;
+  }
+  return l_true;
 }
 
 expr_ref dl_interface::get_cover_delta(int level, ::func_decl* pred_orig) {
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index 827b90e60..f9916808c 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -252,6 +252,11 @@ public:
             print_certificate(ctx);
             break;
         case l_undef: 
+	    if(dlctx.get_status() == datalog::BOUNDED){
+	      ctx.regular_stream() << "bounded\n";
+	      print_certificate(ctx);
+	      break;
+	    }
             ctx.regular_stream() << "unknown\n";
             switch(dlctx.get_status()) {
             case datalog::INPUT_ERROR:

From 38ee8cb807a5afd9c5b9961d3e7b6213dbbb679f Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 22 Aug 2014 12:57:33 +0100
Subject: [PATCH 06/14] .NET API: bugfix. Thanks to Konrad Jamrozik for
 catching this one.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 scripts/update_api.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/update_api.py b/scripts/update_api.py
index f88e0393f..97dacb44b 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -420,7 +420,7 @@ def mk_dotnet():
 
 
 NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
-Unwrapped = [ 'Z3_del_context' ]
+Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
 
 def mk_dotnet_wrappers():
     global Type2Str

From 51aa10821ea54b8c221f6952da146c362edea862 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Tue, 26 Aug 2014 13:46:53 -0700
Subject: [PATCH 07/14] fixed pop issue and interpolation proof mode issue

---
 src/cmd_context/interpolant_cmds.cpp | 3 ++-
 src/solver/solver_na2as.cpp          | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp
index 7fd44c088..cb83b52f6 100644
--- a/src/cmd_context/interpolant_cmds.cpp
+++ b/src/cmd_context/interpolant_cmds.cpp
@@ -33,6 +33,7 @@ Notes:
 #include"iz3checker.h"
 #include"iz3profiling.h"
 #include"interp_params.hpp"
+#include"scoped_proof.h"
 
 static void show_interpolant_and_maybe_check(cmd_context & ctx,
 					     ptr_vector<ast> &cnsts,
@@ -153,7 +154,7 @@ static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, par
   ast_manager &_m = ctx.m();
   // TODO: the following is a HACK to enable proofs in the old smt solver
   // When we stop using that solver, this hack can be removed
-  _m.toggle_proof_mode(PGM_FINE);  
+  scoped_proof_mode spm(_m,PGM_FINE);
   ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
   p.set_bool("proof", true);
   scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());
diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp
index 9889b5872..01c45ee44 100644
--- a/src/solver/solver_na2as.cpp
+++ b/src/solver/solver_na2as.cpp
@@ -82,7 +82,7 @@ void solver_na2as::pop(unsigned n) {
 }
 
 void solver_na2as::restore_assumptions(unsigned old_sz) {
-    SASSERT(old_sz == 0);
+  //    SASSERT(old_sz == 0);
     for (unsigned i = old_sz; i < m_assumptions.size(); i++) {
         m_manager.dec_ref(m_assumptions[i]);
     }

From 8ea7109f8fcca01f57e42c625b4c63ecac801bb4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 28 Aug 2014 10:18:42 -0700
Subject: [PATCH 08/14] update documentation to clarify reference counting
 policies

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

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index b9f4975e8..4ffdfa9c2 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1375,6 +1375,16 @@ extern "C" {
        although some parameters can be changed using #Z3_update_param_value.
        All main interaction with Z3 happens in the context of a \c Z3_context.
 
+       In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects
+       are determined by the scope level of #Z3_push and #Z3_pop.
+       In other words, a Z3_ast object remains valid until there is a 
+       call to Z3_pop that takes the current scope below the level where 
+       the object was created.
+
+       Note that all other reference counted objects, including Z3_model,
+       Z3_solver, Z3_func_interp have to be managed by the caller. 
+       Their reference counts are not handled by the context.       
+
        \conly \sa Z3_del_context
 
        \conly \deprecated Use #Z3_mk_context_rc

From fa24d9db6fc8598b337795b4d2833c57b242f168 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 1 Sep 2014 17:27:07 +0100
Subject: [PATCH 09/14] Added multi processor compilation to VS project.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 scripts/mk_util.py | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 035cdd3c4..5e100b527 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2522,7 +2522,11 @@ def mk_vs_proj(name, components):
     f.write('    <ClCompile>\n')
     f.write('      <Optimization>Disabled</Optimization>\n')
     f.write('      <PreprocessorDefinitions>WIN32;_DEBUG;Z3DEBUG;_TRACE;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
-    f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
+    if VS_PAR:
+        f.write('      <MinimalRebuild>false</MinimalRebuild>\n')
+        f.write('      <MultiProcessorCompilation>true</MultiProcessorCompilation>\n')
+    else:
+        f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
     f.write('      <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n')
     f.write('      <WarningLevel>Level3</WarningLevel>\n')
     f.write('      <RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>\n')
@@ -2556,7 +2560,11 @@ def mk_vs_proj(name, components):
     f.write('    <ClCompile>\n')
     f.write('      <Optimization>Disabled</Optimization>\n')
     f.write('      <PreprocessorDefinitions>WIN32;_NDEBUG;_MP_INTERNAL;_WINDOWS;%(PreprocessorDefinitions)</PreprocessorDefinitions>\n')
-    f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
+    if VS_PAR:
+        f.write('      <MinimalRebuild>false</MinimalRebuild>\n')
+        f.write('      <MultiProcessorCompilation>true</MultiProcessorCompilation>\n')
+    else:
+        f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
     f.write('      <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n')
     f.write('      <WarningLevel>Level3</WarningLevel>\n')
     f.write('      <RuntimeLibrary>MultiThreadedDLL</RuntimeLibrary>\n')

From 23af977d68ee85a3a1b88d1e59c26bf33f5189df Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 3 Sep 2014 17:49:10 +0100
Subject: [PATCH 10/14] Multi-threading bugfix, DLL could be used from other
 threads before the main thread initializes it. Thanks to user xor88 for
 reporting this one.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 src/util/memory_manager.cpp | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 3f2e224d9..45088d5d4 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -35,6 +35,7 @@ static long long  g_memory_max_used_size     = 0;
 static long long  g_memory_watermark         = 0;
 static bool       g_exit_when_out_of_memory  = false;
 static char const * g_out_of_memory_msg      = "ERROR: out of memory";
+static volatile bool g_memory_fully_initialized = false;
 
 void memory::exit_when_out_of_memory(bool flag, char const * msg) {
     g_exit_when_out_of_memory = flag;
@@ -83,10 +84,18 @@ void memory::initialize(size_t max_size) {
             initialize = true;
         }
     }
-    if (!initialize)
-        return;
-    g_memory_out_of_memory  = false;
-    mem_initialize();
+    if (initialize) {
+        g_memory_out_of_memory = false;
+        mem_initialize();
+        g_memory_fully_initialized = true;
+    }
+    else {        
+        // Delay the current thread until the DLL is fully initialized
+        // Without this, multiple threads can start to call API functions
+        // before memory::initialize(...) finishes.
+        while (!g_memory_fully_initialized)
+            /* wait */ ;
+    }
 }
 
 bool memory::is_out_of_memory() {
@@ -98,9 +107,9 @@ bool memory::is_out_of_memory() {
     return r;
 }
 
-void memory::set_high_watermark(size_t watermak) {
+void memory::set_high_watermark(size_t watermark) {
     // This method is only safe to invoke at initialization time, that is, before the threads are created.
-    g_memory_watermark = watermak;
+    g_memory_watermark = watermark;
 }
 
 bool memory::above_high_watermark() {

From 3d9120c74503171c00838f64fe73bb91c3aba821 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 4 Sep 2014 14:49:58 -0700
Subject: [PATCH 11/14] lifetime of expressions from model follow life-time of
 model, not the push/pop scope making scope based reference counting error
 prone

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_model.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index f17f7a586..f0c31d800 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -60,6 +60,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
+        mk_c(c)->save_ast_trail(r);
         RETURN_Z3(of_expr(r));
         Z3_CATCH_RETURN(0);
     }
@@ -263,6 +264,7 @@ extern "C" {
         RESET_ERROR_CODE();
         CHECK_NON_NULL(f, 0);
         expr * e = to_func_interp_ref(f)->get_else();
+        mk_c(c)->save_ast_trail(e);
         RETURN_Z3(of_expr(e));
         Z3_CATCH_RETURN(0);
     }
@@ -301,6 +303,7 @@ extern "C" {
         LOG_Z3_func_entry_get_value(c, e);
         RESET_ERROR_CODE();
         expr * v = to_func_entry_ref(e)->get_result();
+        mk_c(c)->save_ast_trail(v);
         RETURN_Z3(of_expr(v));
         Z3_CATCH_RETURN(0);
     }

From 904ab4bf9e1cf9f147218b88bbfd8ecc8b1a8a0e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 5 Sep 2014 11:18:34 -0700
Subject: [PATCH 12/14] address race condition in cleanup methods

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp              | 10 +++++++--
 src/solver/combined_solver.cpp               | 10 +++++++--
 src/solver/solver.h                          |  4 +++-
 src/solver/tactic2solver.cpp                 |  8 +++++--
 src/tactic/aig/aig.h                         |  2 --
 src/tactic/arith/add_bounds_tactic.cpp       | 10 ++-------
 src/tactic/arith/degree_shift_tactic.cpp     | 10 ++-------
 src/tactic/arith/diff_neq_tactic.cpp         | 13 +++--------
 src/tactic/arith/factor_tactic.cpp           | 10 ++-------
 src/tactic/arith/fix_dl_var_tactic.cpp       | 10 ++-------
 src/tactic/arith/fm_tactic.cpp               | 10 ++-------
 src/tactic/arith/lia2pb_tactic.cpp           | 10 ++-------
 src/tactic/arith/normalize_bounds_tactic.cpp |  9 ++------
 src/tactic/arith/pb2bv_tactic.cpp            |  9 ++------
 src/tactic/arith/propagate_ineqs_tactic.cpp  | 10 ++-------
 src/tactic/arith/recover_01_tactic.cpp       | 10 ++-------
 src/tactic/bv/bit_blaster_tactic.cpp         | 10 ++-------
 src/tactic/bv/bv1_blaster_tactic.cpp         | 10 ++-------
 src/tactic/bv/bv_size_reduction_tactic.cpp   | 10 ++-------
 src/tactic/bv/max_bv_sharing_tactic.cpp      | 10 ++-------
 src/tactic/core/cofactor_elim_term_ite.cpp   | 23 +++++++-------------
 src/tactic/core/cofactor_elim_term_ite.h     |  3 ++-
 src/tactic/core/ctx_simplify_tactic.cpp      |  9 ++------
 src/tactic/core/der_tactic.cpp               |  9 ++------
 src/tactic/core/elim_term_ite_tactic.cpp     |  9 ++------
 src/tactic/core/elim_uncnstr_tactic.cpp      | 11 +++-------
 src/tactic/core/occf_tactic.cpp              | 10 ++-------
 src/tactic/core/propagate_values_tactic.cpp  |  9 ++------
 src/tactic/core/reduce_args_tactic.cpp       | 11 +++-------
 src/tactic/core/simplify_tactic.cpp          |  9 ++------
 src/tactic/core/simplify_tactic.h            |  4 +++-
 src/tactic/core/solve_eqs_tactic.cpp         | 12 ++++------
 src/tactic/core/tseitin_cnf_tactic.cpp       | 12 +++-------
 src/tactic/fpa/fpa2bv_tactic.cpp             | 12 +++-------
 src/tactic/tactic.h                          |  8 ++++++-
 src/tactic/tactical.cpp                      | 16 +++++---------
 src/tactic/ufbv/macro_finder_tactic.cpp      |  9 ++------
 src/tactic/ufbv/quasi_macros_tactic.cpp      |  9 ++------
 src/tactic/ufbv/ufbv_rewriter_tactic.cpp     |  9 ++------
 39 files changed, 115 insertions(+), 264 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 20539266b..ce2838aba 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -346,8 +346,14 @@ cmd_context::~cmd_context() {
 }
 
 void cmd_context::set_cancel(bool f) {
-    if (m_solver)
-        m_solver->set_cancel(f);
+    if (m_solver) {
+        if (f) {
+            m_solver->cancel(); 
+        }
+        else {
+            m_solver->reset_cancel();
+        }
+    }
     if (has_manager())
         m().set_cancel(f);
 }
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index a98e5be49..dfbb62f65 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -218,8 +218,14 @@ public:
     }
 
     virtual void set_cancel(bool f) {
-        m_solver1->set_cancel(f);
-        m_solver2->set_cancel(f);
+        if (f) {
+            m_solver1->cancel();
+            m_solver2->cancel();
+        }
+        else {
+            m_solver1->reset_cancel();
+            m_solver2->reset_cancel();
+        }
     }
     
     virtual void set_progress_callback(progress_callback * callback) {
diff --git a/src/solver/solver.h b/src/solver/solver.h
index e047bace1..a95c649c0 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -99,7 +99,6 @@ public:
     */
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
 
-    virtual void set_cancel(bool f) {}
     /**
        \brief Interrupt this solver.
     */
@@ -130,6 +129,9 @@ public:
        \brief Display the content of this solver.
     */
     virtual void display(std::ostream & out) const;
+protected:
+    virtual void set_cancel(bool f) = 0;
+
 };
 
 #endif
diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp
index 1268fbcea..fb4898ecd 100644
--- a/src/solver/tactic2solver.cpp
+++ b/src/solver/tactic2solver.cpp
@@ -173,8 +173,12 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
 }
 
 void tactic2solver::set_cancel(bool f) {
-    if (m_tactic.get())
-        m_tactic->set_cancel(f);
+    if (m_tactic.get()) {
+        if (f) 
+            m_tactic->cancel();
+        else
+            m_tactic->reset_cancel();
+    }
 }
 
 void tactic2solver::collect_statistics(statistics & st) const {
diff --git a/src/tactic/aig/aig.h b/src/tactic/aig/aig.h
index c8befd9b2..291bfbcf3 100644
--- a/src/tactic/aig/aig.h
+++ b/src/tactic/aig/aig.h
@@ -73,8 +73,6 @@ public:
     void display(std::ostream & out, aig_ref const & r) const;
     void display_smt2(std::ostream & out, aig_ref const & r) const;
     unsigned get_num_aigs() const;
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
     void set_cancel(bool f);
 };
 
diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp
index d396359a3..9bf967be3 100644
--- a/src/tactic/arith/add_bounds_tactic.cpp
+++ b/src/tactic/arith/add_bounds_tactic.cpp
@@ -172,18 +172,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp
index a1aa0bdc8..e8fb72be4 100644
--- a/src/tactic/arith/degree_shift_tactic.cpp
+++ b/src/tactic/arith/degree_shift_tactic.cpp
@@ -319,18 +319,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
 protected:
diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp
index b534c8295..1a33bf4f2 100644
--- a/src/tactic/arith/diff_neq_tactic.cpp
+++ b/src/tactic/arith/diff_neq_tactic.cpp
@@ -398,20 +398,13 @@ public:
     }
     
     virtual void cleanup() {
-        unsigned num_conflicts = m_imp->m_num_conflicts;
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
+        d->m_num_conflicts = m_imp->m_num_conflicts;
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_conflicts = num_conflicts;
     }
 
 protected:
diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp
index 4eec83037..dc17a4f87 100644
--- a/src/tactic/arith/factor_tactic.cpp
+++ b/src/tactic/arith/factor_tactic.cpp
@@ -333,18 +333,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp
index d2e3ebf1f..693066ee1 100644
--- a/src/tactic/arith/fix_dl_var_tactic.cpp
+++ b/src/tactic/arith/fix_dl_var_tactic.cpp
@@ -338,18 +338,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index c4b7cbaf3..c180029ae 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -1682,18 +1682,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
     virtual void operator()(goal_ref const & in, 
diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp
index 9ee8f6728..33d5f138e 100644
--- a/src/tactic/arith/lia2pb_tactic.cpp
+++ b/src/tactic/arith/lia2pb_tactic.cpp
@@ -345,18 +345,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp
index a62b311b5..323903f6c 100644
--- a/src/tactic/arith/normalize_bounds_tactic.cpp
+++ b/src/tactic/arith/normalize_bounds_tactic.cpp
@@ -191,17 +191,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index 89195a9d5..643195b05 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -1002,17 +1002,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp
index 12954005f..d7e4f30d2 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.cpp
+++ b/src/tactic/arith/propagate_ineqs_tactic.cpp
@@ -548,16 +548,10 @@ void propagate_ineqs_tactic::set_cancel(bool f) {
 }
  
 void propagate_ineqs_tactic::cleanup() {
-    ast_manager & m = m_imp->m;
-    imp * d = m_imp;
+    imp * d = alloc(imp, m_imp->m, m_params);
     #pragma omp critical (tactic_cancel)
     {
-        d = m_imp;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel) 
-    {
-        m_imp = d;
-    }
 }
diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp
index 3b1a86345..3d222cf56 100644
--- a/src/tactic/arith/recover_01_tactic.cpp
+++ b/src/tactic/arith/recover_01_tactic.cpp
@@ -425,18 +425,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp
index 0330141cb..33423c8b1 100644
--- a/src/tactic/bv/bit_blaster_tactic.cpp
+++ b/src/tactic/bv/bit_blaster_tactic.cpp
@@ -140,18 +140,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m(), m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
     unsigned get_num_steps() const {
diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp
index 8dcaf2112..5f20015ca 100644
--- a/src/tactic/bv/bv1_blaster_tactic.cpp
+++ b/src/tactic/bv/bv1_blaster_tactic.cpp
@@ -465,18 +465,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m(), m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
     
     unsigned get_num_steps() const {
diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index d3fdb6e56..e149afc75 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -392,17 +392,11 @@ void bv_size_reduction_tactic::set_cancel(bool f) {
 }
  
 void bv_size_reduction_tactic::cleanup() {
-    ast_manager & m = m_imp->m;
-    imp * d = m_imp;
+    imp * d = alloc(imp, m_imp->m);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp
index f60487d60..56b18dd8d 100644
--- a/src/tactic/bv/max_bv_sharing_tactic.cpp
+++ b/src/tactic/bv/max_bv_sharing_tactic.cpp
@@ -311,18 +311,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m(), m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp
index 1f560ef62..aca6d9084 100644
--- a/src/tactic/core/cofactor_elim_term_ite.cpp
+++ b/src/tactic/core/cofactor_elim_term_ite.cpp
@@ -683,12 +683,7 @@ cofactor_elim_term_ite::cofactor_elim_term_ite(ast_manager & m, params_ref const
 }
 
 cofactor_elim_term_ite::~cofactor_elim_term_ite() {
-    imp * d = m_imp;
-    #pragma omp critical (cofactor_elim_term_ite)
-    {
-        m_imp = 0;
-    }
-    dealloc(d);
+    dealloc(m_imp);
 }
 
 void cofactor_elim_term_ite::updt_params(params_ref const & p) {
@@ -704,19 +699,17 @@ void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {
 }
     
 void cofactor_elim_term_ite::set_cancel(bool f) {
-    #pragma omp critical (cofactor_elim_term_ite)
-    {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
+    if (m_imp)
+        m_imp->set_cancel(f);
 }
 
 void cofactor_elim_term_ite::cleanup() {
-    ast_manager & m = m_imp->m;
-    #pragma omp critical (cofactor_elim_term_ite) 
+    ast_manager & m = m_imp->m;    
+    imp * d = alloc(imp, m, m_params);
+    #pragma omp critical (tactic_cancel)
     {
-        dealloc(m_imp);
-        m_imp = alloc(imp, m, m_params);
+        std::swap(d, m_imp);
     }
+    dealloc(d);
 }
 
diff --git a/src/tactic/core/cofactor_elim_term_ite.h b/src/tactic/core/cofactor_elim_term_ite.h
index ce2f31ea0..e734fcad6 100644
--- a/src/tactic/core/cofactor_elim_term_ite.h
+++ b/src/tactic/core/cofactor_elim_term_ite.h
@@ -37,8 +37,9 @@ public:
     
     void cancel() { set_cancel(true); }
     void reset_cancel() { set_cancel(false); }
-    void set_cancel(bool f);
     void cleanup();
+    void set_cancel(bool f);
+
 };
 
 #endif
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 71f4771a9..bb38d28ce 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -548,16 +548,11 @@ void ctx_simplify_tactic::set_cancel(bool f) {
 
 void ctx_simplify_tactic::cleanup() {
     ast_manager & m   = m_imp->m;
-    imp * d = m_imp;
+    imp * d = alloc(imp, m, m_params);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp
index c2245b409..2277c3fa8 100644
--- a/src/tactic/core/der_tactic.cpp
+++ b/src/tactic/core/der_tactic.cpp
@@ -90,17 +90,12 @@ public:
 
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp
index 456bad5e0..e49884004 100644
--- a/src/tactic/core/elim_term_ite_tactic.cpp
+++ b/src/tactic/core/elim_term_ite_tactic.cpp
@@ -174,17 +174,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 4d64bf061..6d7bcb2f2 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -1036,18 +1036,13 @@ public:
     
     virtual void cleanup() {
         unsigned num_elim_apps = get_num_elim_apps();
-        ast_manager & m = m_imp->m_manager;
-        imp * d = m_imp;
+        ast_manager & m = m_imp->m_manager;        
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
         m_imp->m_num_elim_apps = num_elim_apps;
     }
 
diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp
index f8f6174b9..9b974ae19 100644
--- a/src/tactic/core/occf_tactic.cpp
+++ b/src/tactic/core/occf_tactic.cpp
@@ -225,18 +225,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m_imp->m);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
 protected:
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 1e358177f..5873efd61 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -255,17 +255,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
 protected:
diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp
index 59ed2dcd3..99375e6e8 100644
--- a/src/tactic/core/reduce_args_tactic.cpp
+++ b/src/tactic/core/reduce_args_tactic.cpp
@@ -541,17 +541,12 @@ void reduce_args_tactic::set_cancel(bool f) {
 }
 
 void reduce_args_tactic::cleanup() {
-    ast_manager & m   = m_imp->m();
-    imp * d = m_imp;
+    ast_manager & m   = m_imp->m();    
+    imp * d = alloc(imp, m);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp
index 95db962a7..39f10e10c 100644
--- a/src/tactic/core/simplify_tactic.cpp
+++ b/src/tactic/core/simplify_tactic.cpp
@@ -115,17 +115,12 @@ void simplify_tactic::set_cancel(bool f) {
 
 void simplify_tactic::cleanup() {
     ast_manager & m = m_imp->m();
-    imp * d = m_imp;
+    imp * d = alloc(imp, m, m_params);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
 unsigned simplify_tactic::get_num_steps() const {
diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h
index fc9cb393c..1ba5a6da8 100644
--- a/src/tactic/core/simplify_tactic.h
+++ b/src/tactic/core/simplify_tactic.h
@@ -43,9 +43,11 @@ public:
     virtual void cleanup();
 
     unsigned get_num_steps() const;
-    virtual void set_cancel(bool f);
 
     virtual tactic * translate(ast_manager & m) { return alloc(simplify_tactic, m, m_params); }
+protected:
+    virtual void set_cancel(bool f);
+
 };
 
 tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 995940406..3b0a57d20 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -749,23 +749,19 @@ public:
     virtual void cleanup() {
         unsigned num_elim_vars = m_imp->m_num_eliminated_vars;
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
         expr_replacer * r = m_imp->m_r;
         if (r)
             r->set_substitution(0);
         bool owner = m_imp->m_r_owner;
         m_imp->m_r_owner  = false; // stole replacer
+
+        imp * d = alloc(imp, m, m_params, r, owner);
+        d->m_num_eliminated_vars = num_elim_vars;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params, r, owner);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_eliminated_vars = num_elim_vars;
     }
 
     virtual void collect_statistics(statistics & st) const {
diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp
index b6c4b0655..c5be7ab1f 100644
--- a/src/tactic/core/tseitin_cnf_tactic.cpp
+++ b/src/tactic/core/tseitin_cnf_tactic.cpp
@@ -898,20 +898,14 @@ public:
     }
     
     virtual void cleanup() {
-        unsigned num_aux_vars = m_imp->m_num_aux_vars;
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
+        d->m_num_aux_vars = m_imp->m_num_aux_vars;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_aux_vars = num_aux_vars;
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index 3a6b7ea45..4a3a01b6f 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -138,19 +138,13 @@ public:
         (*m_imp)(in, result, mc, pc, core);
     }
     
-    virtual void cleanup() {
-        ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+    virtual void cleanup() {        
+        imp * d = alloc(imp, m_imp->m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
 protected:
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index 80de1bcd0..8b4f9f576 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -47,7 +47,6 @@ public:
 
     void cancel();
     void reset_cancel();
-    virtual void set_cancel(bool f) {}
     
     /**
        \brief Apply tactic to goal \c in.
@@ -96,6 +95,13 @@ public:
 
     // translate tactic to the given manager
     virtual tactic * translate(ast_manager & m) = 0;
+private:
+    friend class nary_tactical;
+    friend class binary_tactical;
+    friend class unary_tactical;
+
+    virtual void set_cancel(bool f) {}
+
 };
 
 typedef ref<tactic>         tactic_ref;
diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp
index ca66b7a14..1e0b07e9d 100644
--- a/src/tactic/tactical.cpp
+++ b/src/tactic/tactical.cpp
@@ -102,11 +102,8 @@ protected:
        \brief Reset cancel flag of t if this was not canceled.
     */
     void parent_reset_cancel(tactic & t) {
-        #pragma omp critical (tactic_cancel)
-        {
-            if (!m_cancel) {
-                t.set_cancel(false);
-            }
+        if (!m_cancel) {
+            t.reset_cancel();
         }
     }
 
@@ -393,11 +390,8 @@ protected:
        \brief Reset cancel flag of st if this was not canceled.
     */
     void parent_reset_cancel(tactic & t) {
-        #pragma omp critical (tactic_cancel)
-        {
-            if (!m_cancel) {
-                t.set_cancel(false);
-            }
+        if (!m_cancel) {
+            t.reset_cancel();
         }
     }
 
@@ -988,7 +982,7 @@ protected:
     virtual void set_cancel(bool f) { 
         m_cancel = f;
         if (m_t) 
-            m_t->set_cancel(f); 
+            m_t->set_cancel(f);
     }
 
     template<typename T>
diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp
index 14a42ec51..2f0262fc8 100644
--- a/src/tactic/ufbv/macro_finder_tactic.cpp
+++ b/src/tactic/ufbv/macro_finder_tactic.cpp
@@ -144,17 +144,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
index 393a40603..cea8f2cfc 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.cpp
+++ b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -151,17 +151,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {
diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
index 0705c627c..efecb38ba 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
@@ -119,17 +119,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {

From 36816e3b2fe1c27c97f88a4aaac8f03eb3243a97 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 6 Sep 2014 19:03:37 -0700
Subject: [PATCH 13/14] clear cache for crash

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/pdr/pdr_context.cpp   | 1 +
 src/tactic/sls/sls_tactic.cpp | 9 ++-------
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 94dd5d0a0..d8b96297a 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -1221,6 +1221,7 @@ namespace pdr {
             remove_node(*m_root, false);
             dealloc(m_root);
             m_root = 0;
+            m_cache.reset();
         }
     }
 
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index ea5d60668..6783d9621 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -557,17 +557,12 @@ public:
     }
 
     virtual void cleanup() {        
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params, m_stats);
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params, m_stats);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
     
     virtual void collect_statistics(statistics & st) const {

From dd62ca5eb36c2a62ee44fc5a79fc27c883de21ae Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 6 Sep 2014 20:54:16 -0700
Subject: [PATCH 14/14] simplify models

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/pdr/pdr_context.cpp | 29 ++++++++++++++++++++++++-----
 1 file changed, 24 insertions(+), 5 deletions(-)

diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index d8b96297a..f07964395 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -47,6 +47,7 @@ Notes:
 #include "dl_boogie_proof.h"
 #include "qe_util.h"
 #include "scoped_proof.h"
+#include "expr_safe_replace.h"
 
 namespace pdr {
 
@@ -1062,10 +1063,7 @@ namespace pdr {
             predicates.pop_back();
             for (unsigned i = rule->get_uninterpreted_tail_size(); i < rule->get_tail_size(); ++i) {
                 subst.apply(2, deltas, expr_offset(rule->get_tail(i), 1), tmp);
-                dctx.get_rewriter()(tmp);
-                if (!m.is_true(tmp)) {
-                    constraints.push_back(tmp);
-                }
+                constraints.push_back(tmp);                
             }
             for (unsigned i = 0; i < constraints.size(); ++i) {
                 max_var = std::max(vc.get_max_var(constraints[i].get()), max_var);
@@ -1088,7 +1086,28 @@ namespace pdr {
 
             children.append(n->children());
         }            
-        return pm.mk_and(constraints);
+
+        expr_safe_replace repl(m);
+        for (unsigned i = 0; i < constraints.size(); ++i) {
+            expr* e = constraints[i].get(), *e1, *e2;
+            if (m.is_eq(e, e1, e2) && is_var(e1) && is_ground(e2)) {
+                repl.insert(e1, e2);
+            }
+            else if (m.is_eq(e, e1, e2) && is_var(e2) && is_ground(e1)) {
+                repl.insert(e2, e1);
+            }
+        }
+        expr_ref_vector result(m);
+        for (unsigned i = 0; i < constraints.size(); ++i) {
+            expr_ref tmp(m);
+            tmp = constraints[i].get();
+            repl(tmp);
+            dctx.get_rewriter()(tmp);
+            if (!m.is_true(tmp)) {
+                result.push_back(tmp);
+            }
+        }        
+        return pm.mk_and(result);
     }
 
     proof_ref model_search::get_proof_trace(context const& ctx) {