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


1
2
3
4
5
6
7
8
9
10
11
12
13
14

; COMMAND-LINE: --strings-exp
; EXPECT: unsat
(set-logic QF_SLIA)
(set-info :status unsat)
(declare-fun x () String)
(declare-fun y () String)
(declare-fun z () String)
(declare-fun w () String)
(assert (str.<= x y))
(assert (str.<= y w))
(declare-fun xp () String)
(assert (= x (str.++ "G" xp)))
(assert (= w "E"))
(check-sat)