diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-20 11:58:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-20 11:58:37 -0500 |
| commit | 0e6e153a78843b134d943f5d1ec33e254d0fb2fe (patch) | |
| tree | 1c203b1d780b7a3592647960ba99333420d0258e /src/theory/quantifiers/ematching/trigger.cpp | |
| parent | 5e714e365dbbd51bbf04305867c4bcdc3d5a4d83 (diff) | |
Make seq.nth a trigger kind (#5314)
This makes seq.nth a trigger kind, analogous to select in arrays.
This fixes a timeout in seq-unsolved-ematch.smt2, fixing the nightlies.
Diffstat (limited to 'src/theory/quantifiers/ematching/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 545dab701..95ab0674f 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -408,7 +408,7 @@ bool Trigger::isAtomicTriggerKind( Kind k ) { || k == APPLY_SELECTOR_TOTAL || k == APPLY_TESTER || k == UNION || k == INTERSECTION || k == SUBSET || k == SETMINUS || k == MEMBER || k == SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT - || k == INT_TO_BITVECTOR || k == HO_APPLY; + || k == INT_TO_BITVECTOR || k == HO_APPLY || k == SEQ_NTH; } bool Trigger::isRelationalTrigger( Node n ) { |