diff options
| author |  leino <unknown> | 2015-01-09 05:09:25 -0800 |
|---|---|---|
| committer | leino <unknown> | 2015-01-09 05:09:25 -0800 |
| commit | 97e7528b3cd3e9b9e21b75abf817d6e0ed3b9df7 (patch) | |
| tree | 7d94bf568cce7b5b232f32c525f05122b934054d /Test/dafny0/DiamondImports.dfy.expect | |
| parent | b09206df1a298d56fca3bec95baab41b7f670731 (diff) | |
When ambiguous references all resolve to the same declaration, don't complain
Diffstat (limited to 'Test/dafny0/DiamondImports.dfy.expect')
| -rw-r--r-- | Test/dafny0/DiamondImports.dfy.expect | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/Test/dafny0/DiamondImports.dfy.expect b/Test/dafny0/DiamondImports.dfy.expect new file mode 100644 index 00000000..e9e8c2b9 --- /dev/null +++ b/Test/dafny0/DiamondImports.dfy.expect @@ -0,0 +1,32 @@ +DiamondImports.dfy(34,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+DiamondImports.dfy(50,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+ (0,0): anon2
+DiamondImports.dfy(101,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon7_Then
+ (0,0): anon2
+ (0,0): anon8_Then
+ (0,0): anon9_Then
+ (0,0): anon6
+DiamondImports.dfy(120,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Then
+ (0,0): anon2
+ (0,0): anon10_Then
+ (0,0): anon4
+ (0,0): anon11_Then
+ (0,0): anon6
+ (0,0): anon12_Then
+ (0,0): anon8
+DiamondImports.dfy(140,26): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 11 verified, 5 errors
|