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
111
|
formula 2 is: A -> A /\ B
task 2 created:
theory Task
predicate A
predicate B
(* meta get_counterexmp *)
goal goal2 : A -> A /\ B
end
On task 1, CVC4,1.7 answers Unknown (sat) (<hidden>s, <hidden> steps)
Model is [{"filename": "myfile.my_ext",
"model":
[{"is_vc_line": false,
"line": "28",
"model_elements":
[{"attrs": ["model_trace:my_A"],
"kind": "other",
"location":
{"end-char": 1,
"end-line": 28,
"file-name": "myfile.my_ext",
"start-char": 0,
"start-line": 28},
"lsymbol":
{"attrs": ["model_trace:my_A"],
"loc":
{"end-char": 1,
"end-line": 28,
"file-name": "myfile.my_ext",
"start-char": 0,
"start-line": 28},
"name": "A"},
"value":
{"value_concrete_term": {"type": "Boolean", "val": true},
"value_term": "Ttrue",
"value_type": null}},
{"attrs": ["model_trace:my_A"],
"kind": "other",
"location":
{"end-char": 1,
"end-line": 28,
"file-name": "myfile.my_ext",
"start-char": 0,
"start-line": 28},
"lsymbol":
{"attrs": ["model_trace:my_A"],
"loc":
{"end-char": 1,
"end-line": 28,
"file-name": "myfile.my_ext",
"start-char": 0,
"start-line": 28},
"name": "A"},
"value":
{"value_concrete_term": {"type": "Boolean", "val": true},
"value_term": "Ttrue",
"value_type": null}}]}]},
{"filename": "myfile.my_ext2",
"model":
[{"is_vc_line": false,
"line": "101",
"model_elements":
[{"attrs": ["model_trace:my_B"],
"kind": "other",
"location":
{"end-char": 1,
"end-line": 101,
"file-name": "myfile.my_ext2",
"start-char": 0,
"start-line": 101},
"lsymbol":
{"attrs": ["model_trace:my_B"],
"loc":
{"end-char": 1,
"end-line": 101,
"file-name": "myfile.my_ext2",
"start-char": 0,
"start-line": 101},
"name": "B"},
"value":
{"value_concrete_term": {"type": "Boolean", "val": false},
"value_term": "Tfalse",
"value_type": null}},
{"attrs": ["model_trace:my_B"],
"kind": "other",
"location":
{"end-char": 1,
"end-line": 101,
"file-name": "myfile.my_ext2",
"start-char": 0,
"start-line": 101},
"lsymbol":
{"attrs": ["model_trace:my_B"],
"loc":
{"end-char": 1,
"end-line": 101,
"file-name": "myfile.my_ext2",
"start-char": 0,
"start-line": 101},
"name": "B"},
"value":
{"value_concrete_term": {"type": "Boolean", "val": false},
"value_term": "Tfalse",
"value_type": null}}]}]}]
== Check CE
|
