-
Notifications
You must be signed in to change notification settings - Fork 0
/
test1.z3
91 lines (91 loc) · 4.8 KB
/
test1.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
(declare-const lambda*3792 Int)
(declare-const lambda*3797 Int)
(declare-const lambda*3801 Int)
(declare-const lambda*3805 Int)
(declare-const lambda*3810 Int)
(declare-const lambda*3815 Int)
(declare-const lambda*3818 Int)
(declare-const lambda3788 Int)
(declare-const lambda3789 Int)
(declare-const lambda3790 Int)
(declare-const lambda3791 Int)
(declare-const lambda3796 Int)
(declare-const lambda3793 Int)
(declare-const lambda3794 Int)
(declare-const lambda3795 Int)
(declare-const lambda3798 Int)
(declare-const lambda3799 Int)
(declare-const lambda3800 Int)
(declare-const lambda3802 Int)
(declare-const lambda3803 Int)
(declare-const lambda3804 Int)
(declare-const lambda3806 Int)
(declare-const lambda3807 Int)
(declare-const lambda3808 Int)
(declare-const lambda3809 Int)
(declare-const lambda3812 Int)
(declare-const lambda3814 Int)
(declare-const lambda3811 Int)
(declare-const lambda3813 Int)
(declare-const lambda3816 Int)
(declare-const lambda3817 Int)
(declare-const u3782 Int)
(declare-const u3783 Int)
(declare-const u3785 Int)
(declare-const u3786 Int)
(declare-const u3784 Int)
(declare-const u3787 Int)
(assert (= (+ 0 (* lambda3788 -1) (* lambda3789 (+ -1 (* u3782 -1) (* u3783 -1))) (* lambda3790 (+ -1 (* u3785 -1) (* u3786 -1))) (* lambda3791 (+ 0 u3782))) (* -1 lambda*3792)))
(assert (= (+ 0 (* lambda3789 (+ (* u3783 -1) (* u3784 -1))) (* lambda3790 (+ (* u3786 -1) (* u3787 -1))) (* lambda3791 u3783)) 0))
(assert (= (+ 0 (* lambda3788 -1) (* lambda3789 (* u3784 -1)) (* lambda3790 (* u3787 -1)) (* lambda3791 u3784)) 0))
(assert (= (+ (* lambda3796 (+ 0 u3785)) 0 (* lambda3793 -1) (* lambda3794 (+ -1 (* u3782 -1) (* u3783 -1))) (* lambda3795 (+ -1 (* u3785 -1) (* u3786 -1)))) (* -1 lambda*3797)))
(assert (= (+ (* lambda3796 u3786) 0 (* lambda3794 (+ (* u3783 -1) (* u3784 -1))) (* lambda3795 (+ (* u3786 -1) (* u3787 -1)))) 0))
(assert (= (+ (* lambda3796 u3787) 0 (* lambda3793 -1) (* lambda3794 (* u3784 -1)) (* lambda3795 (* u3787 -1))) 0))
(assert (= (+ 0 (* lambda3798 0) (* lambda3799 0) (* lambda3800 (+ 0 u3782))) (* -1 lambda*3801)))
(assert (= (+ 0 (* lambda3798 -1) (* lambda3800 u3783)) 0))
(assert (= (+ 0 lambda3799 (* lambda3800 u3784)) 0))
(assert (= (+ 0 (* lambda3802 0) (* lambda3803 0) (* lambda3804 (+ 0 u3785))) (* -1 lambda*3805)))
(assert (= (+ 0 (* lambda3802 -1) (* lambda3804 u3786)) 0))
(assert (= (+ 0 lambda3803 (* lambda3804 u3787)) 0))
(assert (= (+ 0 (* lambda3806 0) (* lambda3807 (+ -1 (* u3782 -1))) (* lambda3808 (+ -1 (* u3785 -1))) (* lambda3809 (+ 0 u3782))) (* -1 lambda*3810)))
(assert (= (+ 0 (* lambda3807 (* u3783 -1)) (* lambda3808 (* u3786 -1)) (* lambda3809 u3783)) 0))
(assert (= (+ 0 lambda3806 (* lambda3807 (* u3784 -1)) (* lambda3808 (* u3787 -1)) (* lambda3809 u3784)) 0))
(assert (= (+ 0 (* lambda3813 (+ -1 (* u3785 -1))) (* lambda3812 (+ -1 (* u3782 -1))) (* lambda3814 (+ 0 u3785)) (* lambda3811 0)) (* -1 lambda*3815)))
(assert (= (+ 0 (* lambda3813 (* u3786 -1)) (* lambda3812 (* u3783 -1)) (* lambda3814 u3786)) 0))
(assert (= (+ 0 (* lambda3813 (* u3787 -1)) (* lambda3812 (* u3784 -1)) (* lambda3814 u3787) lambda3811) 0))
(assert (= (+ 0 (* lambda3816 (+ -1 (* u3782 -1) (* u3784 50))) (* lambda3817 (+ -1 (* u3785 -1) (* u3787 50)))) (* -1 lambda*3818)))
(assert (= (+ 0 (* lambda3816 (* u3783 -1)) (* lambda3817 (* u3786 -1))) 0))
(assert (>= lambda3788 0))
(assert (>= lambda3789 0))
(assert (>= lambda3790 0))
(assert (>= lambda3791 0))
(assert (>= lambda3796 0))
(assert (>= lambda3793 0))
(assert (>= lambda3794 0))
(assert (>= lambda3795 0))
(assert (>= lambda3798 0))
(assert (>= lambda3799 0))
(assert (>= lambda3800 0))
(assert (>= lambda3802 0))
(assert (>= lambda3803 0))
(assert (>= lambda3804 0))
(assert (>= lambda3806 0))
(assert (>= lambda3807 0))
(assert (>= lambda3808 0))
(assert (>= lambda3809 0))
(assert (>= lambda3812 0))
(assert (>= lambda3814 0))
(assert (>= lambda3811 0))
(assert (>= lambda3813 0))
(assert (>= lambda3816 0))
(assert (>= lambda3817 0))
(assert (> lambda*3792 0))
(assert (> lambda*3797 0))
(assert (> lambda*3801 0))
(assert (> lambda*3805 0))
(assert (> lambda*3810 0))
(assert (> lambda*3815 0))
(assert (> lambda*3818 0))
(check-sat)
(get-model)
'(#<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void> #<void>)