Skip to content

Commit 6d44452

Browse files
committed
Fix set statement test case
- assertion used wrong method to check for ghost flag
1 parent b3482d6 commit 6d44452

1 file changed

Lines changed: 2 additions & 1 deletion

File tree

key.core/src/test/java/de/uka/ilkd/key/speclang/SetStatementTest.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
import de.uka.ilkd.key.logic.JTerm;
1414
import de.uka.ilkd.key.logic.ProgramElementName;
1515
import de.uka.ilkd.key.logic.op.LocationVariable;
16+
import de.uka.ilkd.key.logic.op.ProgramVariable;
1617
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
1718
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct;
1819
import de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLSetStatement;
@@ -136,6 +137,6 @@ class Foo {
136137
var fields = cu.getDeclarations().get(0).getAllFields(env.getServices());
137138
var fieldX = fields.stream().filter(it -> "Foo::x".equals(it.getName())).findFirst().get();
138139

139-
Assertions.assertTrue(fieldX.getProgramVariable().isRigid());
140+
Assertions.assertTrue(((ProgramVariable) fieldX.getProgramVariable()).isGhost());
140141
}
141142
}

0 commit comments

Comments
 (0)