test/regress/regress1/strings/strings-leq-trans-unsat.smt2

   1 ; COMMAND-LINE: --strings-exp
   2 ; EXPECT: unsat
   3 (set-logic QF_SLIA)
   4 (set-info :status unsat)
   5 (declare-fun x () String)
   6 (declare-fun y () String)
   7 (declare-fun z () String)
   8 (declare-fun w () String)
   9 (assert (str.<= x y))
  10 (assert (str.<= y w))
  11 (declare-fun xp () String)
  12 (assert (= x (str.++ "G" xp)))
  13 (assert (= w "E"))
  14 (check-sat)