diff --git a/src/math/interval/mod_interval.h b/src/math/interval/mod_interval.h
index 0e3554a9b..aa790b8b1 100644
--- a/src/math/interval/mod_interval.h
+++ b/src/math/interval/mod_interval.h
@@ -42,6 +42,7 @@ template<typename Numeral>
 class mod_interval {
     bool emp { false };
 public:
+    virtual ~mod_interval() {}
     Numeral lo { 0 };
     Numeral hi { 0 };
     mod_interval() {}
@@ -65,6 +66,7 @@ public:
     void intersect_ugt(Numeral const& l);
     void intersect_fixed(Numeral const& n);
     void intersect_diff(Numeral const& n);
+
     mod_interval operator&(mod_interval const& other) const;
     mod_interval operator+(mod_interval const& other) const;
     mod_interval operator-(mod_interval const& other) const;
diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h
index 8ca9a239b..45ce69ba6 100644
--- a/src/math/polysat/fixplex.h
+++ b/src/math/polysat/fixplex.h
@@ -97,6 +97,7 @@ namespace polysat {
                 m_base2row(0),
                 m_is_base(false)
             {}
+            ~var_info() override {}
             var_info& operator&=(mod_interval<numeral> const& range) {
                 mod_interval<numeral>::operator=(range & *this);
                 return *this;
diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h
index 4c3e90ed1..479379de5 100644
--- a/src/math/polysat/viable.h
+++ b/src/math/polysat/viable.h
@@ -48,6 +48,7 @@ namespace polysat {
         bool narrow(std::function<bool(rational const&)>& eval);
     public:
         viable_set(unsigned num_bits): m_num_bits(num_bits) {}
+        ~viable_set() override {}
         dd::find_t find_hint(rational const& c, rational& val) const;
         bool intersect_eq(rational const& a, rational const& b, bool is_positive);
         bool intersect_le(rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive);