; COMMAND-LINE: --strings-exp --no-check-models
(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((a 0)) (((b))))
(define-fun v () (Seq Bool) (as seq.empty (Seq Bool)))
(declare-fun e () (Seq a))
(define-fun w () Int (seq.len e))
(define-fun x () (Seq a) (seq.extract e 1 (- w 1)))
(define-fun i () (Seq a) (seq.extract x 1 (- (seq.len x) 1)))
(define-fun y () (Seq Bool) (ite (= 0 (seq.len i)) v (seq.unit true)))
(define-fun m () (Seq Bool) (seq.++ (seq.unit false) y))
(define-fun n () (Seq Bool) (ite (= 0 (seq.len x)) v m))
(define-fun o () (Seq Bool) (seq.++ (seq.unit false) n))
(define-fun p () (Seq Bool) (ite (= 0 w) v o))
(define-fun s () (Seq Bool) (seq.extract p 1 (- (seq.len p) 1)))
(define-fun u () (Seq Bool) (seq.extract s 1 (- (seq.len s) 1)))
(assert (not (seq.nth u 0)))
(check-sat)