test/regress/regress0/strings/issue4376.smt2


1
2
3
4
5
6
7
8
9
10
11

; COMMAND-LINE: --strings-exp --strings-eager
(set-info :status sat)
(set-logic QF_SLIA)
(declare-const i0 Int)
(declare-const Str1 String)
(declare-const Str9 String)
(declare-const Str11 String)
(declare-const Str15 String)
(assert (= (str.++ Str1 "ijruldtzyp") Str15))
(assert (= (str.++ (str.++ Str1 "ijruldtzyp") Str11 (str.from_int i0)) Str15 Str9))
(check-sat)