diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 69e9e361b..7db1b5f21 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -39,6 +39,7 @@ ONLY_MAKEFILES = False
 Z3PY_SRC_DIR=None
 VS_PROJ = False
 TRACE = False
+DOTNET_ENABLED=False
 
 VER_MAJOR=None
 VER_MINOR=None
@@ -101,6 +102,8 @@ if os.name == 'nt':
     IS_WINDOW=True
     # Visual Studio already displays the files being compiled
     SHOW_CPPS=False
+    # Enable .Net bindings by default on windows
+    DOTNET_ENABLED=True
 
 def display_help():
     print "mk_make.py: Z3 Makefile generator\n"
@@ -116,21 +119,23 @@ def display_help():
     print "  -c, --showcpp                 display file .cpp file names before invoking compiler."
     print "  -v, --vsproj                  generate Visual Studio Project Files."
     print "  -t, --trace                   enable tracing in release mode."
+    print "  -n, --nodotnet                do not generate Microsoft.Z3.dll make rules."
     exit(0)
 
 # Parse configuration option for mk_make script
 def parse_options():
-    global VERBOSE, DEBUG_MODE, IS_WINDOW, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE
-    options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:dsxhmcvt', ['build=', 
-                                                                        'debug',
-                                                                        'silent',
-                                                                        'x64',
-                                                                        'help',
-                                                                        'makefiles',
-                                                                        'showcpp',
-                                                                        'vsproj',
-                                                                        'trace'
-                                                                        ])
+    global VERBOSE, DEBUG_MODE, IS_WINDOW, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, DOTNET_ENABLED
+    options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:dsxhmcvtn', ['build=', 
+                                                                         'debug',
+                                                                         'silent',
+                                                                         'x64',
+                                                                         'help',
+                                                                         'makefiles',
+                                                                         'showcpp',
+                                                                         'vsproj',
+                                                                         'trace',
+                                                                         'nodotnet'
+                                                                         ])
     for opt, arg in options:
         if opt in ('-b', '--build'):
             if arg == 'src':
@@ -154,6 +159,8 @@ def parse_options():
             VS_PROJ = True
         elif opt in ('-t', '--trace'):
             TRACE = True
+        elif opt in ('-n', '--nodotnet'):
+            DOTNET_ENABLED = False
         else:
             raise MKException("Invalid command line option '%s'" % opt)
         
@@ -583,7 +590,7 @@ class DotNetDLLComponent(Component):
         self.assembly_info_dir = assembly_info_dir 
 
     def mk_makefile(self, out):
-        if IS_WINDOW:
+        if DOTNET_ENABLED:
             cs_fp_files = []
             cs_files    = []
             for cs_file in get_cs_files(self.src_dir):
@@ -612,16 +619,17 @@ class DotNetDLLComponent(Component):
             return
     
     def main_component(self):
-        return IS_WINDOW
+        return DOTNET_ENABLED
 
     def has_assembly_info(self):
         return True
 
     def mk_win_dist(self, build_path, dist_path):
-        # Assuming all DotNET dll should be in the distribution
-        mk_dir('%s/bin' % dist_path)
-        shutil.copy('%s/%s.dll' % (build_path, self.dll_name),
-                    '%s/bin/%s.dll' % (dist_path, self.dll_name))
+        if DOTNET_ENABLED:
+            # Assuming all DotNET dll should be in the distribution
+            mk_dir('%s/bin' % dist_path)
+            shutil.copy('%s/%s.dll' % (build_path, self.dll_name),
+                        '%s/bin/%s.dll' % (dist_path, self.dll_name))
 
 class ExampleComponent(Component):
     def __init__(self, name, path):
@@ -685,7 +693,7 @@ class DotNetExampleComponent(ExampleComponent):
         return IS_WINDOW
 
     def mk_makefile(self, out):
-        if IS_WINDOW:
+        if DOTNET_ENABLED:
             dll_name = get_component(DOTNET_COMPONENT).dll_name
             dll = '%s.dll' % dll_name
             exefile = '%s.exe' % self.name
diff --git a/scripts/update_api.py b/scripts/update_api.py
index 2d8f771b5..237fa80a6 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -32,6 +32,12 @@ dotnet_fileout = '%s/Native.cs' % dotnet_dir
 ##
 log_h.write('// Automatically generated file\n')
 log_h.write('#include\"z3.h\"\n')
+log_h.write('#ifdef __GNUC__\n')
+log_h.write('#define _Z3_UNUSED __attribute__((unused))\n')
+log_h.write('#else\n')
+log_h.write('#define _Z3_UNUSED\n')
+log_h.write('#endif\n')
+
 ##
 log_c.write('// Automatically generated file\n')
 log_c.write('#include<iostream>\n')
@@ -432,12 +438,12 @@ def mk_log_macro(file, name, params):
                 cap = param_array_capacity_pos(p)
                 if cap not in auxs:
                     auxs.add(cap)
-                    file.write("unsigned Z3ARG%s; " % cap)
+                    file.write("unsigned _Z3_UNUSED Z3ARG%s; " % cap)
                 sz  = param_array_size_pos(p)
                 if sz not in auxs:
                     auxs.add(sz)
