Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

scripts/mk_util.py

@@ -2522,6 +2522,10 @@ 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')
+    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')
@@ -2556,6 +2560,10 @@ 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')
+    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')

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

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);
     }

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.

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

src/cmd_context/cmd_context.cpp

@@ -346,8 +346,14 @@ cmd_context::~cmd_context() {
 }
 
 void cmd_context::set_cancel(bool f) {
-    if (m_solver)
+    if (m_solver) {
-        m_solver->set_cancel(f);
+        if (f) {
+            m_solver->cancel(); 
+        }
+        else {
+            m_solver->reset_cancel();
+        }
+    }
     if (has_manager())
         m().set_cancel(f);
 }

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());

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);

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();

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()); }
 

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) {

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:

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 {
 
@@ -736,6 +737,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 +751,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 +871,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;
+        model_nodes ns;
-        ++count;
+        model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value;
-        if (count == 1 || is_repeated(n)) {
+        nodes.push_back(&n);
+        if (nodes.size() == 1 || is_repeated(n)) {
             set_leaf(n);
         }
         else {
@@ -875,7 +883,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 +905,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 +913,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 +924,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) {
+    void model_search::remove_node(model_node& n, bool backtrack) {
-        if (0 == --cache(n).find(n.state())) {
+        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());
         }
     }
@@ -1048,11 +1063,8 @@ 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);                
             }
-            }
             for (unsigned i = 0; i < constraints.size(); ++i) {
                 max_var = std::max(vc.get_max_var(constraints[i].get()), max_var);
             }
@@ -1074,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) {
@@ -1203,10 +1236,11 @@ namespace pdr {
 
     void model_search::reset() {
         if (m_root) {
-            erase_children(*m_root);
+            erase_children(*m_root, false);
-            remove_node(*m_root);
+            remove_node(*m_root, false);
             dealloc(m_root);
             m_root = 0;
+            m_cache.reset();
         }
     }
 
@@ -1240,7 +1274,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),

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);
+        obj_map<expr, model_nodes>& cache(model_node const& n);
-        void erase_children(model_node& 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();

src/solver/combined_solver.cpp

@@ -218,8 +218,14 @@ public:
     }
 
     virtual void set_cancel(bool f) {
-        m_solver1->set_cancel(f);
+        if (f) {
-        m_solver2->set_cancel(f);
+            m_solver1->cancel();
+            m_solver2->cancel();
+        }
+        else {
+            m_solver1->reset_cancel();
+            m_solver2->reset_cancel();
+        }
     }
     
     virtual void set_progress_callback(progress_callback * callback) {

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

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]);
     }

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())
+    if (m_tactic.get()) {
-        m_tactic->set_cancel(f);
+        if (f) 
+            m_tactic->cancel();
+        else
+            m_tactic->reset_cancel();
+    }
 }
 
 void tactic2solver::collect_statistics(statistics & st) const {

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);
 };
 

src/tactic/arith/add_bounds_tactic.cpp

@@ -172,18 +172,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        imp * d = m_imp;
         #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:

src/tactic/arith/degree_shift_tactic.cpp

@@ -319,18 +319,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m);
-        imp * d = m_imp;
         #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:

src/tactic/arith/diff_neq_tactic.cpp

@@ -398,20 +398,13 @@ public:
     }
     
     virtual void cleanup() {
-        unsigned num_conflicts = m_imp->m_num_conflicts;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        ast_manager & m = m_imp->m;
+        d->m_num_conflicts = m_imp->m_num_conflicts;
-        imp * d = m_imp;
         #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:

src/tactic/arith/factor_tactic.cpp

@@ -333,18 +333,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        imp * d = m_imp;
         #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) {

src/tactic/arith/fix_dl_var_tactic.cpp

@@ -338,18 +338,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        imp * d = m_imp;
         #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) {

src/tactic/arith/fm_tactic.cpp

@@ -1682,18 +1682,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        imp * d = m_imp;
         #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, 

src/tactic/arith/lia2pb_tactic.cpp

@@ -345,18 +345,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        imp * d = m_imp;
         #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:

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:

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:

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 = alloc(imp, m_imp->m, m_params);
-    imp * d = m_imp;
     #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;
-    }
 }

src/tactic/arith/recover_01_tactic.cpp

@@ -425,18 +425,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        imp * d = m_imp;
         #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:

src/tactic/bv/bit_blaster_tactic.cpp

@@ -140,18 +140,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
+        imp * d = alloc(imp, m_imp->m(), m_params);
-        imp * d = m_imp;
         #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 {

src/tactic/bv/bv1_blaster_tactic.cpp

@@ -465,18 +465,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
+        imp * d = alloc(imp, m_imp->m(), m_params);
-        imp * d = m_imp;
         #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 {

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 = alloc(imp, m_imp->m);
-    imp * d = m_imp;
     #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;
-    }
 }
 

src/tactic/bv/max_bv_sharing_tactic.cpp

@@ -311,18 +311,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
+        imp * d = alloc(imp, m_imp->m(), m_params);
-        imp * d = m_imp;
         #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) {

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;
+    dealloc(m_imp);
-    #pragma omp critical (cofactor_elim_term_ite)
-    {
-        m_imp = 0;
-    }
-    dealloc(d);
 }
 
 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);
 }
-}
 
 void cofactor_elim_term_ite::cleanup() {
     ast_manager & m = m_imp->m;    
-    #pragma omp critical (cofactor_elim_term_ite) 
+    imp * d = alloc(imp, m, m_params);
+    #pragma omp critical (tactic_cancel)
     {
-        dealloc(m_imp);
+        std::swap(d, m_imp);
-        m_imp = alloc(imp, m, m_params);
     }
+    dealloc(d);
 }
 

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

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;
-    }
 }
 

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) {

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) {

src/tactic/core/elim_uncnstr_tactic.cpp

@@ -1037,17 +1037,12 @@ public:
     virtual void cleanup() {
         unsigned num_elim_apps = get_num_elim_apps();
         ast_manager & m = m_imp->m_manager;        
-        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;
-        }
         m_imp->m_num_elim_apps = num_elim_apps;
     }
 

src/tactic/core/occf_tactic.cpp

@@ -225,18 +225,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m);
-        imp * d = m_imp;
         #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:

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:

src/tactic/core/reduce_args_tactic.cpp

@@ -542,16 +542,11 @@ void reduce_args_tactic::set_cancel(bool f) {
 
 void reduce_args_tactic::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;
-    }
 }
 

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 {

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());

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 {

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) {

src/tactic/fpa/fpa2bv_tactic.cpp

@@ -139,18 +139,12 @@ public:
     }
     
     virtual void cleanup() {        
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        imp * d = m_imp;
         #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:

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 {

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;

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);
+            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);
+            t.reset_cancel();
-            }
         }
     }
 

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) {

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) {

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) {

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)
+    if (initialize) {
-        return;
         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() {