blob: 9a14251a06f563930846279fe9c1e9b7c31595b7 (
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
|
; COMMAND-LINE: --incremental
; EXPECT: unsat
; EXPECT: unsat
(set-logic QF_UFNIA)
(set-option :check-models true)
(set-option :produce-models true)
(set-option :arith-rewrite-equalities true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i5 Int)
(declare-const i7 Int)
(declare-const i8 Int)
(declare-const i10 Int)
(declare-const i11 Int)
(declare-const i13 Int)
(declare-const i15 Int)
(declare-const i16 Int)
(declare-const i17 Int)
(push 1)
(assert (< i15 i8))
(declare-const v6 Bool)
(assert (distinct (not v5) v0 v4 (or v1 v2 v0 v5) v2 v1 v6 v6 v2))
(push 1)
(declare-const v7 Bool)
(declare-const i18 Int)
(push 1)
(declare-const v8 Bool)
(assert (distinct (not v5) v0 v4 (or v1 v2 v0 v5) v2 v1 v6 v6 v2))
(declare-const v9 Bool)
(declare-const i19 Int)
(assert (xor (<= (- i4 i3 i10 i7) 65) (not v5) (and (<= i18 i11) v6 (distinct v6 (or v1 v2 v0 v5) (< i15 i8) v3 v2 v1 (< i15 i8) v6 v3 v3) (or v1 v2 v0 v5)) v7 (not v5) (= 128 i11)))
(push 1)
(declare-const v10 Bool)
(assert (=> v9 v1))
(assert (not v5))
(declare-const v11 Bool)
(declare-const i20 Int)
(declare-const i21 Int)
(assert (distinct (not v5) v0 v4 (or v1 v2 v0 v5) v2 v1 v6 v6 v2))
(push 1)
(assert (= v10 (=> (<= i18 i11) (distinct 67 i18)) v1 v6 (<= (- i4 i3 i10 i7) 65) (xor (<= (- i4 i3 i10 i7) 65) (not v5) (and (<= i18 i11) v6 (distinct v6 (or v1 v2 v0 v5) (< i15 i8) v3 v2 v1 (< i15 i8) v6 v3 v3) (or v1 v2 v0 v5)) v7 (not v5) (= 128 i11)) v8))
(push 1)
(check-sat)
(push 1)
(push 1)
(pop 1)
(check-sat)
|
