From 96c6ec71ccdde72c6cbc850df94c8965cda8d7db Mon Sep 17 00:00:00 2001 From: yoni206 Date: Mon, 19 Oct 2020 17:44:12 -0700 Subject: Expand `seq.nth` lazily (#5287) Our first support for seq.nth eliminated it eagerly during expandDefinitions. This PR changes that, by eliminating it lazily, as done with other extended string operators. --- test/regress/regress0/seq/seq-nth-undef-unsat.smt2 | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 test/regress/regress0/seq/seq-nth-undef-unsat.smt2 (limited to 'test/regress/regress0/seq/seq-nth-undef-unsat.smt2') diff --git a/test/regress/regress0/seq/seq-nth-undef-unsat.smt2 b/test/regress/regress0/seq/seq-nth-undef-unsat.smt2 new file mode 100644 index 000000000..4fe2a85a9 --- /dev/null +++ b/test/regress/regress0/seq/seq-nth-undef-unsat.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --strings-exp -q +;EXPECT: unsat +(set-logic ALL) +(declare-fun s () (Seq Int)) +(declare-fun n () Int) + +(assert (=> (and (<= 0 n ) (< n (seq.len s))) (= (seq.nth s n) 6))) +(assert (=> (>= 0 n) (= (seq.nth s n) 7))) +(assert (=> (>= n (seq.len s)) (= (seq.nth s n) 8))) +(assert (distinct (seq.unit 6) (seq.extract s n 1))) +(assert (distinct (seq.unit 7) (seq.extract s n 1))) +(assert (distinct (seq.unit 8) (seq.extract s n 1))) +(assert (> n 0)) +(assert (< n (seq.len s))) +(assert (> (seq.len s) 0)) +(check-sat) + -- cgit v1.2.3