diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-03-20 15:21:31 +0100 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-03-20 15:21:31 +0100 |
| commit | d072e064a960b4e01dfe66ef769f8d4d5fdefa41 (patch) | |
| tree | 3d76eb63bb5c180161b505341a6da269edc2ae59 /Test/dafny0/Answer | |
| parent | e360598b592c207b2372ba450e90288f834c9317 (diff) | |
Added multiset update.
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 2e1bd93c..72c142ac 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1689,8 +1689,13 @@ MultiSets.dfy(163,3): Error BP5003: A postcondition might not hold on this retur MultiSets.dfy(162,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
+MultiSets.dfy(176,11): Error: new number of occurrences might be negative
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Then
+ (0,0): anon3
-Dafny program verifier finished with 38 verified, 2 errors
+Dafny program verifier finished with 39 verified, 3 errors
-------------------- PredExpr.dfy --------------------
PredExpr.dfy(4,12): Error: condition in assert expression might not hold
|