diff options
| author |  Rustan Leino <unknown> | 2014-06-24 10:45:53 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-06-24 10:45:53 -0700 |
| commit | 2e01ab9670a91ab7b6b22a9cff676f45b629755e (patch) | |
| tree | 58089e77f6a32462971aec82c91f4d2c09af89c6 /Test/dafny0/MultiSets.dfy.expect | |
| parent | 19895aaed833d16bad36a07e9459abc882ccd6b6 (diff) | |
Added some axioms about seq-to-multiset conversions
Diffstat (limited to 'Test/dafny0/MultiSets.dfy.expect')
| -rw-r--r-- | Test/dafny0/MultiSets.dfy.expect | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/Test/dafny0/MultiSets.dfy.expect b/Test/dafny0/MultiSets.dfy.expect index cdee5d20..30534b11 100644 --- a/Test/dafny0/MultiSets.dfy.expect +++ b/Test/dafny0/MultiSets.dfy.expect @@ -18,5 +18,11 @@ Execution trace: (0,0): anon3
(0,0): anon12_Then
(0,0): anon14_Else
+MultiSets.dfy(292,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon8_Then
+ (0,0): anon3
+ (0,0): anon9_Else
-Dafny program verifier finished with 54 verified, 4 errors
+Dafny program verifier finished with 59 verified, 5 errors
|