-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtight corner.z3
110 lines (107 loc) · 4.53 KB
/
tight corner.z3
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
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
(declare-const x1 Real) (assert (> x1 0.0)) (assert (< x1 1.0))
(declare-const x2 Real) (assert (> x2 0.0)) (assert (< x2 1.0))
(declare-const x3 Real) (assert (> x3 0.0)) (assert (< x3 1.0))
(declare-const x4 Real) (assert (> x4 0.0)) (assert (< x4 1.0))
(declare-const x5 Real) (assert (> x5 0.0)) (assert (< x5 1.0))
(declare-const x6 Real) (assert (> x6 0.0)) (assert (< x6 1.0))
(declare-const x7 Real) (assert (> x7 0.0)) (assert (< x7 1.0))
(declare-const x8 Real) (assert (> x8 0.0)) (assert (< x8 1.0))
(declare-const x9 Real) (assert (> x9 0.0)) (assert (< x9 1.0))
(declare-const x10 Real) (assert (> x10 0.0)) (assert (< x10 1.0))
(declare-const x11 Real) (assert (> x11 0.0)) (assert (< x11 1.0))
(declare-const x12 Real) (assert (> x12 0.0)) (assert (< x12 1.0))
(declare-const x13 Real) (assert (> x13 0.0)) (assert (< x13 1.0))
(declare-const x14 Real) (assert (> x14 0.0)) (assert (< x14 1.0))
(declare-const x15 Real) (assert (> x15 0.0)) (assert (< x15 1.0))
(declare-const x16 Real) (assert (> x16 0.0)) (assert (< x16 1.0))
(declare-const x17 Real) (assert (> x17 0.0)) (assert (< x17 1.0))
(declare-const x18 Real) (assert (> x18 0.0)) (assert (< x18 1.0))
(declare-const x19 Real) (assert (> x19 0.0)) (assert (< x19 1.0))
(declare-const x20 Real) (assert (> x20 0.0)) (assert (< x20 1.0))
(declare-const x21 Real) (assert (> x21 0.0)) (assert (< x21 1.0))
(declare-const x22 Real) (assert (> x22 0.0)) (assert (< x22 1.0))
(declare-const x23 Real) (assert (> x23 0.0)) (assert (< x23 1.0))
(declare-const x24 Real) (assert (> x24 0.0)) (assert (< x24 1.0))
(declare-const x25 Real) (assert (> x25 0.0)) (assert (< x25 1.0))
(declare-const x26 Real) (assert (> x26 0.0)) (assert (< x26 1.0))
(declare-const x27 Real) (assert (> x27 0.0)) (assert (< x27 1.0))
(declare-const x28 Real) (assert (> x28 0.0)) (assert (< x28 1.0))
(declare-const x29 Real) (assert (> x29 0.0)) (assert (< x29 1.0))
(declare-const x30 Real) (assert (> x30 0.0)) (assert (< x30 1.0))
(declare-const x31 Real) (assert (> x31 0.0)) (assert (< x31 1.0))
(declare-const x32 Real) (assert (> x32 0.0)) (assert (< x32 1.0))
(declare-const x33 Real) (assert (> x33 0.0)) (assert (< x33 1.0))
(declare-const x34 Real) (assert (> x34 0.0)) (assert (< x34 1.0))
(declare-const x35 Real) (assert (> x35 0.0)) (assert (< x35 1.0))
(declare-const x36 Real) (assert (> x36 0.0)) (assert (< x36 1.0))
(declare-const x37 Real) (assert (> x37 0.0)) (assert (< x37 1.0))
(declare-const x38 Real) (assert (> x38 0.0)) (assert (< x38 1.0))
(declare-const x39 Real) (assert (> x39 0.0)) (assert (< x39 1.0))
(declare-const x40 Real) (assert (> x40 0.0)) (assert (< x40 1.0))
(declare-const x41 Real) (assert (> x41 0.0)) (assert (< x41 1.0))
(declare-const x42 Real) (assert (> x42 0.0)) (assert (< x42 1.0))
(declare-const x43 Real) (assert (> x43 0.0)) (assert (< x43 1.0))
(declare-const x44 Real) (assert (> x44 0.0)) (assert (< x44 1.0))
(declare-const x45 Real) (assert (> x45 0.0)) (assert (< x45 1.0))
(declare-const x46 Real) (assert (> x46 0.0)) (assert (< x46 1.0))
(declare-const x47 Real) (assert (> x47 0.0)) (assert (< x47 1.0))
(declare-const x48 Real) (assert (> x48 0.0)) (assert (< x48 1.0))
(declare-const x49 Real) (assert (> x49 0.0)) (assert (< x49 1.0))
(declare-const x50 Real) (assert (> x50 0.0)) (assert (< x50 1.0))
(assert (> x1 0.5))
(assert (> x2 0.5))
(assert (> x3 0.5))
(assert (> x4 0.5))
(assert (> x5 0.5))
(assert (> x6 0.5))
(assert (> x7 0.5))
(assert (> x8 0.5))
(assert (> x9 0.5))
(assert (> x10 0.5))
(assert (> x11 0.5))
(assert (> x12 0.5))
(assert (> x13 0.5))
(assert (> x14 0.5))
(assert (> x15 0.5))
(assert (> x16 0.5))
(assert (> x17 0.5))
(assert (> x18 0.5))
(assert (> x19 0.5))
(assert (> x20 0.5))
(assert (> x21 0.5))
(assert (> x22 0.5))
(assert (> x23 0.5))
(assert (> x24 0.5))
(assert (> x25 0.5))
(assert (> x26 0.5))
(assert (> x27 0.5))
(assert (> x28 0.5))
(assert (> x29 0.5))
(assert (> x30 0.5))
(assert (> x31 0.5))
(assert (> x32 0.5))
(assert (> x33 0.5))
(assert (> x34 0.5))
(assert (> x35 0.5))
(assert (> x36 0.5))
(assert (> x37 0.5))
(assert (> x38 0.5))
(assert (> x39 0.5))
(assert (> x40 0.5))
(assert (> x41 0.5))
(assert (> x42 0.5))
(assert (> x43 0.5))
(assert (> x44 0.5))
(assert (> x45 0.5))
(assert (> x46 0.5))
(assert (> x47 0.5))
(assert (> x48 0.5))
(assert (> x49 0.5))
(assert (> x50 0.5))
(check-sat-using
(par-or
;; Strategy 1: using seed 1
(using-params smt :random-seed 1)
)
)
(get-model)