Adding a destructor to InstantiationNotify.

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 83076c51a99cf311b24d87c5817e17aa979ccd85..150b3945bbe56ff26d402b6566f0f12685cde730 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -47,6 +47,7 @@ namespace quantifiers {
 class InstantiationNotify {
 public:
   InstantiationNotify(){}
+  virtual ~InstantiationNotify() {}
   virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
   virtual void filterInstantiations() = 0;
 };