test/regress/regress1/strings/seq-skeleton-gap.smt2

   1 ; COMMAND-LINE: --strings-exp --seq-array=lazy
   2 ; EXPECT: sat
   3 (set-logic ALL)
   4 (declare-fun a () (Seq Int))
   5 (assert (< 1 (seq.len (seq.update a 0 (seq.unit 1)))))
   6 (assert (distinct a (seq.update a 0 (seq.unit 1))))
   7 (check-sat)