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.h3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index a4e95487c..af0b87bd8 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -73,8 +73,7 @@ class TermDb : public QuantifiersUtil {
using NodeDbListMap = context::CDHashMap<Node, std::shared_ptr<DbList>>;
public:
- TermDb(QuantifiersState& qs,
- QuantifiersRegistry& qr);
+ TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr);
virtual ~TermDb();
/** Finish init, which sets the inference manager */
void finishInit(QuantifiersInferenceManager* qim);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback