blob: ff20ec9d47bb59f5e863c83c88c98c57bf76709e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(set-info :smt-lib-version 2.6)
(set-logic QF_SLIA)
(set-option :strings-exp true)
(set-info :status unsat)
(declare-fun x () String)
(declare-fun y () String)
(declare-fun z () String)
(assert (or (= x y)(= x z)))
(assert (str.in_re x (re.++ (str.to_re "A") (re.* (str.to_re "BAA")))))
(assert (str.in_re y (re.++ (str.to_re "AB") (re.* (str.to_re "AAB")) (str.to_re "A"))))
(assert (str.in_re z (re.++ (str.to_re "AB") (re.* (str.to_re "AAB")) (str.to_re "A"))))
; requires RE solver to reason modulo string equalties
(check-sat)
|
