1 files changed, 77 insertions, 0 deletions
diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect
new file mode 100644
index 00000000..545289b8
--- /dev/null
+++ b/Test/dafny0/FunctionSpecifications.dfy.expect
@@ -0,0 +1,77 @@
+FunctionSpecifications.dfy(35,25): Error BP5003: A postcondition might not hold on this return path.
+FunctionSpecifications.dfy(31,13): Related location: This is the postcondition that might not hold.
+Execution trace:
+    (0,0): anon0
+    (0,0): anon8_Else
+    (0,0): anon9_Else
+    (0,0): anon10_Then
+    (0,0): anon11_Else
+FunctionSpecifications.dfy(45,3): Error BP5003: A postcondition might not hold on this return path.
+FunctionSpecifications.dfy(40,24): Related location: This is the postcondition that might not hold.
+Execution trace:
+    (0,0): anon0
+    (0,0): anon11_Else
+    (0,0): anon14_Else
+    (0,0): anon15_Then
+FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+    (0,0): anon0
+    (0,0): anon8_Then
+    (0,0): anon3
+FunctionSpecifications.dfy(59,10): Error BP5003: A postcondition might not hold on this return path.
+FunctionSpecifications.dfy(60,22): Related location: This is the postcondition that might not hold.
+Execution trace:
+    (0,0): anon0
+    (0,0): anon5_Else
+FunctionSpecifications.dfy(108,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+FunctionSpecifications.dfy(111,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+FunctionSpecifications.dfy(126,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+FunctionSpecifications.dfy(130,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Else
+FunctionSpecifications.dfy(153,15): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+FunctionSpecifications.dfy(165,3): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Else
+FunctionSpecifications.dfy(172,15): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+FunctionSpecifications.dfy(181,3): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Else
+FunctionSpecifications.dfy(135,20): Error BP5003: A postcondition might not hold on this return path.
+FunctionSpecifications.dfy(137,29): Related location: This is the postcondition that might not hold.
+Execution trace:
+    (0,0): anon0
+    (0,0): anon5_Then
+    (0,0): anon2
+    (0,0): anon6_Else
+FunctionSpecifications.dfy(146,3): Error: failure to decrease termination measure
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Else
+FunctionSpecifications.dfy(160,3): Error: failure to decrease termination measure
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Else
+FunctionSpecifications.dfy(188,3): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Else
+FunctionSpecifications.dfy(185,20): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 19 verified, 17 errors