diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index 193ba250e..a937edf44 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -146,6 +146,11 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) std::vector<Node> nodes; for (const Node& p : pat) { + if (std::find(nodes.begin(), nodes.end(), p) != nodes.end()) + { + // skip duplicate pattern term + continue; + } Node pat_use = PatternTermSelector::getIsUsableTrigger(p, q); if (pat_use.isNull()) { |