blob: 7cd3e824257aaba9f8567c4d3f09fc702cb8fcf2 (
plain) (
blame)
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
|
(th_B
(B_0 0
(B_0-1 nil 3666686678 ("" (flatten) (("" (inst -1 "a") nil nil)) nil)
((U nonempty-type-decl nil th_B nil) (a const-decl "U" th_B nil))
shostak))
(B_1 0
(B_1-1 nil 3666686733
("" (flatten) (("" (inst -1 "a") (("" (assert) nil nil)) nil)) nil)
((U nonempty-type-decl nil th_B nil) (a const-decl "U" th_B nil))
shostak))
(B_2 0
(B_2-1 nil 3666686753
("" (flatten) (("" (inst 1 "a") (("" (inst -1 "a") nil nil)) nil))
nil)
((U nonempty-type-decl nil th_B nil) (a const-decl "U" th_B nil))
shostak))
(B_3 0
(B_3-1 nil 3666686845
("" (flatten) (("" (skolem 1 "B") (("" (inst 2 "B") nil nil)) nil))
nil)
((U nonempty-type-decl nil th_B nil)) shostak))
(B_4 0
(B_4-1 nil 3666686921
("" (split)
(("1" (flatten)
(("1" (skolem 1 "A") (("1" (inst 2 "A") nil nil)) nil)) nil)
("2" (flatten)
(("2" (skolem -1 "A") (("2" (inst -1 "A") nil nil)) nil)) nil))
nil)
((U nonempty-type-decl nil th_B nil)) shostak))
(B_5 0
(B_5-1 nil 3666687393
("" (split)
(("1" (flatten)
(("1" (skolem 2 "A") (("1" (inst 1 "A") nil nil)) nil)) nil)
("2" (flatten)
(("2" (skolem -2 "A") (("2" (inst -1 "A") nil nil)) nil)) nil))
nil)
((U nonempty-type-decl nil th_B nil)) shostak))
(B_6 0
(B_6-1 nil 3666687440
("" (split)
(("1" (flatten)
(("1" (skolem 1 "A")
(("1" (split)
(("1" (inst -1 "A") nil nil) ("2" (inst -2 "A") nil nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split)
(("1" (skolem 1 "A")
(("1" (inst -1 "A") (("1" (flatten -1) nil nil)) nil)) nil)
("2" (skolem 1 "A")
(("2" (inst -1 "A") (("2" (flatten -1) nil nil)) nil)) nil))
nil))
nil))
nil)
((U nonempty-type-decl nil th_B nil)) shostak))
(B_7 0
(B_7-1 nil 3666687512
("" (split)
(("1" (flatten)
(("1" (split -1)
(("1" (skolem -1 "A")
(("1" (inst 1 "A") (("1" (flatten 1) nil nil)) nil)) nil)
("2" (skolem -1 "A")
(("2" (inst 1 "A") (("2" (flatten 1) nil nil)) nil)) nil))
nil))
nil)
("2" (flatten)
(("2" (skolem -1 "A")
(("2" (split -1)
(("1" (inst 1 "A") nil nil) ("2" (inst 2 "A") nil nil)) nil))
nil))
nil))
nil)
((U nonempty-type-decl nil th_B nil)) shostak)))
|
