-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtest.z3
90 lines (90 loc) · 4.09 KB
/
test.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
(declare-const lambda*7369 Int)
(declare-const lambda*7374 Int)
(declare-const lambda*7378 Int)
(declare-const lambda*7382 Int)
(declare-const lambda*7387 Int)
(declare-const lambda*7392 Int)
(declare-const lambda*7395 Int)
(declare-const lambda7367 Int)
(declare-const lambda7365 Int)
(declare-const lambda7366 Int)
(declare-const lambda7368 Int)
(declare-const lambda7370 Int)
(declare-const lambda7371 Int)
(declare-const lambda7372 Int)
(declare-const lambda7373 Int)
(declare-const lambda7375 Int)
(declare-const lambda7376 Int)
(declare-const lambda7377 Int)
(declare-const lambda7379 Int)
(declare-const lambda7380 Int)
(declare-const lambda7381 Int)
(declare-const lambda7383 Int)
(declare-const lambda7385 Int)
(declare-const lambda7386 Int)
(declare-const lambda7384 Int)
(declare-const lambda7388 Int)
(declare-const lambda7389 Int)
(declare-const lambda7390 Int)
(declare-const lambda7391 Int)
(declare-const lambda7393 Int)
(declare-const lambda7394 Int)
(declare-const u7359 Int)
(declare-const u7362 Int)
(declare-const u7363 Int)
(declare-const u7360 Int)
(declare-const u7364 Int)
(declare-const u7361 Int)
(assert (= (+ 0 (* lambda7368 (+ 0 u7359)) (* lambda7367 (+ -1 (* u7362 -1) (* u7363 -1))) (* lambda7365 -1) (* lambda7366 (+ -1 (* u7359 -1) (* u7360 -1)))) (* -1 lambda*7369)))
(assert (= (+ 0 (* lambda7368 u7360) (* lambda7367 (+ (* u7363 -1) (* u7364 -1))) (* lambda7366 (+ (* u7360 -1) (* u7361 -1)))) 0))
(assert (= (+ 0 (* lambda7368 u7361) (* lambda7367 (* u7364 -1)) (* lambda7365 -1) (* lambda7366 (* u7361 -1))) 0))
(assert (= (+ 0 (* lambda7370 -1) (* lambda7371 (+ -1 (* u7359 -1) (* u7360 -1))) (* lambda7372 (+ -1 (* u7362 -1) (* u7363 -1))) (* lambda7373 (+ 0 u7362))) (* -1 lambda*7374)))
(assert (= (+ 0 (* lambda7371 (+ (* u7360 -1) (* u7361 -1))) (* lambda7372 (+ (* u7363 -1) (* u7364 -1))) (* lambda7373 u7363)) 0))
(assert (= (+ 0 (* lambda7370 -1) (* lambda7371 (* u7361 -1)) (* lambda7372 (* u7364 -1)) (* lambda7373 u7364)) 0))
(assert (= (+ 0 (* lambda7375 0) (* lambda7376 0) (* lambda7377 (+ 0 u7359))) (* -1 lambda*7378)))
(assert (= (+ 0 (* lambda7375 -1) (* lambda7377 u7360)) 0))
(assert (= (+ 0 lambda7376 (* lambda7377 u7361)) 0))
(assert (= (+ 0 (* lambda7379 0) (* lambda7380 0) (* lambda7381 (+ 0 u7362))) (* -1 lambda*7382)))
(assert (= (+ 0 (* lambda7379 -1) (* lambda7381 u7363)) 0))
(assert (= (+ 0 lambda7380 (* lambda7381 u7364)) 0))
(assert (= (+ 0 (* lambda7384 (+ -1 (* u7359 -1))) (* lambda7383 0) (* lambda7385 (+ -1 (* u7362 -1))) (* lambda7386 (+ 0 u7359))) (* -1 lambda*7387)))
(assert (= (+ 0 (* lambda7384 (* u7360 -1)) (* lambda7385 (* u7363 -1)) (* lambda7386 u7360)) 0))
(assert (= (+ 0 (* lambda7384 (* u7361 -1)) lambda7383 (* lambda7385 (* u7364 -1)) (* lambda7386 u7361)) 0))
(assert (= (+ 0 (* lambda7388 0) (* lambda7389 (+ -1 (* u7359 -1))) (* lambda7390 (+ -1 (* u7362 -1))) (* lambda7391 (+ 0 u7362))) (* -1 lambda*7392)))
(assert (= (+ 0 (* lambda7389 (* u7360 -1)) (* lambda7390 (* u7363 -1)) (* lambda7391 u7363)) 0))
(assert (= (+ 0 lambda7388 (* lambda7389 (* u7361 -1)) (* lambda7390 (* u7364 -1)) (* lambda7391 u7364)) 0))
(assert (= (+ 0 (* lambda7393 (+ -1 (* u7359 -1) (* u7361 50))) (* lambda7394 (+ -1 (* u7362 -1) (* u7364 50)))) (* -1 lambda*7395)))
(assert (= (+ 0 (* lambda7393 (* u7360 -1)) (* lambda7394 (* u7363 -1))) 0))
(assert (>= lambda7367 0))
(assert (>= lambda7365 0))
(assert (>= lambda7366 0))
(assert (>= lambda7368 0))
(assert (>= lambda7370 0))
(assert (>= lambda7371 0))
(assert (>= lambda7372 0))
(assert (>= lambda7373 0))
(assert (>= lambda7375 0))
(assert (>= lambda7376 0))
(assert (>= lambda7377 0))
(assert (>= lambda7379 0))
(assert (>= lambda7380 0))
(assert (>= lambda7381 0))
(assert (>= lambda7383 0))
(assert (>= lambda7385 0))
(assert (>= lambda7386 0))
(assert (>= lambda7384 0))
(assert (>= lambda7388 0))
(assert (>= lambda7389 0))
(assert (>= lambda7390 0))
(assert (>= lambda7391 0))
(assert (>= lambda7393 0))
(assert (>= lambda7394 0))
(assert (> lambda*7369 0))
(assert (> lambda*7374 0))
(assert (> lambda*7378 0))
(assert (> lambda*7382 0))
(assert (> lambda*7387 0))
(assert (> lambda*7392 0))
(assert (> lambda*7395 0))
(check-sat)
(get-model)