Fix warnings and enable -Wnon-virtual-dtor warning (#2079)

This commit fixes warnings for an unused variable, comparison of two
different types and add virtual destructors to classes that were
previously missing them. It also enables the -Wnon-virtual-dtor warning
which warns about any class definition with virtual methods that does
not have a virtual destructor (except if the destructor is protected).
This flag is supported by both clang and GCC and not enabled by default.

4 files changed, 5 insertions, 3 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 856219b73..6330bbd30 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -42,7 +42,7 @@ class Cegis : public SygusModule
 {
  public:
   Cegis(QuantifiersEngine* qe, CegConjecture* p);
-  ~Cegis() {}
+  ~Cegis() override {}
   /** initialize */
   virtual bool initialize(Node n,
                           const std::vector<Node>& candidates,
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index ec338a8b2..c0f860975 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -200,7 +200,7 @@ class CegisUnif : public Cegis
 {
  public:
   CegisUnif(QuantifiersEngine* qe, CegConjecture* p);
-  ~CegisUnif();
+  ~CegisUnif() override;
   /** Retrieves enumerators for constructing solutions
    *
    * Non-unification candidates have themselves as enumerators, while for
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index b01f8e1d0..fb2821e20 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -49,7 +49,7 @@ class SygusModule
 {
  public:
   SygusModule(QuantifiersEngine* qe, CegConjecture* p);
-  ~SygusModule() {}
+  virtual ~SygusModule() {}
   /** initialize
    *
    * n is the "base instantiation" of the deep-embedding version of the
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index cbce5e70c..db0ff4afb 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -93,6 +93,8 @@ std::ostream& operator<<(std::ostream& os, StrategyType st);
 class UnifContext
 {
  public:
+  virtual ~UnifContext() {}
+
   /** Get the current role
    *
    * In a particular context when constructing solutions in synthesis by