summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/trigger.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/trigger.h')
-rw-r--r--src/theory/quantifiers/trigger.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 631627331..9ff82595f 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -142,7 +142,7 @@ private:
static Node getIsUsableEq( Node q, Node eq );
static bool isUsableEqTerms( Node q, Node n1, Node n2 );
/** collect all APPLY_UF pattern terms for f in n */
- static bool collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo,
+ static void collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, std::map< Node, TriggerTermInfo >& tinfo,
quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
bool pol, bool hasPol, bool epol, bool hasEPol );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback