From 6c43b80514259ee489eba99405f703765b613404 Mon Sep 17 00:00:00 2001
From: Tim King <taking@google.com>
Date: Thu, 29 Dec 2016 14:36:00 -0800
Subject: [PATCH] Adding a destructor to InstantiationNotify.

---
 src/theory/quantifiers_engine.h | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 83076c51a..150b3945b 100644
--- 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;
 };
-- 
2.30.2