Heap updates ignored on LetSubstitutionRule application

mattulbrich / dive

Dafny Interactive Verification Environment (DIVE)

GNU General Public License v3.0

4 stars 0 forks source link

Heap updates ignored on LetSubstitutionRule application #206

Open SpringVaS opened 2 years ago

SpringVaS commented 2 years ago

Updates to a heap are handled as a LetTerm with substitution "heap" -> store... The Term representation of heap is a ApplTerm. The SubstitutionVisitor, only substitutes VarTerms. So the heap update is ignored on the application of LetSubstitutionRule.