blob: 4c6b2091b1abf5bd060668c2f4519668f912e7e7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(set-info :smt-lib-version 2.6)
(set-logic QF_S)
(set-option :strings-exp true)
(set-option :strings-fmf true)
(set-info :status sat)
(declare-fun x () String)
(declare-fun y () String)
(assert (str.in_re x
(re.* (re.++ (re.* (str.to_re "a") ) (str.to_re "b") ))
))
(assert (str.in_re y
(re.* (re.++ (re.* (str.to_re "a") ) (str.to_re "b") ))
))
(assert (not (= x y)))
(assert (= (str.len x) (str.len y)))
(check-sat)
|
