diff options
| author |  Rustan Leino <unknown> | 2014-04-04 10:55:23 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-04 10:55:23 -0700 |
| commit | e8bae7e26441d2077d33a8b771c7d559eaee5d71 (patch) | |
| tree | a8ab63f7c5c4e92abeeebb2319fb248af1fc8a5d /Test/dafny4/ClassRefinement.dfy | |
| parent | 0abbaee631e42479bba3cf98cb9a41fdf0f9358d (diff) | |
Also include lower set bounds (bounding a set from below) in witness guesses for assign/let such-that.
Diffstat (limited to 'Test/dafny4/ClassRefinement.dfy')
| -rw-r--r-- | Test/dafny4/ClassRefinement.dfy | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Test/dafny4/ClassRefinement.dfy b/Test/dafny4/ClassRefinement.dfy index 4fc29122..5c444120 100644 --- a/Test/dafny4/ClassRefinement.dfy +++ b/Test/dafny4/ClassRefinement.dfy @@ -21,7 +21,6 @@ module M0 { ensures Valid() && fresh(Repr - {this});
{
Repr := {};
- assert {this} <= {this} && fresh({this} - {this});
ghost var repr :| {this} <= repr && fresh(repr - {this});
N, Repr := 0, repr;
}
|