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

src/ast/ast.cpp

@@ -300,7 +300,7 @@ std::ostream & operator<<(std::ostream & out, func_decl_info const & info) {
 //
 // -----------------------------------
 
-char const * g_ast_kind_names[] = {"application", "variable", "quantifier", "sort", "function declaration" };
+static char const * g_ast_kind_names[] = {"application", "variable", "quantifier", "sort", "function declaration" };
 
 char const * get_ast_kind_name(ast_kind k) {
     return g_ast_kind_names[k];

src/ast/ast.h

@@ -1193,7 +1193,6 @@ enum pattern_op_kind {
    heurisitic quantifier instantiation.
 */
 class pattern_decl_plugin : public decl_plugin {
-    sort * m_list;
 public:
     virtual decl_plugin * mk_fresh() { return alloc(pattern_decl_plugin); }
 

src/ast/dl_decl_plugin.cpp

@@ -326,6 +326,7 @@ namespace datalog {
         }
         unsigned index0;
         sort* last_sort = 0;
+        SASSERT(num_params > 0);
         for (unsigned i = 0; i < num_params; ++i) {
             parameter const& p = params[i];
             if (!p.is_int()) {

src/ast/float_decl_plugin.cpp

@@ -200,6 +200,7 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par
     }
     else {
         m_manager->raise_exception("sort of floating point constant was not specified");
+        UNREACHABLE();
     }
 
     SASSERT(is_sort_of(s, m_family_id, FLOAT_SORT));

src/ast/func_decl_dependencies.cpp

@@ -79,7 +79,6 @@ void func_decl_dependencies::collect_ng_func_decls(expr * n, func_decl_set * s)
 */
 class func_decl_dependencies::top_sort {
     enum color { OPEN, IN_PROGRESS, CLOSED };
-    ast_manager &       m_manager;    
     dependency_graph &  m_deps;
 
     typedef obj_map<func_decl, color> color_map;
@@ -177,7 +176,7 @@ class func_decl_dependencies::top_sort {
     }
 
 public:
-    top_sort(ast_manager & m, dependency_graph & deps):m_manager(m), m_deps(deps) {}
+    top_sort(dependency_graph & deps) : m_deps(deps) {}
     
     bool operator()(func_decl * new_decl) {
 
@@ -198,7 +197,7 @@ bool func_decl_dependencies::insert(func_decl * f, func_decl_set * s) {
 
     m_deps.insert(f, s);
 
-    top_sort cycle_detector(m_manager, m_deps);
+    top_sort cycle_detector(m_deps);
     if (cycle_detector(f)) {
         m_deps.erase(f);
         dealloc(s);

src/ast/macros/quasi_macros.cpp

@@ -22,10 +22,9 @@ Revision History:
 #include"uint_set.h"
 #include"var_subst.h"
 
-quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm, basic_simplifier_plugin & p, simplifier & s) :
+quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s) :
   m_manager(m),
   m_macro_manager(mm),
-  m_bsimp(p), 
   m_simplifier(s),
   m_new_vars(m),
   m_new_eqs(m),

src/ast/macros/quasi_macros.h

@@ -32,7 +32,6 @@ class quasi_macros {
 
     ast_manager &             m_manager;
     macro_manager &           m_macro_manager;
-    basic_simplifier_plugin & m_bsimp;   
     simplifier &              m_simplifier;
     occurrences_map           m_occurrences;
     ptr_vector<expr>          m_todo;    
@@ -57,7 +56,7 @@ class quasi_macros {
     void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
 
 public:
-    quasi_macros(ast_manager & m, macro_manager & mm, basic_simplifier_plugin & p, simplifier & s);
+    quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s);
     ~quasi_macros();
     
     /**

src/ast/recurse_expr.h

@@ -30,7 +30,7 @@ class recurse_expr : public Visitor {
     vector<T, CallDestructors>                m_results2;
 
     bool is_cached(expr * n) const { T c; return m_cache.find(n, c); }
-    T get_cached(expr * n) const { T c; m_cache.find(n, c); return c; }
+    T get_cached(expr * n) const { return m_cache.find(n); }
     void cache_result(expr * n, T c) { m_cache.insert(n, c); }
     
     void visit(expr * n, bool & visited);

src/ast/substitution/matcher.cpp

@@ -18,10 +18,6 @@ Revision History:
 --*/
 #include"matcher.h"
 
-matcher::matcher(ast_manager & m):
-    m_manager(m) {
-}
-
 bool matcher::operator()(expr * e1, expr * e2, substitution & s) {
     reset();
     m_subst = &s;

src/ast/substitution/matcher.h

@@ -30,7 +30,6 @@ class matcher {
     typedef pair_hash<obj_ptr_hash<expr>, obj_ptr_hash<expr> > expr_pair_hash;
     typedef hashtable<expr_pair, expr_pair_hash, default_eq<expr_pair> > cache;
 
-    ast_manager &         m_manager;
     substitution *        m_subst;
     // cache                 m_cache;
     svector<expr_pair>    m_todo;
@@ -38,7 +37,7 @@ class matcher {
     void reset();
 
 public:
-    matcher(ast_manager & m);
+    matcher() {}
 
     /**
        \brief Return true if e2 is an instance of e1.

src/ast/substitution/substitution.cpp

@@ -148,7 +148,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
                     expr * arg     = to_app(e)->get_arg(i);
                     expr * new_arg;
                     
-                    m_apply_cache.find(expr_offset(arg, off), new_arg);
+                    VERIFY(m_apply_cache.find(expr_offset(arg, off), new_arg));
                     new_args.push_back(new_arg);
                     if (arg != new_arg)
                         has_new_args = true;

src/math/subpaving/subpaving.cpp

@@ -85,7 +85,6 @@ namespace subpaving {
     };
 
     class context_mpf_wrapper : public context_wrapper<context_mpf> {
-        f2n<mpf_manager> &            m_fm;
         unsynch_mpq_manager &         m_qm;
         scoped_mpf                    m_c;
         scoped_mpf_vector             m_as;
@@ -103,7 +102,6 @@ namespace subpaving {
     public:
         context_mpf_wrapper(f2n<mpf_manager> & fm, params_ref const & p, small_object_allocator * a):
             context_wrapper<context_mpf>(fm, p, a),
-            m_fm(fm),
             m_qm(fm.m().mpq_manager()),
             m_c(fm.m()),
             m_as(fm.m()),
@@ -145,7 +143,6 @@ namespace subpaving {
     };
 
     class context_hwf_wrapper : public context_wrapper<context_hwf> {
-        f2n<hwf_manager> &            m_fm;
         unsynch_mpq_manager &         m_qm;
         hwf                           m_c;
         svector<hwf>                  m_as;
@@ -166,7 +163,6 @@ namespace subpaving {
     public:
         context_hwf_wrapper(f2n<hwf_manager> & fm, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
             context_wrapper<context_hwf>(fm, p, a),
-            m_fm(fm),
             m_qm(qm) {
         }
 

src/muz_qe/dl_interval_relation.cpp

@@ -99,11 +99,9 @@ namespace datalog {
     }
    
     class interval_relation_plugin::rename_fn : public convenient_relation_rename_fn {
-        interval_relation_plugin& m_plugin;
     public:
-        rename_fn(interval_relation_plugin& p, const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle) 
+        rename_fn(const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle) 
-            : convenient_relation_rename_fn(orig_sig, cycle_len, cycle),
+            : convenient_relation_rename_fn(orig_sig, cycle_len, cycle) {
-              m_plugin(p){
         }
 
         virtual relation_base * operator()(const relation_base & _r) {
@@ -120,7 +118,7 @@ namespace datalog {
         if(!check_kind(r)) {
             return 0;
         }
-        return alloc(rename_fn, *this, r.get_signature(), cycle_len, permutation_cycle);
+        return alloc(rename_fn, r.get_signature(), cycle_len, permutation_cycle);
     }
      
     interval interval_relation_plugin::unite(interval const& src1, interval const& src2) {
@@ -194,11 +192,9 @@ namespace datalog {
     }
 
     class interval_relation_plugin::union_fn : public relation_union_fn {
-        interval_relation_plugin& m_plugin;
         bool                      m_is_widen;
     public:
-        union_fn(interval_relation_plugin& p, bool is_widen) :
+        union_fn(bool is_widen) :
-            m_plugin(p),
             m_is_widen(is_widen) {            
         }
 
@@ -223,7 +219,7 @@ namespace datalog {
         if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
             return 0;
         }
-        return alloc(union_fn, *this, false);
+        return alloc(union_fn, false);
     }
 
     relation_union_fn * interval_relation_plugin::mk_widen_fn(
@@ -232,7 +228,7 @@ namespace datalog {
         if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
             return 0;
         }
-        return alloc(union_fn, *this, true);
+        return alloc(union_fn, true);
     }
 
     class interval_relation_plugin::filter_identical_fn : public relation_mutator_fn {

src/muz_qe/dl_mk_explanations.cpp

@@ -527,11 +527,10 @@ namespace datalog {
     }
 
     class explanation_relation_plugin::intersection_filter_fn : public relation_intersection_filter_fn {
-        explanation_relation_plugin & m_plugin;
         func_decl_ref m_union_decl;
     public:
         intersection_filter_fn(explanation_relation_plugin & plugin)
-            : m_plugin(plugin), m_union_decl(plugin.m_union_decl) {}
+            : m_union_decl(plugin.m_union_decl) {}
 
         virtual void operator()(relation_base & tgt0, const relation_base & src0) {
             explanation_relation & tgt = static_cast<explanation_relation &>(tgt0);

src/muz_qe/dl_mk_karr_invariants.cpp

@@ -963,11 +963,8 @@ namespace datalog {
 
 
     class karr_relation_plugin::union_fn : public relation_union_fn {
-        karr_relation_plugin& m_plugin;
     public:
-        union_fn(karr_relation_plugin& p) :
+        union_fn() {}
-            m_plugin(p) {            
-        }
 
         virtual void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) {
 
@@ -991,7 +988,7 @@ namespace datalog {
         if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
             return 0;
         }
-        return alloc(union_fn, *this);
+        return alloc(union_fn);
     }
 
     class karr_relation_plugin::filter_identical_fn : public relation_mutator_fn {

src/muz_qe/dl_mk_subsumption_checker.cpp

@@ -320,9 +320,7 @@ namespace datalog {
             if(!m_ground_unconditional_rule_heads.contains(pred)) {
                 m_ground_unconditional_rule_heads.insert(pred, alloc(obj_hashtable<app>));
             }
-            obj_hashtable<app> * head_store;
+            m_ground_unconditional_rule_heads.find(pred)->insert(head);
-            m_ground_unconditional_rule_heads.find(pred, head_store);
-            head_store->insert(head);
 
         next_rule:;
         }

src/muz_qe/dl_relation_manager.cpp

@@ -1090,12 +1090,10 @@ namespace datalog {
 
     class relation_manager::default_table_rename_fn 
             : public convenient_table_rename_fn, auxiliary_table_transformer_fn {
-        const unsigned m_cycle_len;
     public:
         default_table_rename_fn(const table_signature & orig_sig, unsigned permutation_cycle_len, 
                     const unsigned * permutation_cycle) 
-                : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle), 
+                : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle) {
-                m_cycle_len(permutation_cycle_len) {
             SASSERT(permutation_cycle_len>=2);
         }
 

src/muz_qe/dl_relation_manager.h

@@ -661,17 +661,15 @@ namespace datalog {
                 SASSERT(res_idx<m_allocated_kinds.size());
                 ids.insert(spec, res_idx);
 
-                family_id2spec * idspecs;
+                family_id2spec * idspecs = m_kind_specs.find(sig);
-                VERIFY( m_kind_specs.find(sig, idspecs) );
                 idspecs->insert(m_allocated_kinds[res_idx], spec);
             }
             return m_allocated_kinds[res_idx];
         }
 
         void get_relation_spec(const relation_signature & sig, family_id kind, Spec & spec) {
-            family_id2spec * idspecs;
+            family_id2spec * idspecs = m_kind_specs.find(sig);
-            VERIFY( m_kind_specs.find(sig, idspecs) );
+            spec = idspecs->find(kind);
-            VERIFY( idspecs->find(kind, spec) );
         }
 
     };

src/muz_qe/dl_util.h

@@ -198,8 +198,6 @@ namespace datalog {
     {
         bool values_match(const expr * v1, const expr * v2);
 
-        ast_manager &    m_manager;
-
         unsigned_vector m_args1;
         unsigned_vector m_args2;
 
@@ -211,7 +209,7 @@ namespace datalog {
         static unsigned expr_cont_get_size(const ptr_vector<expr> & v) { return v.size(); }
         static expr * expr_cont_get(const ptr_vector<expr> & v, unsigned i) { return v[i]; }
     public:
-        variable_intersection(ast_manager & m) : m_manager(m), m_consts(m) {}
+        variable_intersection(ast_manager & m) : m_consts(m) {}
 
         unsigned size() const {
             return m_args1.size();

src/muz_qe/nlarith_util.cpp

@@ -1028,7 +1028,6 @@ namespace nlarith {
         };
 
         class sqrt_subst : public isubst {
-            bool m_even;
             sqrt_form const& m_s;
         public:
             sqrt_subst(imp& i, sqrt_form const& s): isubst(i), m_s(s) {}

src/muz_qe/pdr_context.cpp

@@ -1285,7 +1285,7 @@ namespace pdr {
             obj_hashtable<func_decl>::iterator itf = deps.begin(), endf = deps.end();
             for (; itf != endf; ++itf) {
                 TRACE("pdr", tout << mk_pp(pred, m) << " " << mk_pp(*itf, m) << "\n";);
-                VERIFY (rels.find(*itf, pt_user));
+                pt_user = rels.find(*itf);
                 pt_user->add_use(pt);                
             }
         }      

src/muz_qe/pdr_farkas_learner.cpp

@@ -418,11 +418,10 @@ namespace pdr {
 
     class farkas_learner::constant_replacer_cfg : public default_rewriter_cfg
     {
-        ast_manager& m;
         const obj_map<expr, expr *>& m_translation;
     public:
-        constant_replacer_cfg(ast_manager& m, const obj_map<expr, expr *>& translation)
+        constant_replacer_cfg(const obj_map<expr, expr *>& translation)
-            : m(m), m_translation(translation)
+            : m_translation(translation)
         { }
 
         bool get_subst(expr * s, expr * & t, proof * & t_pr) {

src/muz_qe/qe.cpp

@@ -1093,8 +1093,7 @@ namespace qe {
         bool has_branch(rational const& branch_id) const { return m_branch_index.contains(branch_id); }
 
         search_tree* child(rational const& branch_id) const {
-            unsigned idx;
+            unsigned idx = m_branch_index.find(branch_id);
-            VERIFY(m_branch_index.find(branch_id, idx));
             return m_children[idx];
         }
 
@@ -1963,7 +1962,6 @@ namespace qe {
         expr_ref                m_assumption;
         bool                    m_produce_models;
         ptr_vector<quant_elim_plugin> m_plugins;
-        unsigned                     m_name_counter; // fresh-id
         volatile bool            m_cancel;
         bool                     m_eliminate_variables_as_block;
 
@@ -1973,7 +1971,6 @@ namespace qe {
             m_fparams(p),
             m_assumption(m),
             m_produce_models(m_fparams.m_model),
-            m_name_counter(0),
             m_cancel(false),
             m_eliminate_variables_as_block(true)
           {

src/muz_qe/qe_dl_plugin.cpp

@@ -12,14 +12,12 @@ namespace qe {
     // dl_plugin
 
     class eq_atoms {
-        ast_manager& m;
         expr_ref_vector m_eqs;
         expr_ref_vector m_neqs;
         app_ref_vector m_eq_atoms;
         app_ref_vector m_neq_atoms;
     public:
         eq_atoms(ast_manager& m):
-          m(m),
           m_eqs(m),
           m_neqs(m),
           m_eq_atoms(m), 

src/muz_qe/tab_context.cpp

@@ -740,7 +740,6 @@ namespace tb {
         typedef svector<double>                   double_vector;
         typedef obj_map<func_decl, double_vector> score_map;
         typedef obj_map<app, double>              pred_map;
-        datalog::context&  m_ctx;
         ast_manager&       m;
         datatype_util      dt;
         score_map          m_score_map;
@@ -750,19 +749,16 @@ namespace tb {
         pred_map           m_pred_map;
         expr_ref_vector    m_refs;
         double             m_weight_multiply;
-        unsigned           m_num_invocations;
         unsigned           m_update_frequency;
         unsigned           m_next_update;
         
 
     public:
         selection(datalog::context& ctx):
-            m_ctx(ctx),
             m(ctx.get_manager()),
             dt(m),
             m_refs(m),
             m_weight_multiply(1.0),
-            m_num_invocations(0),
             m_update_frequency(20),
             m_next_update(20) {
             set_strategy(ctx.get_params().tab_selection());

src/parsers/smt/smtparser.cpp

@@ -1472,7 +1472,7 @@ private:
 
                     SASSERT(sorts.size() > 0);
 
-                    idbuilder* pop_q = new (region) pop_quantifier(this, (head_symbol == m_forall), weight, qid, skid, patterns, no_patterns, sorts, vars, local_scope, current);
+                    idbuilder* pop_q = new (region) pop_quantifier(this, (head_symbol == m_forall), weight, qid, skid, patterns, no_patterns, sorts, vars, local_scope);
 
                     expr_ref_vector * empty_v = alloc(expr_ref_vector, m_manager);
                     up.push_back(new (region) parse_frame(current, pop_q, empty_v, 0, m_binding_level));
@@ -2522,7 +2522,7 @@ private:
     class pop_quantifier : public idbuilder {
     public:
         pop_quantifier(smtparser * smt, bool is_forall, int weight, symbol const& qid, symbol const& skid, expr_ref_buffer & patterns, expr_ref_buffer & no_patterns, sort_ref_buffer & sorts, 
-                       svector<symbol>& vars, symbol_table<idbuilder*> & local_scope, proto_expr* p_expr):
+                       svector<symbol>& vars, symbol_table<idbuilder*> & local_scope):
             m_smt(smt),
             m_is_forall(is_forall),
             m_weight(weight),
@@ -2531,8 +2531,7 @@ private:
             m_patterns(m_smt->m_manager),
             m_no_patterns(m_smt->m_manager),
             m_sorts(m_smt->m_manager),
-            m_local_scope(local_scope),
+            m_local_scope(local_scope) {
-            m_p_expr(p_expr) {
             SASSERT(sorts.size() == vars.size());
 
             m_vars.append(vars);
@@ -2619,7 +2618,6 @@ private:
         sort_ref_buffer            m_sorts;
         svector<symbol>            m_vars;
         symbol_table<idbuilder*>&  m_local_scope;
-        proto_expr*                m_p_expr;
     };
 
     class builtin_builder : public idbuilder {

src/parsers/smt2/smt2scanner.cpp

@@ -243,7 +243,6 @@ namespace smt2 {
     }
     
     scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
-        m_ctx(ctx),
         m_interactive(interactive), 
         m_spos(0),
         m_curr(0), // avoid Valgrind warning

src/parsers/smt2/smt2scanner.h

@@ -31,7 +31,6 @@ namespace smt2 {
     
     class scanner {
     private:
-        cmd_context &      m_ctx;
         bool               m_interactive;
         int                m_spos; // position in the current line of the stream
         char               m_curr;  // current char;

src/smt/asserted_formulas.cpp

@@ -408,7 +408,7 @@ void asserted_formulas::apply_quasi_macros() {
     TRACE("before_quasi_macros", display(tout););
     expr_ref_vector  new_exprs(m_manager);
     proof_ref_vector new_prs(m_manager);      
-    quasi_macros proc(m_manager, m_macro_manager, *m_bsimp, m_simplifier);    
+    quasi_macros proc(m_manager, m_macro_manager, m_simplifier);    
     while (proc(m_asserted_formulas.size() - m_asserted_qhead, 
                 m_asserted_formulas.c_ptr() + m_asserted_qhead, 
                 m_asserted_formula_prs.c_ptr() + m_asserted_qhead,

src/smt/database.h

@@ -1,4 +1,4 @@
-char const * g_pattern_database =
+static char const * g_pattern_database =
 "(benchmark patterns \n"
 " :status unknown \n"
 " :logic ALL \n"

src/smt/expr_context_simplifier.cpp

@@ -311,7 +311,7 @@ bool expr_context_simplifier::is_false(expr* e) const {
 // 
 
 expr_strong_context_simplifier::expr_strong_context_simplifier(smt_params& p, ast_manager& m): 
-    m_manager(m), m_params(p), m_arith(m), m_id(0), m_fn(0,m), m_solver(m, p) {
+    m_manager(m), m_arith(m), m_fn(0,m), m_solver(m, p) {
     sort* i_sort = m_arith.mk_int();
     m_fn = m.mk_func_decl(symbol(0xbeef101), i_sort, m.mk_bool_sort());
 }

src/smt/expr_context_simplifier.h

@@ -57,9 +57,7 @@ private:
 
 class expr_strong_context_simplifier {
     ast_manager& m_manager;
-    smt_params & m_params;
     arith_util    m_arith;
-    unsigned      m_id;
     func_decl_ref m_fn;
     smt::kernel   m_solver;
     

src/smt/mam.cpp

@@ -1849,11 +1849,9 @@ namespace smt {
         unsigned            m_curr_max_generation;  // temporary var used to store a copy of m_max_generation
         unsigned            m_num_args;
         unsigned            m_oreg;
-        unsigned            m_ireg;
         enode *             m_n1;
         enode *             m_n2;
         enode *             m_app;
-        instruction *       m_alt;
         const bind *        m_b;
         ptr_vector<enode>   m_used_enodes;
         unsigned            m_curr_used_enodes_size;

src/smt/theory_dl.cpp

@@ -68,14 +68,11 @@ namespace smt {
         bv_util& b() { return m_bv; }
 
         class dl_value_proc : public smt::model_value_proc {
-            smt::model_generator &      m_mg; 
             theory_dl&                  m_th;
             smt::enode*                 m_node;
         public:
             
-            dl_value_proc(smt::model_generator & m, theory_dl& th, smt::enode* n):
+            dl_value_proc(theory_dl& th, smt::enode* n) : m_th(th), m_node(n) {}
-                m_mg(m), m_th(th), m_node(n)
-            { }
             
             virtual void get_dependencies(buffer<smt::model_value_dependency> & result) {}
             
@@ -165,8 +162,8 @@ namespace smt {
             m.register_factory(alloc(dl_factory, m_util, m.get_model()));
         }
         
-        virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator & m) {
+        virtual smt::model_value_proc * mk_value(smt::enode * n) {
-            return alloc(dl_value_proc, m, *this, n);
+            return alloc(dl_value_proc, *this, n);
         }
 
         virtual void apply_sort_cnstr(enode * n, sort * s) {

src/tactic/ufbv/quasi_macros_tactic.cpp

@@ -67,7 +67,7 @@ class quasi_macros_tactic : public tactic {
             simp.register_plugin(bvsimp);
                 
             macro_manager mm(m_manager, simp);
-            quasi_macros qm(m_manager, mm, *bsimp, simp);
+            quasi_macros qm(m_manager, mm, simp);
             bool more = true;
         
             expr_ref_vector forms(m_manager), new_forms(m_manager);

src/tactic/ufbv/ufbv_rewriter.cpp

@@ -442,11 +442,10 @@ expr * ufbv_rewriter::rewrite(expr * n) {
 }
 
 class ufbv_rewriter::add_back_idx_proc {
-    ast_manager &  m_manager;
     back_idx_map & m_back_idx;
     expr *         m_expr;
 public:
-    add_back_idx_proc(ast_manager & m, back_idx_map & bi, expr * e):m_manager(m),m_back_idx(bi),m_expr(e) {}
+    add_back_idx_proc(back_idx_map & bi, expr * e):m_back_idx(bi),m_expr(e) {}
     void operator()(var * n) {}
     void operator()(quantifier * n) {}
     void operator()(app * n) {        
@@ -469,11 +468,10 @@ public:
 };
 
 class ufbv_rewriter::remove_back_idx_proc {
-    ast_manager &  m_manager;
     back_idx_map & m_back_idx;
     expr *         m_expr;
 public:
-    remove_back_idx_proc(ast_manager & m, back_idx_map & bi, expr * e):m_manager(m),m_back_idx(bi),m_expr(e) {}
+    remove_back_idx_proc(back_idx_map & bi, expr * e):m_back_idx(bi),m_expr(e) {}
     void operator()(var * n) {}
     void operator()(quantifier * n) {}    
     void operator()(app * n) {        
@@ -511,7 +509,7 @@ void ufbv_rewriter::reschedule_processed(func_decl * f) {
             expr * p = *sit;
             // remove p from m_processed and m_back_idx
             m_processed.remove(p);
-            remove_back_idx_proc proc(m_manager, m_back_idx, p); // this could change it->m_value, thus we need the `temp' set.
+            remove_back_idx_proc proc(m_back_idx, p); // this could change it->m_value, thus we need the `temp' set.
             for_each_expr(proc, p);
             // insert p into m_todo                
             m_todo.push_back(p);
@@ -619,7 +617,7 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
                     //     remove d from m_back_idx                    
                     // just remember it here, because otherwise it and/or esit might become invalid?
                     // to_remove.insert(d); 
-                    remove_back_idx_proc proc(m_manager, m_back_idx, d);
+                    remove_back_idx_proc proc(m_back_idx, d);
                     for_each_expr(proc, d);
                     //     insert d into m_todo
                     m_todo.push_back(d);                    
@@ -674,7 +672,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
             // insert n' into m_processed
             m_processed.insert(np);            
             // update m_back_idx (traverse n' and for each uninterpreted function declaration f in n' add the entry f->n' to m_back_idx)            
-            add_back_idx_proc proc(m_manager, m_back_idx, np);
+            add_back_idx_proc proc(m_back_idx, np);
             for_each_expr(proc, np);
         } else {            
             // np is a demodulator that allows us to replace 'large' with 'small'.
@@ -702,7 +700,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
             insert_fwd_idx(large, small, to_quantifier(np));
 
             // update m_back_idx
-            add_back_idx_proc proc(m_manager, m_back_idx, np);
+            add_back_idx_proc proc(m_back_idx, np);
             for_each_expr(proc, np);
         }        
     }

src/test/matcher.cpp

@@ -26,7 +26,7 @@ void tst_match(ast_manager & m, app * t, app * i) {
     substitution s(m);
     s.reserve(2, 10); // reserving a big number of variables to be safe.
 
-    matcher      match(m);
+    matcher      match;
     std::cout << "Is " << mk_pp(i, m) << " an instance of " << mk_pp(t, m) << "\n";
     if (match(t, i, s)) {
         std::cout << "yes\n";

src/util/bit_util.cpp

@@ -19,6 +19,7 @@ Revision History:
 #include"bit_util.h"
 #include"util.h"
 #include"debug.h"
+#include <cstring>
 
 /**
    \brief (Debugging version) Return the position of the most significant (set) bit of a
@@ -67,7 +68,11 @@ unsigned msb_pos(unsigned v) {
 */
 unsigned nlz_core(unsigned x) {
     SASSERT(x != 0);
+#ifdef __GNUC__
+    return __builtin_clz(x);
+#else
     return 31 - msb_pos(x);
+#endif
 }
 
 /**
@@ -92,8 +97,15 @@ unsigned nlz(unsigned sz, unsigned const * data) {
 */
 unsigned ntz_core(unsigned x) {
     SASSERT(x != 0);
+#ifdef __GNUC__
+    return __builtin_ctz(x);
+#else
     float f = static_cast<float>(x & static_cast<unsigned>(-static_cast<int>(x)));
-    return (*reinterpret_cast<unsigned *>(&f) >> 23) - 0x7f;
+    unsigned u;
+    SASSERT(sizeof(u) == sizeof(f));
+    memcpy(&u, &f, sizeof(u));
+    return (u >> 23) - 0x7f;
+#endif
 }
 
 /**

src/util/debug.cpp

@@ -24,7 +24,7 @@ Revision History:
 #include"str_hashtable.h"
 #include"z3_exception.h"
 
-volatile bool g_enable_assertions = true;
+static volatile bool g_enable_assertions = true;
 
 void enable_assertions(bool f) {
     g_enable_assertions = f;
@@ -41,7 +41,7 @@ void notify_assertion_violation(const char * fileName, int line, const char * co
     std::cerr << condition << "\n";
 }
 
-str_hashtable* g_enabled_debug_tags = 0;
+static str_hashtable* g_enabled_debug_tags = 0;
 
 static void init_debug_table() {
     if (!g_enabled_debug_tags) {

src/util/debug.h

@@ -29,6 +29,10 @@ bool assertions_enabled();
 #include<crtdbg.h>
 #endif
 
+#ifndef __has_builtin
+# define __has_builtin(x) 0
+#endif
+
 #include"error_codes.h"
 #include"warning.h"
 
@@ -53,7 +57,14 @@ bool is_debug_enabled(const char * tag);
 #define SASSERT(COND) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
 #define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
 #define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); })
+
+#if (defined(__GNUC__) && ((__GNUC__ * 100 + __GNUC_MINOR__) >= 405)) || __has_builtin(__builtin_unreachable)
+// only available in gcc >= 4.5 and in newer versions of clang
+# define UNREACHABLE() __builtin_unreachable()
+#else
 #define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();)
+#endif
+
 #define NOT_IMPLEMENTED_YET() { std::cerr << "NOT IMPLEMENTED YET!\n"; UNREACHABLE(); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)
 
 #ifdef Z3DEBUG

src/util/gparams.cpp

@@ -22,7 +22,7 @@ Notes:
 
 extern void gparams_register_modules();
 
-char const * g_old_params_names[] = {
+static char const * g_old_params_names[] = {
     "arith_adaptive","arith_adaptive_assertion_threshold","arith_adaptive_gcd","arith_adaptive_propagation_threshold","arith_add_binary_bounds","arith_blands_rule_threshold","arith_branch_cut_ratio","arith_dump_lemmas","arith_eager_eq_axioms","arith_eager_gcd","arith_eq_bounds","arith_euclidean_solver","arith_expand_eqs","arith_force_simplex","arith_gcd_test","arith_ignore_int","arith_lazy_adapter","arith_lazy_pivoting","arith_max_lemma_size","arith_process_all_eqs","arith_propagate_eqs","arith_propagation_mode","arith_propagation_threshold","arith_prop_strategy","arith_random_initial_value","arith_random_lower","arith_random_seed","arith_random_upper","arith_reflect","arith_skip_big_coeffs","arith_small_lemma_size","arith_solver","arith_stronger_lemmas","array_always_prop_upward","array_canonize","array_cg","array_delay_exp_axiom","array_extensional","array_laziness","array_lazy_ieq","array_lazy_ieq_delay","array_solver","array_weak","async_commands","at_labels_cex","auto_config","bb_eager","bb_ext_gates","bb_quantifiers","bin_clauses","bit2int","bv2int_distribute","bv_blast_max_size","bv_cc","bv_enable_int2bv_propagation","bv_lazy_le","bv_max_sharing","bv_reflect","bv_solver","case_split","check_at_labels","check_proof","cnf_factor","cnf_mode","context_simplifier","dack","dack_eq","dack_factor","dack_gc","dack_gc_inv_decay","dack_threshold","default_qid","default_table","default_table_checked","delay_units","delay_units_threshold","der","display_config","display_dot_proof","display_error_for_visual_studio","display_features","display_proof","display_unsat_core","distribute_forall","dt_lazy_splits","dump_goal_as_smt","elim_and","elim_bounds","elim_nlarith_quantifiers","elim_quantifiers","elim_term_ite","ematching","engine","eq_propagation","hi_div0","ignore_bad_patterns","ignore_setparameter","instruction_max","inst_gen","interactive","internalizer_nnf","lemma_gc_factor","lemma_gc_half","lemma_gc_initial","lemma_gc_new_clause_activity","lemma_gc_new_clause_relevancy","lemma_gc_new_old_ratio","lemma_gc_old_clause_activity","lemma_gc_old_clause_relevancy","lemma_gc_strategy","lift_ite","lookahead_diseq","macro_finder","max_conflicts","max_counterexamples","mbqi","mbqi_force_template","mbqi_max_cexs","mbqi_max_cexs_incr","mbqi_max_iterations","mbqi_trace","minimize_lemmas","model","model_compact","model_completion","model_display_arg_sort","model_hide_unused_partitions","model_on_final_check","model_on_timeout","model_partial","model_v1","model_v2","model_validate","new_core2th_eq","ng_lift_ite","nl_arith","nl_arith_branching","nl_arith_gb","nl_arith_gb_eqs","nl_arith_gb_perturbate","nl_arith_gb_threshold","nl_arith_max_degree","nl_arith_rounds","nnf_factor","nnf_ignore_labels","nnf_mode","nnf_sk_hack","order","order_var_weight","order_weights","phase_selection","pi_arith","pi_arith_weight","pi_avoid_skolems","pi_block_looop_patterns","pi_max_multi_patterns","pi_non_nested_arith_weight","pi_nopat_weight","pi_pull_quantifiers","pi_use_database","pi_warnings","pp_bounded","pp_bv_literals","pp_bv_neg","pp_decimal","pp_decimal_precision","pp_fixed_indent","pp_flat_assoc","pp_max_depth","pp_max_indent","pp_max_num_lines","pp_max_ribbon","pp_max_width","pp_min_alias_size","pp_simplify_implies","pp_single_line","precedence","precedence_gen","pre_demodulator","pre_simplifier","pre_simplify_expr","profile_res_sub","progress_sampling_freq","proof_mode","propagate_booleans","propagate_values","pull_cheap_ite_trees","pull_nested_quantifiers","qi_conservative_final_check","qi_cost","qi_eager_threshold","qi_lazy_instantiation","qi_lazy_quick_checker","qi_lazy_threshold","qi_max_eager_multi_patterns","qi_max_instances","qi_max_lazy_multi_pattern_matching","qi_new_gen","qi_profile","qi_profile_freq","qi_promote_unsat","qi_quick_checker","quasi_macros","random_case_split_freq","random_initial_activity","random_seed","recent_lemma_threshold","reduce_args","refine_inj_axiom","relevancy","relevancy_lemma","rel_case_split_order","restart_adaptive","restart_agility_threshold","restart_factor","restart_initial","restart_strategy","restricted_quasi_macros","simplify_clauses","smtlib2_compliant","smtlib_category","smtlib_dump_lemmas","smtlib_logic","smtlib_source_info","smtlib_trace_path","soft_timeout","solver","spc_bs","spc_es","spc_factor_subsumption_index_opt","spc_initial_subsumption_index_opt","spc_max_subsumption_index_features","spc_min_func_freq_subsumption_index","spc_num_iterations","spc_trace","statistics","strong_context_simplifier","tick","trace","trace_file_name","type_check","user_theory_persist_axioms","user_theory_preprocess_axioms","verbose","warning","well_sorted_check","z3_solver_ll_pp","z3_solver_smt_pp", 0 };
 
 bool is_old_param_name(symbol const & name) {
@@ -35,7 +35,7 @@ bool is_old_param_name(symbol const & name) {
     return false;
 }
 
-char const * g_params_renames[] = {
+static char const * g_params_renames[] = {
     "proof_mode", "proof",
     "soft_timeout", "timeout",
     "mbqi", "smt.mbqi",

src/util/hwf.h

@@ -28,6 +28,12 @@ class hwf {
     friend class hwf_manager;
     double value;
     hwf & operator=(hwf const & other) { UNREACHABLE(); return *this; }
+    uint64 get_raw() const {
+      uint64 n;
+      SASSERT(sizeof(n) == sizeof(value));
+      memcpy(&n, &value, sizeof(value));
+      return n;
+    }
 
 public:    
     hwf() {}
@@ -122,16 +128,15 @@ public:
     
     
     bool sgn(hwf const & x) const { 
-        uint64 raw = *reinterpret_cast<uint64 const *>(&x.value);
+        return (x.get_raw() & 0x8000000000000000ull) != 0; 
-        return (raw & 0x8000000000000000ull) != 0; 
     }
 
     const uint64 sig(hwf const & x) const { 
-        return *reinterpret_cast<uint64 const *>(&x.value) & 0x000FFFFFFFFFFFFFull;
+        return x.get_raw() & 0x000FFFFFFFFFFFFFull;
     }
 
     const int exp(hwf const & x) const {         
-        return ((*reinterpret_cast<uint64 const *>(&x.value) & 0x7FF0000000000000ull) >> 52) - 1023;
+        return ((x.get_raw() & 0x7FF0000000000000ull) >> 52) - 1023;
     }
 
     bool is_nan(hwf const & x);
@@ -151,7 +156,7 @@ public:
     void mk_pinf(hwf & o);
     void mk_ninf(hwf & o);
     
-    unsigned hash(hwf const & a) { return hash_ull(*reinterpret_cast<const unsigned long long*>(&a.value)); }
+    unsigned hash(hwf const & a) { return hash_ull(a.get_raw()); }
 
     inline void set_rounding_mode(mpf_rounding_mode rm);
 

src/util/memory_manager.cpp

@@ -27,14 +27,14 @@ void mem_finalize();
 out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
 }
 
-volatile bool g_memory_out_of_memory  = false;
+static volatile bool g_memory_out_of_memory  = false;
-bool       g_memory_initialized       = false;
+static bool       g_memory_initialized       = false;
-long long  g_memory_alloc_size        = 0;
+static long long  g_memory_alloc_size        = 0;
-long long  g_memory_max_size          = 0;
+static long long  g_memory_max_size          = 0;
-long long  g_memory_max_used_size     = 0;
+static long long  g_memory_max_used_size     = 0;
-long long  g_memory_watermark         = 0;
+static long long  g_memory_watermark         = 0;
-bool       g_exit_when_out_of_memory  = false;
+static bool       g_exit_when_out_of_memory  = false;
-char const * g_out_of_memory_msg      = "ERROR: out of memory";
+static char const * g_out_of_memory_msg      = "ERROR: out of memory";
 
 void memory::exit_when_out_of_memory(bool flag, char const * msg) {
     g_exit_when_out_of_memory = flag;

src/util/warning.cpp

@@ -60,11 +60,11 @@ void myInvalidParameterHandler(
 #define END_ERR_HANDLER() {}
 #endif
 
-bool g_warning_msgs   = true;
+static bool g_warning_msgs   = true;
-bool g_use_std_stdout = false;
+static bool g_use_std_stdout = false;
-std::ostream* g_error_stream = 0;
+static std::ostream* g_error_stream = 0;
-std::ostream* g_warning_stream = 0;
+static std::ostream* g_warning_stream = 0;
-bool g_show_error_msg_prefix = true;
+static bool g_show_error_msg_prefix = true;
 
 void send_warnings_to_stdout(bool flag) {
     g_use_std_stdout = flag;