blob: 531556e6df8846918e9244c01db10f7d66eaa7f6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(set-info :smt-lib-version 2.5)
(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)
|
