Fixing issue #845 - Githubissues

viperproject / silicon

Symbolic-execution-based verifier for the Viper intermediate verification language.

Mozilla Public License 2.0

79 stars 31 forks source link

Closed marcoeilers closed 3 months ago

marcoeilers commented 3 months ago

When we need a snapshot map without a domain, we can take a cached one that does have a domain if the domain condition is true
When we create a new snapshot map to define the snapshot of consuming a single location, it does not need a domain.

Fixes #845 and #844.