blob: fe91cb87b44dabfcc63b376c309b58466430e5b5 (
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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
(set-logic QF_BV)
(set-info :status unsat)
(declare-fun x1 () (_ BitVec 12))
(declare-fun x2 () (_ BitVec 12))
(declare-fun x3 () (_ BitVec 12))
(declare-fun y1 () (_ BitVec 12))
(declare-fun y2 () (_ BitVec 12))
(declare-fun y3 () (_ BitVec 12))
(declare-fun z1 () (_ BitVec 12))
(declare-fun z2 () (_ BitVec 12))
(declare-fun z3 () (_ BitVec 12))
(declare-fun a () (_ BitVec 12))
(declare-fun x01 () (_ BitVec 10))
(declare-fun x02 () (_ BitVec 10))
(declare-fun x03 () (_ BitVec 10))
(declare-fun y01 () (_ BitVec 10))
(declare-fun y02 () (_ BitVec 10))
(declare-fun y03 () (_ BitVec 10))
(declare-fun z01 () (_ BitVec 10))
(declare-fun z02 () (_ BitVec 10))
(declare-fun z03 () (_ BitVec 10))
(declare-fun a0 () (_ BitVec 10))
(assert
(or
(and
(= a (_ bv0 12))
(or (not (= (bvudiv x1 a) (bvudiv x2 a)))
(not (= (bvudiv x1 a) (bvudiv x3 a)))
(not (= (bvudiv x2 a) (bvudiv x3 a))))
(or (and (= x1 y1) (= y1 x2))
(and (= x1 z1) (= z1 x2)))
(or (and (= x2 y2) (= y2 x3))
(and (= x2 z2) (= z2 x3))))
(and
(= a0 (_ bv0 10))
(or (not (= (bvurem x01 a0) (bvurem x02 a0)))
(not (= (bvurem x01 a0) (bvurem x03 a0)))
(not (= (bvurem x02 a0) (bvurem x03 a0))))
(or (and (= x01 y01) (= y01 x02))
(and (= x01 z01) (= z01 x02)))
(or (and (= x02 y02) (= y02 x03))
(and (= x02 z02) (= z02 x03))))))
(check-sat)
|
