4 files changed, 12 insertions, 6 deletions
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index 10ef6ab4c..59dc543ae 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -37,7 +37,7 @@ class BvInverterQuery
 {
  public:
   BvInverterQuery() {}
-  ~BvInverterQuery() {}
+  virtual ~BvInverterQuery() {}
   /** returns the current model value of n */
   virtual Node getModelValue(Node n) = 0;
   /** returns a bound variable of type tn */
diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index a0137abde..03983fe1a 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.h
@@ -52,6 +52,8 @@ class InstantiatorPreprocess;
 class TermProperties {
 public:
   TermProperties() : d_type(0) {}
+  virtual ~TermProperties() {}
+
   // type of property for a term
   //  for arithmetic this corresponds to bound type (0:equal, 1:upper bound, -1:lower bound)
   int d_type;
diff --git a/src/theory/quantifiers/sygus_invariance.h b/src/theory/quantifiers/sygus_invariance.h
index bf3c56572..1cc43fb7d 100644
--- a/src/theory/quantifiers/sygus_invariance.h
+++ b/src/theory/quantifiers/sygus_invariance.h
@@ -43,6 +43,8 @@ class CegConjecture;
 class SygusInvarianceTest
 {
  public:
+  virtual ~SygusInvarianceTest(){}
+
   /** Is nvn invariant with respect to this test ?
    *
    * - nvn is the term to check whether it is invariant.
@@ -96,7 +98,7 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest
 {
  public:
   EvalSygusInvarianceTest() {}
-  ~EvalSygusInvarianceTest() {}
+
   /** initialize this invariance test
     * This sets d_conj/d_var/d_result, where
     * we are checking whether:
@@ -156,7 +158,7 @@ class EquivSygusInvarianceTest : public SygusInvarianceTest
 {
  public:
   EquivSygusInvarianceTest() : d_conj(nullptr) {}
-  ~EquivSygusInvarianceTest() {}
+
   /** initialize this invariance test
    * tn is the sygus type for e
    * aconj/e are used for conjecture-specific symmetry breaking
@@ -197,7 +199,7 @@ class DivByZeroSygusInvarianceTest : public SygusInvarianceTest
 {
  public:
   DivByZeroSygusInvarianceTest() {}
-  ~DivByZeroSygusInvarianceTest() {}
+
  protected:
   /** checks whether nvn involves division by zero. */
   bool invariant(TermDbSygus* tds, Node nvn, Node x);
@@ -233,7 +235,7 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest
 {
  public:
   NegContainsSygusInvarianceTest() : d_conj(nullptr) {}
-  ~NegContainsSygusInvarianceTest() {}
+
   /** initialize this invariance test
    *  cpbe is the conjecture utility.
    *  e is the enumerator which we are reasoning about (associated with a synth
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index d8f2244c7..8ed4bc783 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -31,6 +31,7 @@ namespace quantifiers {
 class LazyTrieEvaluator
 {
  public:
+  virtual ~LazyTrieEvaluator() {}
   virtual Node evaluate(Node n, unsigned index) = 0;
 };
 
@@ -134,7 +135,8 @@ class SygusSampler : public LazyTrieEvaluator
 {
  public:
   SygusSampler();
-  virtual ~SygusSampler() {}
+  ~SygusSampler() override {}
+
   /** initialize
    *
    * tn : the return type of terms we will be testing with this class