diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-09-25 15:16:41 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-09-25 15:16:41 +0000 |
| commit | 89bcd4deee07a2c61d30a9dfca64e58e8c2d701b (patch) | |
| tree | d60e9264731c73a88a3947a06dea6ff294ff0f80 /src/theory/quantifiers_engine.h | |
| parent | 86df00c36c6cbabac53001082219c3fc8c0fa297 (diff) | |
some buggy examples for incrementality, and make bug326 run as part of make regress, because the bug was fixed.
Also make QuantifiersModule's destructor virtual (it has virtual members).
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index befd12d9d..c374f18ba 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -94,7 +94,7 @@ protected: QuantifiersEngine* d_quantEngine; public: QuantifiersModule( QuantifiersEngine* qe ) : d_quantEngine( qe ){} - ~QuantifiersModule(){} + virtual ~QuantifiersModule(){} //get quantifiers engine QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } /* Call during check registerQuantifier has already been called */ |