summaryrefslogtreecommitdiff
path: root/test/regress/regress1/strings/issue4379.smt2
blob: c5d024bc22be499c18be6d639d1cef2b9f786a6f (plain) 
1
2
3
4
5
6
7
8
9

; COMMAND-LINE: --strings-exp
; EXPECT: sat
(set-logic QF_SLIA)
(set-info :status sat)
(declare-const i7 Int)
(declare-const Str8 String)
(declare-const Str17 String)
(assert (distinct (str.++ "" "rvhhcn" "" Str8 (int.to.str 56)) (str.++ "" (int.to.str i7) "" Str17) Str17))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback