diff options
| -rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 2 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/seq/quant_len_trigger.smt2 | 13 |
3 files changed, 15 insertions, 1 deletions
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 654b1fd12..a111e0221 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -419,7 +419,7 @@ bool Trigger::isAtomicTriggerKind( Kind k ) { || 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 == SEQ_NTH; + || k == STRING_LENGTH || k == SEQ_NTH; } bool Trigger::isRelationalTrigger( Node n ) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 62978220a..509427d45 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -975,6 +975,7 @@ set(regress_0_tests regress0/seq/seq-nth.smt2 regress0/seq/seq-rewrites.smt2 regress0/seq/seq-types.smt2 + regress0/seq/quant_len_trigger.smt2 regress0/sets/abt-min.smt2 regress0/sets/abt-te-exh.smt2 regress0/sets/abt-te-exh2.smt2 diff --git a/test/regress/regress0/seq/quant_len_trigger.smt2 b/test/regress/regress0/seq/quant_len_trigger.smt2 new file mode 100644 index 000000000..08fdb4a43 --- /dev/null +++ b/test/regress/regress0/seq/quant_len_trigger.smt2 @@ -0,0 +1,13 @@ +; EXPECT: unsat + +(set-option :strings-exp true) +(set-logic ALL) + +(assert (forall ((x (Seq Int)) (xx (Seq Int)) ) (=> (and (= (seq.len x) (seq.len xx)) (forall ((i Int) ) (=> (and (<= 0 i) (< i (seq.len x))) (= (seq.nth x i) (seq.nth xx i))))) (= x xx)))) + +(declare-fun x () (Seq Int)) +(declare-fun y () (Seq Int)) + +(assert (not (=> (= (seq.len x) (seq.len y)) (=> (forall ((i Int) ) (=> (and (<= 0 i) (< i (seq.len x))) (= (seq.nth x i) (seq.nth y i)))) (= x y))))) + +(check-sat) |