diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
index e80d98553..138ea6fb0 100644
--- a/src/api/api_seq.cpp
+++ b/src/api/api_seq.cpp
@@ -155,9 +155,9 @@ extern "C" {
     MK_UNARY(Z3_mk_re_plus, mk_c(c)->get_seq_fid(), OP_RE_PLUS, SKIP);
     MK_UNARY(Z3_mk_re_star, mk_c(c)->get_seq_fid(), OP_RE_STAR, SKIP);
     MK_UNARY(Z3_mk_re_option, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP);
-    MK_UNARY(Z3_mk_re_complement, mk_c(c)->get_seq_fid(), OP_RE_OPTION, SKIP);
+    MK_UNARY(Z3_mk_re_complement, mk_c(c)->get_seq_fid(), OP_RE_COMPLEMENT, SKIP);
     MK_NARY(Z3_mk_re_union, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP);
-    MK_NARY(Z3_mk_re_intersect, mk_c(c)->get_seq_fid(), OP_RE_UNION, SKIP);
+    MK_NARY(Z3_mk_re_intersect, mk_c(c)->get_seq_fid(), OP_RE_INTERSECT, SKIP);
     MK_NARY(Z3_mk_re_concat, mk_c(c)->get_seq_fid(), OP_RE_CONCAT, SKIP);
     MK_BINARY(Z3_mk_re_range, mk_c(c)->get_seq_fid(), OP_RE_RANGE, SKIP);
 
diff --git a/src/math/automata/boolean_algebra.h b/src/math/automata/boolean_algebra.h
index e3977b4cd..4f5527f5e 100644
--- a/src/math/automata/boolean_algebra.h
+++ b/src/math/automata/boolean_algebra.h
@@ -26,6 +26,7 @@ Revision History:
 template<class T>
 class positive_boolean_algebra {
 public:
+    virtual ~positive_boolean_algebra() {}
     virtual T mk_false() = 0;
     virtual T mk_true() = 0;
     virtual T mk_and(T x, T y) = 0;
@@ -38,6 +39,7 @@ public:
 template<class T>
 class boolean_algebra : public positive_boolean_algebra<T> {
 public:
+    virtual ~boolean_algebra() {}
     virtual T mk_not(T x) = 0;	
     //virtual lbool are_equivalent(T x, T y) = 0;
     //virtual T simplify(T x) = 0;    
diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp
index 27e096777..2d0199223 100644
--- a/src/math/subpaving/tactic/subpaving_tactic.cpp
+++ b/src/math/subpaving/tactic/subpaving_tactic.cpp
@@ -35,6 +35,8 @@ class subpaving_tactic : public tactic {
         display_var_proc(expr2var & e2v):m_inv(e2v.m()) {
             e2v.mk_inv(m_inv);
         }
+
+        virtual ~display_var_proc() {}
         
         ast_manager & m() const { return m_inv.get_manager(); }
         
diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp
index 950248698..8ff82af17 100644
--- a/src/tactic/arith/add_bounds_tactic.cpp
+++ b/src/tactic/arith/add_bounds_tactic.cpp
@@ -51,6 +51,7 @@ public:
     virtual result operator()(goal const & g) {
         return is_unbounded(g);
     }
+    virtual ~is_unbounded_probe() {}
 };
 
 probe * mk_is_unbounded_probe() {
@@ -109,11 +110,11 @@ class add_bounds_tactic : public tactic {
             void operator()(quantifier*) {}
         };
         
-        virtual void operator()(goal_ref const & g, 
-                                goal_ref_buffer & result, 
-                                model_converter_ref & mc, 
-                                proof_converter_ref & pc,
-                                expr_dependency_ref & core) {
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
             mc = 0; pc = 0; core = 0;
             tactic_report report("add-bounds", *g);
             bound_manager bm(m);
diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp
index 410185cf8..d63c2fcf4 100644
--- a/src/tactic/arith/diff_neq_tactic.cpp
+++ b/src/tactic/arith/diff_neq_tactic.cpp
@@ -312,11 +312,11 @@ class diff_neq_tactic : public tactic {
             return md;
         }
 
-        virtual void operator()(goal_ref const & g, 
-                                goal_ref_buffer & result, 
-                                model_converter_ref & mc, 
-                                proof_converter_ref & pc,
-                                expr_dependency_ref & core) {
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
             m_produce_models = g->models_enabled();
             mc = 0; pc = 0; core = 0; result.reset();
diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp
index 5c82bbbc3..6db0f5ad3 100644
--- a/src/tactic/arith/fm_tactic.cpp
+++ b/src/tactic/arith/fm_tactic.cpp
@@ -1549,11 +1549,11 @@ class fm_tactic : public tactic {
                 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
         }
         
-        virtual void operator()(goal_ref const & g, 
-                                goal_ref_buffer & result, 
-                                model_converter_ref & mc, 
-                                proof_converter_ref & pc,
-                                expr_dependency_ref & core) {
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
             mc = 0; pc = 0; core = 0;
             tactic_report report("fm", *g);
diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp
index 8d637bada..2b54dd463 100644
--- a/src/tactic/arith/lia2pb_tactic.cpp
+++ b/src/tactic/arith/lia2pb_tactic.cpp
@@ -188,11 +188,11 @@ class lia2pb_tactic : public tactic {
             return true;
         }
 
-        virtual void operator()(goal_ref const & g, 
-                                goal_ref_buffer & result, 
-                                model_converter_ref & mc, 
-                                proof_converter_ref & pc,
-                                expr_dependency_ref & core) {
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
             fail_if_proof_generation("lia2pb", g);
             m_produce_models      = g->models_enabled();
diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp
index b3ec505ea..06f1368a2 100644
--- a/src/tactic/arith/normalize_bounds_tactic.cpp
+++ b/src/tactic/arith/normalize_bounds_tactic.cpp
@@ -80,11 +80,11 @@ class normalize_bounds_tactic : public tactic {
             return false;
         }
         
-        virtual void operator()(goal_ref const & in, 
-                                goal_ref_buffer & result, 
-                                model_converter_ref & mc, 
-                                proof_converter_ref & pc,
-                                expr_dependency_ref & core) {
+        void operator()(goal_ref const & in, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
             mc = 0; pc = 0; core = 0;
             bool produce_models = in->models_enabled();
             bool produce_proofs = in->proofs_enabled();
diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp
index 6348ddd74..3931a1ea4 100644
--- a/src/tactic/arith/pb2bv_tactic.cpp
+++ b/src/tactic/arith/pb2bv_tactic.cpp
@@ -885,11 +885,11 @@ private:
             r.erase("elim_and");            
         }
         
-        virtual void operator()(goal_ref const & g, 
-                                goal_ref_buffer & result, 
-                                model_converter_ref & mc, 
-                                proof_converter_ref & pc,
-                                expr_dependency_ref & core) {
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
             TRACE("pb2bv", g->display(tout););
             SASSERT(g->is_well_sorted());
             fail_if_proof_generation("pb2bv", g);
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index 156f69388..df3b9f0f5 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -819,7 +819,7 @@ class elim_uncnstr_tactic : public tactic {
             m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps);            
         }
 
-        virtual void operator()(goal_ref const & g, 
+        void operator()(goal_ref const & g, 
                                 goal_ref_buffer & result, 
                                 model_converter_ref & mc, 
                                 proof_converter_ref & pc,