-                    file.write("unsigned * Z3ARG%s; " % sz)
-            file.write("%s Z3ARG%s; " % (param2str(p), i))
+                    file.write("unsigned * _Z3_UNUSED Z3ARG%s; " % sz)
+            file.write("%s _Z3_UNUSED Z3ARG%s; " % (param2str(p), i))
         i = i + 1
     file.write("if (_LOG_CTX.enabled()) { log_%s(" % name)
     i = 0
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index b15f34629..222d91081 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -130,7 +130,7 @@ namespace api {
         ast_manager& m = m_context.get_manager();
         
         datalog::context ctx(m, m_context.get_fparams());
-        datalog::rule_manager& rm = ctx.get_rule_manager();
+        // datalog::rule_manager& rm = ctx.get_rule_manager();
         for (unsigned i = 0; i < num_rules; ++i) {
             expr* rule = rules[i], *body, *head;
             while (true) {
diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
index 03e947c8a..0a76c710e 100644
--- a/src/api/api_parsers.cpp
+++ b/src/api/api_parsers.cpp
@@ -296,7 +296,7 @@ extern "C" {
                                 Z3_symbol const decl_names[],
                                 Z3_func_decl const decls[]) {
         Z3_TRY;
-        cmd_context ctx(mk_c(c)->fparams(), false, &(mk_c(c)->m()));
+        cmd_context ctx(&mk_c(c)->fparams(), false, &(mk_c(c)->m()));
         ctx.set_ignore_check(true);
         if (exec) {
             ctx.set_solver(alloc(z3_context_solver, *mk_c(c)));
@@ -362,7 +362,7 @@ extern "C" {
                                          Z3_symbol decl_names[],
                                          Z3_func_decl decls[]) { 
         Z3_TRY;
-        cmd_context ctx(mk_c(c)->fparams(), false, &(mk_c(c)->m()));
+        cmd_context ctx(&mk_c(c)->fparams(), false, &(mk_c(c)->m()));
         std::string s(str);
         std::istringstream is(s);
         // No logging for this one, since it private.
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 059ea5e47..86f30ed73 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -225,7 +225,6 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app * & hea
    \remark n is a "polynomial".
 */
 bool macro_util::poly_contains_head(expr * n, func_decl * f, expr * exception) const {
-    expr * curr = n;
     unsigned num_args;
     expr * const * args;
     if (is_add(n)) {
@@ -734,7 +733,6 @@ void macro_util::get_rest_clause_as_cond(expr * except_lit, expr_ref & extra_con
 
 void macro_util::collect_poly_args(expr * n, expr * exception, ptr_buffer<expr> & args) {
     args.reset();
-    bool stop = false;
     unsigned num_args;
     expr * const * _args;
     if (is_add(n)) {
@@ -762,7 +760,6 @@ void macro_util::add_arith_macro_candidate(app * head, unsigned num_decls, expr
 void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * atom, unsigned num_decls, bool is_ineq, macro_candidates & r) {
     if (!is_add(lhs) && m_manager.is_eq(atom)) // this case is a simple macro.
         return;
-    bool stop = false;
     ptr_buffer<expr> args;
     unsigned lhs_num_args;
     expr * const * lhs_args;
diff --git a/src/ast/normal_forms/cnf.cpp b/src/ast/normal_forms/cnf.cpp
index cda4272a9..f43b85154 100644
--- a/src/ast/normal_forms/cnf.cpp
+++ b/src/ast/normal_forms/cnf.cpp
@@ -273,13 +273,10 @@ void cnf::reduce1_or(app * n, bool in_q) {
         if (m_params.m_cnf_mode != CNF_OPPORTUNISTIC || result_size < m_params.m_cnf_factor) {
             expr_ref_buffer  cheap_args(m_manager);
             proof_ref_buffer cheap_args_pr(m_manager);
-            bool named_args;
             if (is_too_expensive(result_size, f_args)) {
-                named_args = true;
                 name_args(f_args, cheap_args, cheap_args_pr);
             }
             else {
-                named_args = false;
                 cheap_args.append(f_args.size(), f_args.c_ptr());
             }
             
diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp
index 3fe68c1ee..aca739949 100644
--- a/src/ast/pattern/expr_pattern_match.cpp
+++ b/src/ast/pattern/expr_pattern_match.cpp
@@ -404,7 +404,7 @@ expr_pattern_match::initialize(char const * spec_string) {
 
     std::istringstream is(spec_string);
     front_end_params p;
-    cmd_context      ctx(p, true, &m_manager);
+    cmd_context      ctx(&p, true, &m_manager);
     VERIFY(parse_smt2_commands(ctx, is));
 
     ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 5e80863de..e9a613d4e 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -300,12 +300,13 @@ public:
     }
 };
 
-cmd_context::cmd_context(front_end_params & params, bool main_ctx, ast_manager * m, symbol const & l):
+cmd_context::cmd_context(front_end_params * params, bool main_ctx, ast_manager * m, symbol const & l):
     m_main_ctx(main_ctx),
-    m_params(params),
+    m_params(params == 0 ? alloc(front_end_params) : params),
+    m_params_owner(params == 0),
     m_logic(l),
     m_interactive_mode(false),
-    m_global_decls(!params.m_smtlib2_compliant), // SMTLIB 2.0 uses scoped decls.
+    m_global_decls(!this->params().m_smtlib2_compliant), // SMTLIB 2.0 uses scoped decls.
     m_print_success(false), // params.m_smtlib2_compliant), 
     m_random_seed(0),
     m_produce_unsat_cores(false),
@@ -340,6 +341,11 @@ cmd_context::~cmd_context() {
     finalize_cmds();
     finalize_tactic_cmds();
     finalize_probes();
+    m_solver = 0;
+    m_check_sat_result = 0;
+    if (m_params_owner) {
+        dealloc(m_params);
+    }
 }
 
 cmd_context::check_sat_state cmd_context::cs_state() const {
@@ -531,10 +537,10 @@ void cmd_context::init_manager() {
     SASSERT(m_manager == 0);
     SASSERT(m_pmanager == 0);
     m_check_sat_result = 0;
-    m_manager  = alloc(ast_manager, m_params.m_proof_mode, m_params.m_trace_stream);
+    m_manager  = alloc(ast_manager, params().m_proof_mode, params().m_trace_stream);
     m_pmanager = alloc(pdecl_manager, *m_manager);
     init_manager_core(true);
-    if (m_params.m_smtlib2_compliant)
+    if (params().m_smtlib2_compliant)
         m_manager->enable_int_real_coercions(false);
 }
 
@@ -1240,7 +1246,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         init_manager();
     if (m_solver) {
         m_check_sat_result = m_solver.get(); // solver itself stores the result.
-        m_solver->set_front_end_params(m_params);
+        m_solver->set_front_end_params(params());
         m_solver->set_progress_callback(this);
         m_solver->set_produce_proofs(produce_proofs());
         m_solver->set_produce_models(produce_models());
@@ -1390,7 +1396,7 @@ void cmd_context::validate_model() {
 void cmd_context::set_solver(solver * s) {
     m_check_sat_result = 0;
     m_solver = s;
-    m_solver->set_front_end_params(m_params);
+    m_solver->set_front_end_params(params());
     if (has_manager() && s != 0) {
         m_solver->init(m(), m_logic);
         // assert formulas and create scopes in the new solver.
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index d730ba002..efbfbfb75 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -133,7 +133,8 @@ public:
 
 protected:
     bool                         m_main_ctx;
-    front_end_params &           m_params;
+    front_end_params *           m_params;
+    bool                         m_params_owner;
     symbol                       m_logic;
     bool                         m_interactive_mode;
     bool                         m_global_decls;
@@ -246,9 +247,9 @@ protected:
     void print_unsupported_info(symbol const& s) { if (s != symbol::null) diagnostic_stream() << "; " << s << std::endl;}
 
 public:
-    cmd_context(front_end_params & params, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
+    cmd_context(front_end_params * params = 0, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
     ~cmd_context(); 
-    bool is_smtlib2_compliant() const { return m_params.m_smtlib2_compliant; }
+    bool is_smtlib2_compliant() const { return params().m_smtlib2_compliant; }
     void set_logic(symbol const & s);
     bool has_logic() const { return m_logic != symbol::null; }
     symbol const & get_logic() const { return m_logic; }
@@ -268,8 +269,8 @@ public:
     void set_global_decls(bool flag) { SASSERT(!has_manager()); m_global_decls = flag; }
     unsigned random_seed() const { return m_random_seed; }
     void set_random_seed(unsigned s) { m_random_seed = s; }
-    bool produce_models() const { return m_params.m_model; }
-    bool produce_proofs() const { return m_params.m_proof_mode != PGM_DISABLED; }
+    bool produce_models() const { return params().m_model; }
+    bool produce_proofs() const { return params().m_proof_mode != PGM_DISABLED; }
     bool produce_unsat_cores() const { return m_produce_unsat_cores; }
     void set_produce_unsat_cores(bool flag) { m_produce_unsat_cores = flag; }
     bool produce_assignments() const { return m_produce_assignments; }
@@ -283,7 +284,7 @@ public:
     virtual ast_manager & get_ast_manager() { return m(); }
     pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
     sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
-    front_end_params & params() const { return m_params; }
+    front_end_params & params() const { return *m_params; }
  
     void set_solver(solver * s);
     solver * get_solver() const { return m_solver.get(); }
diff --git a/src/muz_qe/datalog_parser.cpp b/src/muz_qe/datalog_parser.cpp
index 160337a35..f527bb25a 100644
--- a/src/muz_qe/datalog_parser.cpp
+++ b/src/muz_qe/datalog_parser.cpp
@@ -1382,12 +1382,12 @@ private:
             uint64_set & sort_content = *sit->m_value;
             //the +1 is for a zero element which happens to appear in the problem files
             uint64 domain_size = sort_content.size()+1;
-            sort * s;
+            // sort * s;
             if(!m_use_map_names) {
-                s = register_finite_sort(sort_name, domain_size, context::SK_UINT64);
+                /* s = */ register_finite_sort(sort_name, domain_size, context::SK_UINT64);
             }
             else {
-                s = register_finite_sort(sort_name, domain_size, context::SK_SYMBOL);
+                /* s = */ register_finite_sort(sort_name, domain_size, context::SK_SYMBOL);
             }
 
             /*
diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp
index 793fdd9db..8e0e3b9b7 100644
--- a/src/muz_qe/dl_bmc_engine.cpp
+++ b/src/muz_qe/dl_bmc_engine.cpp
@@ -34,12 +34,12 @@ namespace datalog {
     bmc::bmc(context& ctx): 
         m_ctx(ctx), 
         m(ctx.get_manager()), 
-        m_cancel(false), 
         m_solver(m, m_fparams),
         m_pinned(m),
         m_rules(ctx),
         m_query_pred(m),
         m_answer(m),
+        m_cancel(false), 
         m_path_sort(m),
         m_bv(m) {
         }
@@ -794,7 +794,7 @@ namespace datalog {
             sort* pred_sort = m_pred2sort.find(p);
             path_var  = m.mk_var(0, m_path_sort);
             trace_var = m.mk_var(1, pred_sort);            
-            sort* sorts[2] = { pred_sort, m_path_sort };
+            // sort* sorts[2] = { pred_sort, m_path_sort };
             ptr_vector<func_decl> const& cnstrs = *dtu.get_datatype_constructors(pred_sort);
             ptr_vector<func_decl> const& succs  = *dtu.get_datatype_constructors(m_path_sort);
             SASSERT(cnstrs.size() == rls.size());
@@ -966,10 +966,10 @@ namespace datalog {
         datalog::rule_vector const& rules = m_rules.get_predicate_rules(p);
         ptr_vector<func_decl> const& cnstrs = *dtu.get_datatype_constructors(trace_sort);
         ptr_vector<func_decl> const& succs  = *dtu.get_datatype_constructors(m_path_sort);
-        bool found = false;
+        // bool found = false;
         for (unsigned i = 0; i < cnstrs.size(); ++i) {
             if (trace->get_decl() == cnstrs[i]) {
-                found = true;
+                // found = true;
                 svector<std::pair<unsigned, unsigned> > positions;
                 scoped_coarse_proof _sc(m);
                 proof_ref_vector prs(m);
diff --git a/src/muz_qe/dl_bound_relation.cpp b/src/muz_qe/dl_bound_relation.cpp
index ec8551600..0c76e8e1e 100644
--- a/src/muz_qe/dl_bound_relation.cpp
+++ b/src/muz_qe/dl_bound_relation.cpp
@@ -395,12 +395,10 @@ namespace datalog {
         uint_set::iterator it = t.lt.begin(), end = t.lt.end();
         unsigned_vector ltv, lev;
         for (; it != end; ++it) {
-            unsigned elem = *it;
             ltv.push_back(renaming[*it]);
         }
         it = t.le.begin(), end = t.le.end();
         for (; it != end; ++it) {
-            unsigned elem = *it;
             lev.push_back(renaming[*it]);
         }
         TRACE("dl", 
diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp
index c8947d78e..92f5cfc89 100644
--- a/src/muz_qe/dl_cmds.cpp
+++ b/src/muz_qe/dl_cmds.cpp
@@ -228,7 +228,6 @@ public:
 private:
     void set_background(cmd_context& ctx) {
         datalog::context& dlctx = m_dl_ctx->get_dl_context();
-        ast_manager& m = ctx.m();                
         ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
         ptr_vector<expr>::const_iterator end = ctx.end_assertions();
         for (; it != end; ++it) {
diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp
index 2d677ed7f..99c7b86f5 100644
--- a/src/muz_qe/dl_compiler.cpp
+++ b/src/muz_qe/dl_compiler.cpp
@@ -168,7 +168,6 @@ namespace datalog {
         
         TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
             IF_VERBOSE(3, { 
-                    relation_manager& rm = m_context.get_rmanager(); 
                     expr_ref e(m_context.get_manager()); 
                     compiled_rule->to_formula(e); 
                     verbose_stream() << "Compiling unsafe rule column " << col_idx << "\n" 
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index bf25e0277..ae7bc360d 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -457,19 +457,18 @@ namespace datalog {
                 /*}*/
             }
             SASSERT(!rel_kinds.empty());
-            relation_plugin * rel_plugin; //the aggregate kind of non-table plugins
-            relation_signature rel_sig;
+            // relation_plugin * rel_plugin; //the aggregate kind of non-table plugins
             family_id rel_kind; //the aggregate kind of non-table plugins
             if (rel_kinds.size()==1) {
                 rel_kind = rel_kinds[0];
-                rel_plugin = rel_plugins[0];
+                // rel_plugin = rel_plugins[0];
             }
             else {
                 relation_signature rel_sig;
                 //rmgr.from_predicate(pred, rel_sig);
                 product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
                 rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
-                rel_plugin = &prod_plugin;
+                // rel_plugin = &prod_plugin;
             }
             if (tr_plugin==0) {
                 target_kind = rel_kind;
@@ -532,7 +531,6 @@ namespace datalog {
         rule_ref r(rules[0].get(), rm);
         get_rmanager().reset_saturated_marks();
         rule_ref_vector const& rls = m_rule_set.get_rules();
-        bool found = false;
         rule* old_rule = 0;
         for (unsigned i = 0; i < rls.size(); ++i) {
             if (rls[i]->name() == name) {
@@ -757,6 +755,9 @@ namespace datalog {
             check_existential_tail(r);
             check_positive_predicates(r);
             break;            
+        default:
+            UNREACHABLE();
+            break;
         }
     }
 
@@ -1550,6 +1551,8 @@ namespace datalog {
         }
     }
     
+#if 0
+    // [Leo] dead code?
     static func_decl* get_head_relation(ast_manager& m, expr* fml) {
         while (is_quantifier(fml)) {
             fml = to_quantifier(fml)->get_expr();            
@@ -1563,6 +1566,7 @@ namespace datalog {
             return 0;
         }
     }
+#endif
 
     void context::display_smt2(
         unsigned num_queries, 
@@ -1694,7 +1698,7 @@ namespace datalog {
                 max_vars.insert(s, max_var);
 
                 // index into fresh variable array.
-                unsigned fresh_var_idx = 0;
+                // unsigned fresh_var_idx = 0;
                 obj_map<sort, unsigned_vector>::obj_map_entry* e = var_idxs.insert_if_not_there2(s, unsigned_vector());
                 unsigned_vector& vars = e->get_data().m_value;
                 if (max_var >= vars.size()) {
diff --git a/src/muz_qe/dl_finite_product_relation.cpp b/src/muz_qe/dl_finite_product_relation.cpp
index 80dcfc54b..3ab3da45d 100644
--- a/src/muz_qe/dl_finite_product_relation.cpp
+++ b/src/muz_qe/dl_finite_product_relation.cpp
@@ -1001,6 +1001,9 @@ namespace datalog {
             }
         };
 
+        // [Leo]: gcc complained about the following class.
+        // It does not have a constructor and uses a reference
+#if 0
         class inner_relation_copier : public table_row_mutator_fn {
             finite_product_relation & m_tgt;
             const finite_product_relation & m_src;
@@ -1023,6 +1026,7 @@ namespace datalog {
                 return true;
             }
         };
+#endif
 
         scoped_ptr<table_union_fn> m_t_union_fun;
         offset_row_mapper * m_offset_mapper_obj; //initialized together with m_offset_mapper_fun, and deallocated by it
diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp
index 82df6dc40..9c503360c 100644
--- a/src/muz_qe/dl_mk_bit_blast.cpp
+++ b/src/muz_qe/dl_mk_bit_blast.cpp
@@ -130,7 +130,7 @@ namespace datalog {
 
     class mk_bit_blast::impl {
 
-        context &	         m_context;
+        context &	     m_context;
         ast_manager &        m;
         params_ref           m_params;
         rule_ref_vector      m_rules;
@@ -161,8 +161,8 @@ namespace datalog {
         impl(context& ctx):
             m_context(ctx),
             m(ctx.get_manager()),
-            m_rules(ctx.get_rule_manager()),
             m_params(ctx.get_params()),
+            m_rules(ctx.get_rule_manager()),
             m_blaster(ctx.get_manager(), m_params),
             m_rewriter(ctx.get_manager(), ctx, m_rules) {
             m_params.set_bool(":blast-full", true);
diff --git a/src/muz_qe/dl_mk_coalesce.cpp b/src/muz_qe/dl_mk_coalesce.cpp
index a19b2853c..cd825b7c7 100644
--- a/src/muz_qe/dl_mk_coalesce.cpp
+++ b/src/muz_qe/dl_mk_coalesce.cpp
@@ -179,9 +179,9 @@ namespace datalog {
         }
         rule_set* rules = alloc(rule_set, m_ctx);
         rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules();
-        bool change = false;
+        // bool change = false;
         for (; it != end; ++it) {
-            func_decl* p = it->m_key;
+            // func_decl* p = it->m_key;
             rule_ref_vector d_rules(rm);
             d_rules.append(it->m_value->size(), it->m_value->c_ptr());
             for (unsigned i = 0; i < d_rules.size(); ++i) {
@@ -191,7 +191,7 @@ namespace datalog {
                         merge_rules(r1, *d_rules[j].get());
                         d_rules[j] = d_rules.back();
                         d_rules.pop_back();
-                        change = true;
+                        // change = true;
                         --j;
                     }
                 }
diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz_qe/dl_mk_rule_inliner.h
index b93e51435..1be7ef059 100644
--- a/src/muz_qe/dl_mk_rule_inliner.h
+++ b/src/muz_qe/dl_mk_rule_inliner.h
@@ -179,9 +179,9 @@ namespace datalog {
             m_simp(m_context.get_rewriter()),
             m_pinned(m_rm),
             m_inlined_rules(m_context),
-            m_unifier(ctx),
             m_mc(0),
             m_pc(0),
+            m_unifier(ctx),
             m_head_index(m),
             m_tail_index(m),
             m_subst(m),
diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp
index 77d53cf4e..cfe168629 100644
--- a/src/muz_qe/dl_mk_slice.cpp
+++ b/src/muz_qe/dl_mk_slice.cpp
@@ -205,8 +205,8 @@ namespace datalog {
             expr* fact0   = m.get_fact(p0);
             TRACE("dl", tout << "fact0: " << mk_pp(fact0, m) << "\n";);
             rule* orig0    = m_sliceform2rule.find(fact0);
-            rule* slice0   = m_rule2slice.find(orig0);
-            unsigned_vector const& renaming0 = m_renaming.find(orig0);
+            /* rule* slice0   = */ m_rule2slice.find(orig0);
+            /* unsigned_vector const& renaming0 = */ m_renaming.find(orig0);
             premises.push_back(p0_new);
             rule_ref r1(rm), r2(rm), r3(rm);
             r1 = orig0;
@@ -217,8 +217,8 @@ namespace datalog {
                 expr* fact1   = m.get_fact(p1);
                 TRACE("dl", tout << "fact1: " << mk_pp(fact1, m) << "\n";);
                 rule* orig1     = m_sliceform2rule.find(fact1);
-                rule* slice1    = m_rule2slice.find(orig1);
-                unsigned_vector const& renaming1 = m_renaming.find(orig1); //TBD
+                /* rule* slice1    = */ m_rule2slice.find(orig1);
+                /* unsigned_vector const& renaming1 = */ m_renaming.find(orig1); //TBD
                 premises.push_back(p1_new);
 
                 // TODO: work with substitutions.
diff --git a/src/muz_qe/dl_table.cpp b/src/muz_qe/dl_table.cpp
index 1f2ba3abc..99a868bea 100644
--- a/src/muz_qe/dl_table.cpp
+++ b/src/muz_qe/dl_table.cpp
@@ -567,10 +567,10 @@ namespace datalog {
     public:
         eq_iterator(const equivalence_table& eq, bool end):
             m_eq(eq), 
-            m_row_obj(*this),
             m_last(eq.m_uf.get_num_vars()),
             m_current(end?m_last:0),
-            m_next(0)
+            m_next(0),
+            m_row_obj(*this)
         { 
             while (m_current < m_last && !m_eq.is_valid(m_current)) {
                 m_current++;
diff --git a/src/muz_qe/dl_util.cpp b/src/muz_qe/dl_util.cpp
index 4b48a1687..b1c5e129c 100644
--- a/src/muz_qe/dl_util.cpp
+++ b/src/muz_qe/dl_util.cpp
@@ -594,7 +594,7 @@ namespace datalog {
 
     void del_rule(horn_subsume_model_converter* mc, rule& r) {
         if (mc) {
-            app* head = r.get_head();
+            // app* head = r.get_head();
             ast_manager& m = mc->get_manager();
             expr_ref_vector body(m);
             for (unsigned i = 0; i < r.get_tail_size(); ++i) {
diff --git a/src/muz_qe/dl_vector_relation.h b/src/muz_qe/dl_vector_relation.h
index a3795aa22..114f4ca43 100644
--- a/src/muz_qe/dl_vector_relation.h
+++ b/src/muz_qe/dl_vector_relation.h
@@ -209,7 +209,6 @@ namespace datalog {
 
         void mk_project(vector_relation const& r, unsigned col_cnt, unsigned const* removed_cols) {
             SASSERT(is_full());
-            unsigned j = 0, k = 0;
             unsigned_vector classRep, repNode;
             unsigned result_size = get_signature().size();
             unsigned input_size = r.get_signature().size();
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 7d7438f7b..27e0f7e6a 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -57,7 +57,8 @@ namespace pdr {
     // pred_tansformer
 
     pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): 
-        ctx(ctx), pm(pm), m(pm.get_manager()), m_head(head, m), 
+        pm(pm), m(pm.get_manager()),
+        ctx(ctx), m_head(head, m), 
         m_sig(m), m_solver(pm, head->get_name()),
         m_invariants(m), m_transition(m), m_initial_state(m), 
         m_reachable(pm, pm.get_params()) {}
@@ -196,7 +197,6 @@ namespace pdr {
         tactic_ref us = mk_unit_subsumption_tactic(m);
         simplify_formulas(*us, m_invariants);
         for (unsigned i = 0; i < m_levels.size(); ++i) {
-            expr_ref_vector& v = m_levels[i];
             simplify_formulas(*us, m_levels[i]);
         }             
     }
diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp
index 69f0995f0..045411fb1 100644
--- a/src/muz_qe/pdr_dl_interface.cpp
+++ b/src/muz_qe/pdr_dl_interface.cpp
@@ -80,7 +80,6 @@ lbool dl_interface::query(expr * query) {
     m_pdr_rules.reset();
     m_ctx.get_rmanager().reset_relations();
     ast_manager& m =                      m_ctx.get_manager();
-    datalog::relation_manager& rm =       m_ctx.get_rmanager();
     datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
     datalog::rule_set        old_rules(m_ctx.get_rules());
     func_decl_ref            query_pred(m);
diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp
index dc73148b2..e0d584f09 100644
--- a/src/muz_qe/pdr_generalizers.cpp
+++ b/src/muz_qe/pdr_generalizers.cpp
@@ -38,7 +38,7 @@ namespace pdr {
             return;
         }
         ast_manager& m = core.get_manager();
-        TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; } "\n";);
+        TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; });
         unsigned num_failures = 0, i = 0, old_core_size = core.size();
         ptr_vector<expr> processed;
 
@@ -109,7 +109,6 @@ namespace pdr {
     {}
     
     void core_farkas_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
-        front_end_params& p = m_ctx.get_fparams();
         ast_manager& m  = n.pt().get_manager();
         manager& pm = n.pt().get_pdr_manager();
         if (core.empty()) return;
diff --git a/src/muz_qe/pdr_interpolant_provider.cpp b/src/muz_qe/pdr_interpolant_provider.cpp
index 6c0dd3c6b..a243ed899 100644
--- a/src/muz_qe/pdr_interpolant_provider.cpp
+++ b/src/muz_qe/pdr_interpolant_provider.cpp
@@ -20,7 +20,9 @@ Revision History:
 --*/
 
 //disables the warning on deprecation of fgets function -- didn't really find by what it should be replaced
+#ifdef _WINDOWS
 #pragma warning(disable: 4995)
+#endif
 
 #include <sstream>
 #include "ast_smt_pp.h"
diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz_qe/pdr_smt_context_manager.cpp
index 062607f2a..ec813f606 100644
--- a/src/muz_qe/pdr_smt_context_manager.cpp
+++ b/src/muz_qe/pdr_smt_context_manager.cpp
@@ -26,8 +26,8 @@ Revision History:
 namespace pdr {
 
     smt_context::smt_context(smt_context_manager& p, ast_manager& m, app* pred):
-        m_parent(p),
         m_pred(pred, m),
+        m_parent(p),
         m_in_delay_scope(false),
         m_pushed(false)
     {}
@@ -94,8 +94,12 @@ namespace pdr {
     }
 
     smt_context_manager::smt_context_manager(front_end_params& fp, params_ref const& p, ast_manager& m):
-        m_fparams(fp), m_max_num_contexts(p.get_uint(":max-num-contexts", 500)), 
-        m(m), m_num_contexts(0), m_predicate_list(m) {}
+        m_fparams(fp), 
+        m(m), 
+        m_max_num_contexts(p.get_uint(":max-num-contexts", 500)), 
+        m_num_contexts(0), 
+        m_predicate_list(m) {
+    }
     
     
     smt_context_manager::~smt_context_manager() {
diff --git a/src/muz_qe/qe.cpp b/src/muz_qe/qe.cpp
index e678fbb3e..08b737609 100644
--- a/src/muz_qe/qe.cpp
+++ b/src/muz_qe/qe.cpp
@@ -856,8 +856,8 @@ namespace qe {
     public:
         nnf_normalizer(ast_manager& m, i_expr_pred& is_relevant, i_nnf_atom& mk_atom):
             m_nnf_core(m, is_relevant),
-            m_normalize_literals(m, is_relevant, mk_atom),
-            m_collect_atoms(m, is_relevant)
+            m_collect_atoms(m, is_relevant),
+            m_normalize_literals(m, is_relevant, mk_atom)
         {}
 
         void operator()(expr_ref& fml, atom_set& pos, atom_set& neg) {
@@ -1767,7 +1767,7 @@ namespace qe {
 
         void propagate_assignment(model_evaluator& model_eval) {
             if (m_fml) {
-                update_status st = update_current(model_eval, true);
+                /* update_status st = */ update_current(model_eval, true);
             }
         }
 
@@ -2551,7 +2551,7 @@ namespace qe {
             ) 
         {
             
-            bool is_forall = old_q->is_forall();
+            // bool is_forall = old_q->is_forall();
             app_ref_vector vars(m);
             TRACE("qe", tout << "simplifying" << mk_pp(new_body, m) << "\n";);
             result = new_body;
diff --git a/src/muz_qe/qe_arith_plugin.cpp b/src/muz_qe/qe_arith_plugin.cpp
index f8fe967c0..c10716dc8 100644
--- a/src/muz_qe/qe_arith_plugin.cpp
+++ b/src/muz_qe/qe_arith_plugin.cpp
@@ -110,11 +110,10 @@ namespace qe {
             m_minus_one_i(m_arith.mk_numeral(numeral(-1), true), m),
             m_zero_r(m_arith.mk_numeral(numeral(0), false), m),
             m_one_r(m_arith.mk_numeral(numeral(1), false), m),
+            m_tmp(m), 
             m_replace(mk_default_expr_replacer(m)),
             m_bool_rewriter(m),
-            m_arith_rewriter(m),
-            m_tmp(m)
-        {
+            m_arith_rewriter(m) {
         }
 
         ast_manager& get_manager() { return m; }
@@ -1817,7 +1816,6 @@ public:
             }
             --v;
             is_strict = e_size <= v;
-            bool is_eq = false;
             
             SASSERT(v < t_size + e_size);
             if (is_strict) {
@@ -1826,7 +1824,6 @@ public:
             }
             else if (m_util.is_real(x)) {
                 SASSERT(0 == (e_size & 0x1));
-                is_eq = (0 == (v & 0x1));
                 v  /= 2;
                 e_size /= 2;
             }
@@ -1896,7 +1893,6 @@ public:
             bounds_proc& bounds = get_bounds(x.x(), fml);
             bool is_lower   = bounds.le_size() + bounds.lt_size() < bounds.ge_size() + bounds.gt_size();
             unsigned e_size = bounds.e_size(is_lower);
-            unsigned t_size = bounds.t_size(is_lower);
             numeral bound1, bound2, vl, x_val;
             unsigned idx1, idx2;
             bool found1 = find_min_max(is_lower, false, bounds, model_eval, bound1, idx1);
diff --git a/src/muz_qe/qe_sat_tactic.cpp b/src/muz_qe/qe_sat_tactic.cpp
index 8cf5e5d58..e5a57871a 100644
--- a/src/muz_qe/qe_sat_tactic.cpp
+++ b/src/muz_qe/qe_sat_tactic.cpp
@@ -213,12 +213,12 @@ namespace qe {
             m_projection_mode_param(true),
             m_strong_context_simplify_param(true),
             m_ctx_simplify_local_param(false),
+            m_solver(m, m_fparams),
             m_fml(m),
             m_Ms(m),
             m_assignments(m),
             m_rewriter(m),
-            m_ctx_rewriter(m_fparams, m),
-            m_solver(m, m_fparams) {            
+            m_ctx_rewriter(m_fparams, m) {            
             m_fparams.m_model = true;
         }
 
diff --git a/src/parsers/smt/smtlib_solver.cpp b/src/parsers/smt/smtlib_solver.cpp
index 1aff13a3d..77c2455dc 100644
--- a/src/parsers/smt/smtlib_solver.cpp
+++ b/src/parsers/smt/smtlib_solver.cpp
@@ -82,7 +82,7 @@ namespace smtlib {
             // Hack: it seems SMT-LIB allow benchmarks without any :formula
             benchmark.add_formula(m_ast_manager.mk_true());
         }
-        m_ctx = alloc(cmd_context, m_params, true, &m_ast_manager, benchmark.get_logic());
+        m_ctx = alloc(cmd_context, &m_params, true, &m_ast_manager, benchmark.get_logic());
         m_ctx->set_solver(mk_smt_strategic_solver(*m_ctx));
         theory::expr_iterator fit  = benchmark.begin_formulas();
         theory::expr_iterator fend = benchmark.end_formulas();
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index a19474ceb..822590867 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -107,6 +107,8 @@ public:
         m_statistics(g_display_statistics) {
     }
 
+    virtual ~extra_params() {}
+
     virtual void register_params(ini_params & p) {
         datalog_params::register_params(p);
         p.register_bool_param("STATISTICS", m_statistics, "display statistics");
diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp
index 1b1299971..dd8987529 100644
--- a/src/shell/smtlib_frontend.cpp
+++ b/src/shell/smtlib_frontend.cpp
@@ -97,7 +97,7 @@ unsigned read_smtlib2_commands(char const* file_name, front_end_params& front_en
     g_start_time = clock();
     register_on_timeout_proc(on_timeout);
     signal(SIGINT, on_ctrl_c);
-    cmd_context ctx(front_end_params);
+    cmd_context ctx(&front_end_params);
 
     // temporary hack until strategic_solver is ported to new tactic framework
     if (front_end_params.m_nlsat) {
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index f7d75be8c..2c7d32cf7 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -675,7 +675,7 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
     inc_conflicts();
     literal_vector const& lits = m_nc_functor.get_lits();
     context & ctx = get_context();
-    region& r = ctx.get_region();
+    // region& r = ctx.get_region();
     TRACE("arith_conflict", 
           //display(tout);
           tout << "conflict: ";
diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp
index bfb23fd12..77ff50e9b 100644
--- a/src/tactic/fpa/fpa2bv_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_converter.cpp
@@ -1562,7 +1562,7 @@ void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref &
         L = m_bv_util.mk_extract(bv_sz/2-1, 0, e);
 
         unsigned H_size = m_bv_util.get_bv_size(H);
-        unsigned L_size = m_bv_util.get_bv_size(L);
+        // unsigned L_size = m_bv_util.get_bv_size(L);
 
         expr_ref lzH(m), lzL(m);
         mk_leading_zeros(H, max_bits, lzH); /* recursive! */
@@ -2109,4 +2109,4 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
 	}
 
     fu.fm().del(fp_val);
-}
\ No newline at end of file
+}
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index 6765ef4cb..1b95cb1ed 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -910,12 +910,13 @@ class sls_tactic : public tactic {
 
             void randomize_local(goal_ref const & g) {
                 ptr_vector<func_decl> & unsat_constants = get_unsat_constants(g);
-                bool did_something = false;
+                // bool did_something = false;
                 for (unsigned i = 0; i < unsat_constants.size(); i++) {
                     func_decl * fd = unsat_constants[i];
                     mpz temp = get_random(fd->get_range());
-                    if (m_mpz_manager.neq(temp, get_value(fd)))
-                        did_something = true;
+                    if (m_mpz_manager.neq(temp, get_value(fd))) {
+                        // did_something = true;
+                    }
                     update(fd, temp);
                     m_mpz_manager.del(temp);
                 }
diff --git a/src/tactic/smt/ctx_solver_simplify_tactic.cpp b/src/tactic/smt/ctx_solver_simplify_tactic.cpp
index 1faf73f19..76379e595 100644
--- a/src/tactic/smt/ctx_solver_simplify_tactic.cpp
+++ b/src/tactic/smt/ctx_solver_simplify_tactic.cpp
@@ -84,11 +84,9 @@ protected:
 
     void reduce(goal& g) {
         SASSERT(g.is_well_sorted());
-        bool proofs_enabled = g.proofs_enabled();
         m_num_steps = 0;
         expr_ref fml(m);
         tactic_report report("ctx-solver-simplify", g);
-        unsigned sz = g.size();
         if (g.inconsistent())
             return;
         ptr_vector<expr> fmls;
diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp
index 11e58ee69..3872a3a2e 100644
--- a/src/tactic/ufbv/macro_finder_tactic.cpp
+++ b/src/tactic/ufbv/macro_finder_tactic.cpp
@@ -33,7 +33,10 @@ class macro_finder_tactic : public tactic {
         bool m_cancel;
         bool m_elim_and;
 
-        imp(ast_manager & m, params_ref const & p) : m_manager(m),m_elim_and(false),m_cancel(false) {
+        imp(ast_manager & m, params_ref const & p) : 
+            m_manager(m),
+            m_cancel(false),
+            m_elim_and(false) {
             updt_params(p);
         }
         
@@ -54,7 +57,6 @@ class macro_finder_tactic : public tactic {
             fail_if_unsat_core_generation("macro-finder", g);
 
             bool produce_proofs = g->proofs_enabled();
-            bool produce_models = g->models_enabled();
 
             simplifier simp(m_manager);
             basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp
index 8d8c7cae0..d7e55379a 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.cpp
+++ b/src/tactic/ufbv/quasi_macros_tactic.cpp
@@ -54,7 +54,6 @@ class quasi_macros_tactic : public tactic {
             fail_if_unsat_core_generation("quasi-macros", g);
 
             bool produce_proofs = g->proofs_enabled();
-            bool produce_models = g->models_enabled();
             
             simplifier simp(m_manager);
             basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
index 010ffab28..0705c627c 100644
--- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp
@@ -49,7 +49,6 @@ class ufbv_rewriter_tactic : public tactic {
             fail_if_unsat_core_generation("ufbv-rewriter", g);
 
             bool produce_proofs = g->proofs_enabled();
-            bool produce_models = g->models_enabled();
             
             basic_simplifier_plugin bsimp(m_manager);
             bsimp.set_eliminate_and(true);
diff --git a/src/test/bv_simplifier_plugin.cpp b/src/test/bv_simplifier_plugin.cpp
index 271d1a534..4a472425e 100644
--- a/src/test/bv_simplifier_plugin.cpp
+++ b/src/test/bv_simplifier_plugin.cpp
@@ -75,10 +75,10 @@ class tst_bv_simplifier_plugin_cls {
 public:
 
     tst_bv_simplifier_plugin_cls() : 
-        m_bv_util(m_manager), 
         m_bsimp(m_manager),
         m_arith(m_manager),
         m_simp(m_manager, m_bsimp, m_bv_params), 
+        m_bv_util(m_manager), 
         m_fid(m_manager.get_family_id("bv")) {
         reg_decl_plugins(m_manager);
     }
@@ -88,7 +88,6 @@ public:
     void test_num(unsigned a) {
         expr_ref e(m_manager), e1(m_manager);
         app_ref ar(m_manager);
-        int sa = static_cast<int>(a);
         uint64 a64 = static_cast<uint64>(a);
 
         e1 = m_bv_util.mk_numeral(rational(a), 32);
diff --git a/src/test/check_assumptions.cpp b/src/test/check_assumptions.cpp
index 033e3fdc9..e6a5433e9 100644
--- a/src/test/check_assumptions.cpp
+++ b/src/test/check_assumptions.cpp
@@ -39,6 +39,6 @@ void tst_check_assumptions()
 
     expr * assumpt[] = { nq.get(), nr.get() };
     //here it should crash
-    lbool res2 = ctx.check(2, assumpt);
+    ctx.check(2, assumpt);
 }
 
diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp
index 3ac9095a5..b2530b9da 100644
--- a/src/test/dl_context.cpp
+++ b/src/test/dl_context.cpp
@@ -31,7 +31,7 @@ static void dl_context_simple_query_test(params_ref & params) {
     context ctx(m, fparams);
     ctx.updt_params(params);
 
-    lbool status = dl_context_eval_unary_predicate(m, ctx, "Z 64\n\nP(x:Z)\nP(\"a\").", "P");
+    /* lbool status = */ dl_context_eval_unary_predicate(m, ctx, "Z 64\n\nP(x:Z)\nP(\"a\").", "P");
 
 #if 0
     // TBD:
diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp
index 469797bf0..2cca7cce6 100644
--- a/src/test/dl_query.cpp
+++ b/src/test/dl_query.cpp
@@ -48,7 +48,6 @@ void dl_query_test(ast_manager & m, front_end_params & fparams, params_ref& para
         bool use_magic_sets) {
 
     dl_decl_util decl_util(m);
-    relation_manager & rel_mgr_b = ctx_b.get_rmanager();
 
     context ctx_q(m, fparams);
     params.set_bool(":magic-sets-for-queries", use_magic_sets);
diff --git a/src/test/dl_smt_relation.cpp b/src/test/dl_smt_relation.cpp
index a809af4ca..fa66a89c9 100644
--- a/src/test/dl_smt_relation.cpp
+++ b/src/test/dl_smt_relation.cpp
@@ -179,8 +179,8 @@ namespace datalog {
         Z3_ast ffx = Z3_mk_app(ctx, cons_decl, 2, zero_fx);
         Z3_ast xy[2] = { x, y };
         Z3_ast zy[2] = { z, y };
-        Z3_ast ffxy[2] = { ffx, y };
-        Z3_ast fxy[2] = { fx, y };
+        // Z3_ast ffxy[2] = { ffx, y };
+        // Z3_ast fxy[2] = { fx, y };
         Z3_ast zero_nil[2] = { zero, Z3_mk_app(ctx, nil_decl, 0, 0) };
         Z3_ast f0 = Z3_mk_app(ctx, cons_decl, 2, zero_nil);
         Z3_ast zero_f0[2] = { zero, f0 };
diff --git a/src/test/get_implied_equalities.cpp b/src/test/get_implied_equalities.cpp
index 223689bbd..91c71438f 100644
--- a/src/test/get_implied_equalities.cpp
+++ b/src/test/get_implied_equalities.cpp
@@ -73,18 +73,15 @@ static void tst_get_implied_equalities2() {
     Z3_context ctx = Z3_mk_context(cfg);
     Z3_del_config(cfg);
     Z3_sort int_ty = Z3_mk_int_sort(ctx);
-	Z3_sort a_ty = Z3_mk_array_sort(ctx, int_ty, int_ty);	
     Z3_ast a = mk_int_var(ctx,"a");
     Z3_ast b = mk_int_var(ctx,"b");
-    Z3_ast c = mk_int_var(ctx,"c");
-    Z3_ast d = mk_int_var(ctx,"d");
-	Z3_ast one = Z3_mk_numeral(ctx, "1", int_ty);
-	Z3_ast two = Z3_mk_numeral(ctx, "2", int_ty);
-	Z3_ast x = Z3_mk_const_array(ctx, int_ty, one);
-	Z3_ast y = Z3_mk_store(ctx, x, one, a);
-	Z3_ast z = Z3_mk_store(ctx, y, two , b);
-	Z3_ast u = Z3_mk_store(ctx, x, two , b);
-	Z3_ast v = Z3_mk_store(ctx, u, one , a);
+    Z3_ast one = Z3_mk_numeral(ctx, "1", int_ty);
+    Z3_ast two = Z3_mk_numeral(ctx, "2", int_ty);
+    Z3_ast x = Z3_mk_const_array(ctx, int_ty, one);
+    Z3_ast y = Z3_mk_store(ctx, x, one, a);
+    Z3_ast z = Z3_mk_store(ctx, y, two , b);
+    Z3_ast u = Z3_mk_store(ctx, x, two , b);
+    Z3_ast v = Z3_mk_store(ctx, u, one , a);
     unsigned const num_terms = 5;
     unsigned i;
     Z3_ast terms[5] = { x, y, z, u, v};
diff --git a/src/test/hwf.cpp b/src/test/hwf.cpp
index 9c940f1d9..be32b5400 100644
--- a/src/test/hwf.cpp
+++ b/src/test/hwf.cpp
@@ -92,16 +92,16 @@ static void bug_to_rational() {
     m.to_rational(a, r);
     ad = m.to_double(a);
     rd = mq.get_double(r);
-    double diff = (ad-rd);
 #ifdef _WINDOWS    
     // CMW: This one depends on the rounding mode,
     // which is implicit in both hwf::set and in mpq::to_double.
+    double diff = (ad-rd);
     SASSERT(diff >= -DBL_EPSILON && diff <= DBL_EPSILON);
 #endif
 }
 
 static void bug_is_int() {
-    unsigned raw_val[2] = { 2147483648, 1077720461 };
+    unsigned raw_val[2] = { 2147483648u, 1077720461u };
     double   val = *(double*)(raw_val);
     std::cout << val << "\n";
     hwf_manager m;
diff --git a/src/test/inf_rational.cpp b/src/test/inf_rational.cpp
index cb025a789..1b0a293ce 100644
--- a/src/test/inf_rational.cpp
+++ b/src/test/inf_rational.cpp
@@ -167,8 +167,6 @@ tst_inf_rational()
     SASSERT(ceil(inf_rational(rational(1))) == rational(1));
     SASSERT(ceil(inf_rational(rational(1),true)) == rational(2));
 
-    unsigned h = r9.hash();
-
     inf_rational x(rational(1,2),true);
     inf_rational y(1,2);
     x.swap(y);
diff --git a/src/test/interval.cpp b/src/test/interval.cpp
index 4621c0416..ef733394b 100644
--- a/src/test/interval.cpp
+++ b/src/test/interval.cpp
@@ -91,6 +91,7 @@ static void assert_conj(std::ostream & out, unsynch_mpq_manager & m, char const
     out << "))\n";
 }
 
+#if 0
 static bool mk_interval(im_default_config & cfg, interval & a, bool l_inf, bool l_open, int l_val, bool u_inf, bool u_open, int u_val) {
     if (!l_inf && !u_inf) {
         if (l_val > u_val)
@@ -121,6 +122,7 @@ static bool mk_interval(im_default_config & cfg, interval & a, bool l_inf, bool
     
     return true;
 }
+#endif
 
 static void mk_random_interval(im_default_config & cfg, interval & a, unsigned magnitude) {
     switch (rand()%3) {
@@ -381,6 +383,7 @@ static void tst_div(unsigned N, unsigned magnitude) {
 
 #include"im_float_config.h"
 
+#if 0
 static void tst_float() {
     unsynch_mpq_manager   qm;
     mpf_manager           fm;
@@ -414,6 +417,7 @@ static void tst_float() {
 
     del_f_interval(ifc, a); del_f_interval(ifc, b); del_f_interval(ifc, c);
 }
+#endif
 
 void tst_pi() {
     unsynch_mpq_manager                 nm;     
@@ -429,6 +433,7 @@ void tst_pi() {
     del_interval(imc, r);
 }
 
+#if 0
 static void tst_pi_float() {
     std::cout << "pi float...\n";
     unsynch_mpq_manager   qm;
@@ -446,6 +451,7 @@ static void tst_pi_float() {
     }
     del_f_interval(ifc, r);
 }
+#endif 
 
 #define NUM_TESTS 1000
 #define SMALL_MAG 3
diff --git a/src/test/model_retrieval.cpp b/src/test/model_retrieval.cpp
index 2fa1cb24f..0a0b8a0dc 100644
--- a/src/test/model_retrieval.cpp
+++ b/src/test/model_retrieval.cpp
@@ -20,9 +20,7 @@ void tst_model_retrieval()
 
     family_id array_fid = m.get_family_id(symbol("array"));
     array_util au(m);
-    array_decl_plugin& ad = *static_cast<array_decl_plugin *>(m.get_plugin(array_fid));
-
-
+    
     // arr_s and select_fn creation copy-pasted from z3.cpp
 
     parameter sparams[2]  = { parameter(to_sort(m.mk_bool_sort())), parameter(to_sort(m.mk_bool_sort())) };
diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp
index 4b811689e..35afcccf3 100644
--- a/src/test/mpff.cpp
+++ b/src/test/mpff.cpp
@@ -113,7 +113,7 @@ static void tst7() {
     m.display_smt2(std::cout, a); std::cout << "\n";
 }
 
-//  if (!qm.le(qa, qt)) { TRACE("mpff_bug", tout << fa << "\n" << qa << "\n" << qt << "\n";); UNREACHABLE(); } \
+//  if (!qm.le(qa, qt)) { TRACE("mpff_bug", tout << fa << "\n" << qa << "\n" << qt << "\n";); UNREACHABLE(); }
 
 
 #define MK_BIN_OP(OP)                                                   \
@@ -533,10 +533,12 @@ static void tst_limits(unsigned prec) {
     SASSERT(!m.is_minus_epsilon(a));
 }
 
+#if 0
 static void tst_add_corner(unsigned prec) {
     mpff_manager m(prec);
     scoped_mpff a(m), b(m);
 }
+#endif
 
 static void tst_decimal(int64 n, uint64 d, bool to_plus_inf, unsigned prec, char const * expected, unsigned decimal_places = UINT_MAX) {
     mpff_manager m(prec);
diff --git a/src/test/mpq.cpp b/src/test/mpq.cpp
index 5c221d617..68c7d8bb3 100644
--- a/src/test/mpq.cpp
+++ b/src/test/mpq.cpp
@@ -55,6 +55,7 @@ static void tst1() {
     m.del(v3);
 }
 
+#if 0
 static void mk_random_num_str(unsigned buffer_sz, char * buffer) {
     unsigned div_pos;
     unsigned sz = (rand() % (buffer_sz-2)) + 1;
@@ -80,6 +81,7 @@ static void mk_random_num_str(unsigned buffer_sz, char * buffer) {
     }
     buffer[sz-1] = 0;
 }
+#endif
 
 static void bug1() {
     synch_mpq_manager m;
diff --git a/src/test/mpz.cpp b/src/test/mpz.cpp
index 70b49f5a7..d7944ae95 100644
--- a/src/test/mpz.cpp
+++ b/src/test/mpz.cpp
@@ -77,6 +77,7 @@ static void tst2b() {
     m.del(v3);
 }
 
+#if 0
 static void mk_random_num_str(unsigned buffer_sz, char * buffer) {
     unsigned sz = (rand() % (buffer_sz-2)) + 1;
     SASSERT(sz < buffer_sz);
@@ -87,6 +88,7 @@ static void mk_random_num_str(unsigned buffer_sz, char * buffer) {
         buffer[0] = '-';
     buffer[sz-1] = 0;
 }
+#endif
 
 static void bug1() {
     synch_mpz_manager m;
diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp
index aa79df99e..e53378dcc 100644
--- a/src/test/nlsat.cpp
+++ b/src/test/nlsat.cpp
@@ -268,7 +268,6 @@ static void tst4() {
 static void tst5() {
     params_ref      ps;
     nlsat::solver s(ps);
-    unsynch_mpq_manager & qm = s.qm();
     anum_manager & am = s.am();
     nlsat::pmanager & pm = s.pm();
     nlsat::assignment           as(am);
diff --git a/src/test/object_allocator.cpp b/src/test/object_allocator.cpp
index caac3aa93..16b9331e2 100644
--- a/src/test/object_allocator.cpp
+++ b/src/test/object_allocator.cpp
@@ -55,7 +55,7 @@ static void tst1() {
     cell_allocator m;
     
     cell * c1 = m.allocate<true>();
-    cell * c2 = m.allocate<true>();
+    /* cell * c2 = */ m.allocate<true>();
 
     c1->m_coeff = rational(10);
     m.recycle(c1);
diff --git a/src/test/parray.cpp b/src/test/parray.cpp
index 77e8dc15d..7976971d8 100644
--- a/src/test/parray.cpp
+++ b/src/test/parray.cpp
@@ -112,10 +112,10 @@ static void tst2() {
           m.display_info(tout, a1); tout << "\n";
           m.display_info(tout, a2); tout << "\n";);
     for (unsigned i = 0; i < m.size(a1); i++) {
-        SASSERT(m.get(a1, i) == i);
+        SASSERT(static_cast<unsigned>(m.get(a1, i)) == i);
     }
     for (unsigned i = 0; i < m.size(a2); i++) {
-        SASSERT(m.get(a2, i) == i);
+        SASSERT(static_cast<unsigned>(m.get(a2, i)) == i);
     }
     TRACE("parray", 
           m.display_info(tout, a1); tout << "\n";
@@ -161,7 +161,7 @@ static void tst3() {
     m.push_back(a4, 30);
     
     for (unsigned i = 0; i < 20; i++) {
-        SASSERT(m.get(a2, i) == i+1);
+        SASSERT(static_cast<unsigned>(m.get(a2, i)) == i+1);
     }
     TRACE("parray", 
           m.display_info(tout, a1); tout << "\n";
@@ -182,11 +182,11 @@ static void tst3() {
     SASSERT(m.size(a3) == 19);
     SASSERT(m.size(a4) == 19);
     for (unsigned i = 0; i < 20; i++) {
-        SASSERT(m.get(a1, i) == i);
-        SASSERT(m.get(a2, i) == i+1);
-        SASSERT(i >= 18 || m.get(a4, i) == i+1);
-        SASSERT(i >= 6 || m.get(a3, i) == i+1);
-        SASSERT(!(6 <= i && i <= 17) || m.get(a3, i) == i);
+        SASSERT(static_cast<unsigned>(m.get(a1, i)) == i);
+        SASSERT(static_cast<unsigned>(m.get(a2, i)) == i+1);
+        SASSERT(i >= 18 || static_cast<unsigned>(m.get(a4, i)) == i+1);
+        SASSERT(i >= 6 ||  static_cast<unsigned>(m.get(a3, i)) == i+1);
+        SASSERT(!(6 <= i && i <= 17) || static_cast<unsigned>(m.get(a3, i)) == i);
     }
     SASSERT(m.get(a4, 18) == 30);
     SASSERT(m.get(a3, 18) == 40);
diff --git a/src/test/polynomial.cpp b/src/test/polynomial.cpp
index d5e20edd2..beb53c0fc 100644
--- a/src/test/polynomial.cpp
+++ b/src/test/polynomial.cpp
@@ -704,6 +704,7 @@ static void tst_psc(polynomial_ref const & p, polynomial_ref const & q, polynomi
     }
 }
 
+#if 0
 static void tst_psc_perf(polynomial_ref const & p, polynomial_ref const & q, polynomial::var x) {
     polynomial::manager & m = p.m();
     polynomial_ref_vector S(m);
@@ -716,6 +717,7 @@ static void tst_psc_perf(polynomial_ref const & p, polynomial_ref const & q, pol
         std::cout << "S_" << i << ": " << m.size(S.get(i)) << std::endl; // polynomial_ref(S.get(i), m) << std::endl;
     }
 }
+#endif
 
 static void tst_psc() {
     polynomial::numeral_manager nm;
@@ -747,9 +749,6 @@ static void tst_psc() {
     polynomial_ref & d = x3;
     polynomial_ref & e = x4;
     polynomial_ref & f = x5;
-    polynomial_ref & g = x6;
-    polynomial_ref & h = x7;
-    polynomial_ref & i = x8;
     polynomial_ref & x = x9;
     tst_psc((x^4) + a*(x^2) + b*x + c, 4*(x^3) + 2*a*x + b, 9,
             16*(a^4)*c - 4*(a^3)*(b^2) - 128*(a^2)*(c^2) + 144*a*(b^2)*c - 27*(b^4) + 256*(c^3), 8*(a^3) - 32*a*c + 36*(b^2));
@@ -1261,6 +1260,7 @@ static void tst_translate() {
                   );
 }
 
+#if 0
 static void tst_p25() {
     unsynch_mpq_manager qm;
     polynomial::manager m(qm);
@@ -1282,6 +1282,7 @@ static void tst_p25() {
     p = (x0 + x1 + x2 + x3 + x4 + x5 + x6)^25;
     std::cout << "size(p): " << size(p) << "\n";
 }
+#endif
 
 static void tst_mm() {
     unsynch_mpq_manager qm;
@@ -1574,6 +1575,7 @@ static void tst_gcd2() {
     tst_gcd(p, p_prime, x1^4);
 }
 
+#if 0
 static void tst_gcd3() {
     enable_trace("polynomial_gcd");
     enable_trace("polynomial_gcd_detail");
@@ -1623,6 +1625,7 @@ static void tst_gcd4() {
         (1000000*x + 1)*(333333333*x + 1)*(77777777*x + 1)*(11111111*x + 1)*(x + 128384747)*(x + 82837437)*(x + 22848481);
     tst_gcd(p, derivative(p, 0), (x + 3)^9);
 }
+#endif 
 
 static void tst_newton_interpolation() {
     // enable_trace("newton");
diff --git a/src/test/polynomial_factorization.cpp b/src/test/polynomial_factorization.cpp
index c8dda5313..06c67b9c2 100644
--- a/src/test/polynomial_factorization.cpp
+++ b/src/test/polynomial_factorization.cpp
@@ -172,6 +172,7 @@ int random_polynomial[20][2][11] = {
     }
 };
 
+#if 0
 static void tst_square_free_finite_1() {
     polynomial::numeral_manager nm;
     polynomial::manager pm(nm);
@@ -247,7 +248,7 @@ static void tst_factor_finite_1() {
         
         // factor it
         upolynomial::zp_factors factors(upm);        
-        bool factorized = upolynomial::zp_factor(upm, K_u, factors);
+        /* bool factorized = */ upolynomial::zp_factor(upm, K_u, factors);
     
         // check the result
         unsigned distinct = factors.distinct_factors();
@@ -383,8 +384,8 @@ static void tst_factor_finite_3() {
             cout << "Got " << factors << endl;
             cout << "Thats " << distinct << " distinct factors, " << total << " total" << endl;
 
-            SASSERT(random_polynomial[random_i][0][prime_i] == distinct);
-            SASSERT(random_polynomial[random_i][1][prime_i] == total);
+            // SASSERT(random_polynomial[random_i][0][prime_i] == distinct);
+            // SASSERT(random_polynomial[random_i][1][prime_i] == total);
             
             upolynomial::numeral_vector multiplied;
             factors.multiply(multiplied);
@@ -548,7 +549,7 @@ static void tst_factor_square_free_univariate_1(unsigned max_length) {
             cout << "factoring "; upm.display(cout, f_u); cout << endl;
             cout << "expecting " << length << " factors ";
             upolynomial::factors factors(upm);
-            bool ok = upolynomial::factor_square_free(upm, f_u, factors);        
+            /* bool ok = */ upolynomial::factor_square_free(upm, f_u, factors); 
             cout << "got " << factors << endl;
             
             SASSERT(factors.distinct_factors() == length);
@@ -616,6 +617,7 @@ static void tst_factor_square_free_univariate_3() {
         
     upm.reset(deg70_u);
 }
+#endif
 
 void tst_factor_swinnerton_dyer_big(unsigned max) {
     polynomial::numeral_manager nm;
diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp
index 16fc3bcfd..fe3454336 100644
--- a/src/test/quant_solve.cpp
+++ b/src/test/quant_solve.cpp
@@ -44,6 +44,7 @@ static void validate_quant_solution(ast_manager& m, expr* fml, expr* guard, qe::
 }
 
 
+#if 0
 static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards) {
     return;
     // quant_elim option got removed...
@@ -73,7 +74,7 @@ static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards)
         fatal_error(0);
     }
 }
-
+#endif
 
 
 static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml) {
@@ -97,7 +98,7 @@ static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr*
 static expr_ref parse_fml(ast_manager& m, char const* str) {
     expr_ref result(m);
     front_end_params fp;
-    cmd_context ctx(fp, false, &m);
+    cmd_context ctx(&fp, false, &m);
     ctx.set_ignore_check(true);
     std::ostringstream buffer;
     buffer << "(declare-const x Int)\n"
diff --git a/src/test/trigo.cpp b/src/test/trigo.cpp
index 66805ed45..da26d0f39 100644
--- a/src/test/trigo.cpp
+++ b/src/test/trigo.cpp
@@ -116,6 +116,7 @@ static void tst_float_sine(std::ostream & out, unsigned N, unsigned k) {
    }
 }
 
+#if 0
 static void tst_mpf_bug() {
     mpf_manager fm;
     scoped_mpf a(fm), b(fm), c(fm);
@@ -126,6 +127,7 @@ static void tst_mpf_bug() {
     fm.mul(MPF_ROUND_TOWARD_NEGATIVE, a, b, c);
     std::cout << "c: " << fm.to_double(c) << "\n";
 }
+#endif
 
 static void tst_e(std::ostream & out) {
     unsynch_mpq_manager                 nm;     
diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp
index 80bc8f278..b38c3af34 100644
--- a/src/test/upolynomial.cpp
+++ b/src/test/upolynomial.cpp
@@ -726,6 +726,7 @@ static void tst_sturm2() {
     um.display(std::cout, seq2);
 }
 
+#if 0
 static void tst_isolate_roots2() {
     polynomial::numeral_manager nm;
     polynomial::manager m(nm);
@@ -793,6 +794,7 @@ static void tst_gcd2() {
     }
     um.display(std::cout, _p_sqf.size(), _p_sqf.c_ptr()); std::cout << "\n";
 }
+#endif 
 
 static void tst_isolate_roots5() {
     polynomial::numeral_manager nm;
diff --git a/src/test/vector.cpp b/src/test/vector.cpp
index 5ae62e150..0a3904954 100644
--- a/src/test/vector.cpp
+++ b/src/test/vector.cpp
@@ -23,12 +23,12 @@ static void tst1() {
     SASSERT(v1.empty());
     for (unsigned i = 0; i < 1000; i++) {
         v1.push_back(i + 3);
-        SASSERT(v1[i] == i + 3);
+        SASSERT(static_cast<unsigned>(v1[i]) == i + 3);
         SASSERT(v1.capacity() >= v1.size());
         SASSERT(!v1.empty());
     }
     for (unsigned i = 0; i < 1000; i++) {
-        SASSERT(v1[i] == i + 3);
+        SASSERT(static_cast<unsigned>(v1[i]) == i + 3);
     }
     vector<int>::iterator it = v1.begin();
     vector<int>::iterator end = v1.end();
@@ -36,7 +36,7 @@ static void tst1() {
         SASSERT(*it == i + 3);
     }
     for (unsigned i = 0; i < 1000; i++) {
-        SASSERT(v1.back() == 1000 - i - 1 + 3);
+        SASSERT(static_cast<unsigned>(v1.back()) == 1000 - i - 1 + 3);
         SASSERT(v1.size() == 1000 - i);
         v1.pop_back();
     }
diff --git a/src/util/debug.h b/src/util/debug.h
index ec904aa4e..ab9fdd57b 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -68,7 +68,11 @@ bool is_debug_enabled(const char * tag);
 #define MAKE_NAME2(LINE) zofty_ ## LINE 
 #define MAKE_NAME(LINE) MAKE_NAME2(LINE)
 #define DBG_UNIQUE_NAME MAKE_NAME(__LINE__)
+#ifdef __GNUC__
+#define COMPILE_TIME_ASSERT(expr) extern __attribute__((unused)) char DBG_UNIQUE_NAME[expr]
+#else
 #define COMPILE_TIME_ASSERT(expr) extern char DBG_UNIQUE_NAME[expr]
+#endif
 
 template<class T>
 class class_invariant 
diff --git a/src/util/diff_logic.h b/src/util/diff_logic.h
index d616edf57..b4b22029f 100644
--- a/src/util/diff_logic.h
+++ b/src/util/diff_logic.h
@@ -1041,7 +1041,7 @@ private:
         for (unsigned i = 0; i < edges.size(); ++i) {
             
             potential0 += m_edges[edges[i]].get_weight();
-            numeral potential1 = potentials[i];
+            // numeral potential1 = potentials[i];
             if (potential0 != potentials[i] || 
                 nodes[i] != m_edges[edges[i]].get_source()) {
                 TRACE("diff_logic_traverse", tout << "checking index " << i << " ";
diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp
index c54f51040..219172b34 100644
--- a/src/util/hwf.cpp
+++ b/src/util/hwf.cpp
@@ -24,7 +24,9 @@ Revision History:
 #pragma fp_contract(off)              // contractions off (`contraction' means x*y+z is turned into a fused-mul-add).
 #pragma fenv_access(on)               // fpu environment sensitivity (needed to be allowed to make FPU mode changes).
 #else
+#ifdef _WINDOWS
 #pragma STDC FENV_ACCESS ON
+#endif
 #include <math.h>
 #include <fenv.h>
 #endif
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 16a3f1a9e..c77978647 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -1713,18 +1713,6 @@ void mpz_manager<SYNCH>::machine_div2k(mpz & a, unsigned k) {
 #endif    
 }
 
-#ifndef _MP_GMP
-static void display_bits(std::ostream & out, digit_t a) {
-    for (unsigned i = 0; i < sizeof(digit_t) * 8; i++) {
-        if (a % 2 == 0)
-            out << "0";
-        else
-            out << "1";
-        a /= 2;
-    }
-}
-#endif
-
 template<bool SYNCH>
 void mpz_manager<SYNCH>::mul2k(mpz & a, unsigned k) {
     if (k == 0 || is_zero(a))
diff --git a/src/util/warning.cpp b/src/util/warning.cpp
index dd4ca04d4..4ab54f203 100644
--- a/src/util/warning.cpp
+++ b/src/util/warning.cpp
@@ -91,6 +91,8 @@ void disable_error_msg_prefix() {
     g_show_error_msg_prefix = false;
 }
 
+#if 0
+// [Leo]: Do we need this?
 static void string2ostream(std::ostream& out, char const* msg) {
     svector<char>  buff;
     buff.resize(10);
@@ -104,6 +106,7 @@ static void string2ostream(std::ostream& out, char const* msg) {
     END_ERR_HANDLER();
     out << buff.c_ptr();
 }
+#endif
 
 void format2ostream(std::ostream & out, char const* msg, va_list args) {
     svector<char>  buff;
@@ -147,14 +150,14 @@ void format2ostream(std::ostream & out, char const* msg, va_list args) {
 
 void print_msg(std::ostream * out, const char* prefix, const char* msg, va_list args) {
     if (out) {
-        string2ostream(*out, prefix);
+        *out << prefix;
         format2ostream(*out, msg, args);
-        string2ostream(*out, "\n");
+        *out << "\n";
         out->flush();
     }
     else {
         FILE * f = g_use_std_stdout ? stdout : stderr;
-        fprintf(f, prefix);
+        fprintf(f, "%s", prefix);
         vfprintf(f, msg, args);
         fprintf(f, "\n");
         fflush(f);