summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 199fe79b9..2b466b96b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -290,7 +290,7 @@ public:
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
/** add term to database */
- void addTermToDatabase( Node n, bool withinQuant = false );
+ void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
/** get the master equality engine */
eq::EqualityEngine* getMasterEqualityEngine() ;
/** debug print equality engine */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback