Skip to content

Commit eaa8345

Browse files
committed
BV refinement: include XML output in schema
Make sure <refinement-iteration> tags do not cause validation errors.
1 parent 5e145e4 commit eaa8345

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

doc/assets/xml_spec.xsd

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -181,6 +181,8 @@
181181
</xs:complexType>
182182
</xs:element>
183183

184+
<xs:element name="refinement-iteration" type="xs:integer"/>
185+
184186
<xs:element name="program" type="xs:string"/>
185187
<xs:element name="cprover-status" type="xs:string"/>
186188
<xs:element name="cprover">
@@ -190,6 +192,7 @@
190192
<xs:choice minOccurs="0" maxOccurs="unbounded">
191193
<xs:element ref="message"/>
192194
<xs:element ref="result"/>
195+
<xs:element ref="refinement-iteration"/>
193196
</xs:choice>
194197
<xs:element ref="cprover-status" minOccurs="0"/>
195198
</xs:sequence>

0 commit comments

Comments
 (0)