Skip to content

Commit e995740

Browse files
committed
taking static final fields into account for createdness proofs.
1 parent 2f599d3 commit e995740

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1356,9 +1356,9 @@
13561356
deltaObject::final(o, f),
13571357
java.lang.Object::<created>) = TRUE )
13581358

1359-
\replacewith( ==> boolean::select(h, o, java.lang.Object::<created>) = TRUE )
1359+
\replacewith( ==> boolean::select(h, o, java.lang.Object::<created>) = TRUE | o = null )
13601360

1361-
\heuristics(concrete)
1361+
\heuristics(simplify_enlarging)
13621362
};
13631363

13641364
referencedObjectIsCreatedRighFinalEQ {
@@ -1372,7 +1372,7 @@
13721372
EQ,
13731373
java.lang.Object::<created>) = TRUE)
13741374

1375-
\add( ==> boolean::select(h, o, java.lang.Object::<created>) = TRUE )
1375+
\add( ==> boolean::select(h, o, java.lang.Object::<created>) = TRUE | o = null )
13761376

13771377
\heuristics(concrete)
13781378
};

0 commit comments

Comments
 (0)