test/regress/regress0/seq/array/update-word-eq.smt2

   1 ; COMMAND-LINE: --strings-exp --seq-array=eager
   2 (set-logic QF_SLIA)
   3 (set-info :status unsat)
   4
   5 (declare-fun x () (Seq Int))
   6 (declare-fun y () (Seq Int))
   7 (declare-fun z () (Seq Int))
   8 (declare-fun a () Int)
   9 (declare-fun b () Int)
  10 (declare-fun i () Int)
  11
  12 (assert (= (seq.++ (seq.unit a) z) (seq.update x 0 (seq.unit b))))
  13 (assert (not (= a b)))
  14
  15 (check-sat)