diff options
| -rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 7 |
2 files changed, 6 insertions, 3 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 ) { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3e8201144..42677fa3f 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -166,8 +166,11 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) Node TermDb::getMatchOperator( Node n ) { Kind k = n.getKind(); //datatype operators may be parametric, always assume they are - if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || - k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO || k==HO_APPLY ){ + if (k == SELECT || k == STORE || k == UNION || k == INTERSECTION + || k == SUBSET || k == SETMINUS || k == MEMBER || k == SINGLETON + || k == APPLY_SELECTOR_TOTAL || k == APPLY_TESTER || k == SEP_PTO + || k == HO_APPLY || k == SEQ_NTH) + { //since it is parametric, use a particular one as op TypeNode tn = n[0].getType(); Node op = n.getOperator(); |