diff options
| author |  Jason Koenig <unknown> | 2012-08-01 16:10:31 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-08-01 16:10:31 -0700 |
| commit | e185476ebd83b0134fb0701afcecd33b7fa1225b (patch) | |
| tree | b83bb2a5aa2c63228b781538caba77d6eabd8e6f /Test/dafny0/Answer | |
| parent | 65d7904363c7ff7159fd042b48099e232bea49a7 (diff) | |
Dafny: fixed bug in reverifying allowing old locals to be modified.
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 3899b6df..70527966 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1599,10 +1599,9 @@ LiberalEquality.dfy(52,14): Error: arguments must have the same type (got array< 3 resolution/type errors detected in LiberalEquality.dfy
-------------------- RefinementModificationChecking.dfy --------------------
-RefinementModificationChecking.dfy(16,4): Error: cannot assign to variable defined previously
RefinementModificationChecking.dfy(17,4): Error: cannot assign to variable defined previously
-RefinementModificationChecking.dfy(18,4): Error: cannot assign to field defined previously
-3 resolution/type errors detected in RefinementModificationChecking.dfy
+RefinementModificationChecking.dfy(18,4): Error: cannot assign to variable defined previously
+2 resolution/type errors detected in RefinementModificationChecking.dfy
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
|