blob: ab1cea0c86b05c81d81fb4ece89a6c5d69397d34 (
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
25
|
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
(declare-const x Int)
(declare-const a1 Int)
(declare-const a2 Int)
(declare-const a3 Int)
(declare-const a4 Int)
(declare-const a5 Int)
(declare-const a6 Int)
(declare-const a7 Int)
(declare-const a8 Int)
(declare-const a9 Int)
(assert (and (pto x a1) (pto x a2) (pto x a3)
(pto x a4) (pto x a5) (pto x a6)
(pto x a7) (pto x a8) (pto x a9)
)
)
(assert (not (= a1 a2 a3 a4 a5 a6 a7 a8 a9)))
(check-sat)
|
