blob: 1acc091c1d510ceef9346af0f3fc9fc16e27939c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
(set-logic QF_SLIA)
(set-info :status sat)
(declare-fun x () String)
(declare-fun y () String)
(declare-fun z () String)
(declare-fun w () String)
(assert (>= (str.code x) 65))
(assert (<= (str.code x) 75))
(assert (>= (str.code y) 65))
(assert (<= (str.code y) 75))
(assert (>= (str.code z) 65))
(assert (<= (str.code z) 75))
(assert (= (str.len w) 1))
(assert (= (+ (str.code x) (str.code y)) 140))
(assert (= (+ (str.code x) (str.code z)) 141))
(assert (distinct x y z w "A" "B" "C" "D" "AA"))
(check-sat)
|
