summaryrefslogtreecommitdiff
path: root/Test/dafny0/Char.dfy.expect
diff options
context:
space:
mode:
authorGravatar leino <unknown>2014-10-21 01:16:56 -0700
committerGravatar leino <unknown>2014-10-21 01:16:56 -0700
commitbf6de3d13197e1635a4d9fe807b3f4b45113ae6a (patch)
treec72587e9340fe59aed06852ef4b8d23dc39fba18 /Test/dafny0/Char.dfy.expect
parentc182b533a83dfee69828620f12a051feaab03eac (diff)
Comparisons and well-founded order of char
Diffstat (limited to 'Test/dafny0/Char.dfy.expect')
-rw-r--r--Test/dafny0/Char.dfy.expect16
1 files changed, 16 insertions, 0 deletions
diff --git a/Test/dafny0/Char.dfy.expect b/Test/dafny0/Char.dfy.expect
new file mode 100644
index 00000000..55418934
--- /dev/null
+++ b/Test/dafny0/Char.dfy.expect
@@ -0,0 +1,16 @@
+Char.dfy(48,21): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Then
+ (0,0): anon10_Then
+Char.dfy(52,21): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon9_Then
+ (0,0): anon11_Else
+Char.dfy(63,17): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+
+Dafny program verifier finished with 8 verified, 3 errors