summaryrefslogtreecommitdiff
path: root/test/regress/regress1/strings/issue5483-pp-leq.smt2
blob: 9e9900b2151f097499ec6084a97585a4baf0b3f0 (plain) 
1
2
3
4
5
6
7
8
9

; COMMAND-LINE: -i
; EXPECT: sat
(set-logic QF_SLIA)
(declare-fun _substvar_21_ () String)
(declare-fun _substvar_29_ () String)
(set-option :strings-lazy-pp false)
(assert (xor true true true true (str.<= _substvar_21_ _substvar_29_) true true))
(push 1)
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback