Skip to content

Commit dbed9ab

Browse files
committed
ignore information within "STATE" block in Boogie counterexample
in newer Boogie versions such blocks are emitted for /mv:- (we should switch to /printModel:1, but it does not seem to work with /errorTrace:0)
1 parent 2f2b333 commit dbed9ab

1 file changed

Lines changed: 6 additions & 0 deletions

File tree

src/main/scala/viper/carbon/verifier/BoogieInterface.scala

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -124,8 +124,14 @@ trait BoogieInterface {
124124
}
125125

126126
var parsingModel : Option[StringBuilder] = None
127+
var stateInitialBlock = false
127128
for (l <- output.linesIterator) {
128129
l match {
130+
case "*** END_STATE" =>
131+
stateInitialBlock = false
132+
case "*** STATE <initial>" =>
133+
stateInitialBlock = true
134+
case _ if stateInitialBlock => //ignore everything within state block
129135
case "*** END_MODEL" if parsingModel.isDefined =>
130136
models.append(parsingModel.get.toString())
131137
parsingModel = None

0 commit comments

Comments
 (0)