summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r--src/theory/quantifiers/term_database.h6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index de766cc2a..e440e68e9 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -141,11 +141,11 @@ class TermDb : public QuantifiersUtil {
/** presolve (called once per user check-sat) */
void presolve();
/** reset (calculate which terms are active) */
- virtual bool reset(Theory::Effort effort) override;
+ bool reset(Theory::Effort effort) override;
/** register quantified formula */
- virtual void registerQuantifier(Node q) override;
+ void registerQuantifier(Node q) override;
/** identify */
- virtual std::string identify() const override { return "TermDb"; }
+ std::string identify() const override { return "TermDb"; }
/** get number of operators */
unsigned getNumOperators();
/** get operator at index i */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback