test/regress/regress1/strings/issue4701_substr_splice.smt2


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

(set-logic QF_SLIA)
(set-info :status sat)
(set-option :strings-exp true)
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun e () String)
(assert (= e (str.++ b (str.substr a 0 1))))
(assert (= a (str.substr c 0 (str.len e))))
(assert (= "a" b))
(assert (= (str.++ b a) (str.replace c e a)))
(check-sat)