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.

1 files changed, 17 insertions, 0 deletions

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)
+