test/regress/regress0/seq/seq-expand-defs.smt2

   1 ; COMMAND-LINE: --strings-exp -q
   2 ; EXPECT: sat
   3 ; EXPECT: (((seq.nth y 7) 404))
   4 ; EXPECT: (((str.from_code x) "?"))
   5 (set-logic ALL)
   6 (set-option :produce-models true)
   7 (declare-fun x () Int)
   8 (declare-fun y () (Seq Int))
   9
  10 (assert (< (seq.len y) 5))
  11
  12 (assert (= x 63))
  13
  14 (assert (= (seq.nth y 7) 404))
  15
  16 (check-sat)
  17
  18 (get-value ((seq.nth y 7)))
  19 (get-value ((str.from_code x)))