-
Notifications
You must be signed in to change notification settings - Fork 1
/
TESTS
108 lines (68 loc) · 1.45 KB
/
TESTS
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
A few tests below. There are also internal test cases in Java.
No sorts, but A C:
Error: Sort A was undeclared, but used in ordering: A C.
********************************
Check for double constant, double function:
Function/Constant name: c appeared more than once.
The current web application does not support overloading of functions.
********************************
********************************
Empty test:
A
all x : A | x in P
Expect: All finitary but empty
********************************
Basic test:
A
B
C
A B
A C
c A
some x : A | x in P
Expect: 2 in A, B, C
********************************
More advanced counting:
A
B
C
D
<no subs>
f A A B
g B B C
h C C D
c A
some x : A | x in P
univ: 278 C: 16 D: 256 A: 2 B: 4
********************************
Same, but with subs to check propagation:
A
B
C
D
A C
f A A B
g B B C
h C C D
c A
some x : A | x in P
C is 2 more than before, due to propagation.
18^2 = 324.
univ: 346 C: 18 D: 324 A: 2 B: 4
********************************
No integer overflow:
A
B
C
D
E
<no subs>
f A A A B
g B B B C
h C C C D
i D D D E
c A
some x : A | x in P
2 ----> 2^3 = 8 ----> 2^3^3 = 2^9 = 512 ----> 512^3 = 134217728 ----> 134217728^3 = 2417851639229258349412352
added together, we get the univ result:
univ: 2417851639229258483630602 C: 512 D: 134217728 E: 2417851639229258349412352 A: 2 B: 8