diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-06 16:57:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-06 18:57:37 -0300 |
| commit | d0c3c164c9f722d4ea506706c5843373c8a948c4 (patch) | |
| tree | 81d307f524426ed01364c6c07ec69090570494c3 /src/theory | |
| parent | f28ed39a59e6ec8a282ef25b9415bc7d33cb919c (diff) | |
Discard duplicate terms in patterns (#6501)
Fixes #6495.
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()) { |