1 files changed, 95 insertions, 0 deletions
diff --git a/Test/dafny0/Fuel.dfy.expect b/Test/dafny0/Fuel.dfy.expect
new file mode 100644
index 00000000..4c180a9c
--- /dev/null
+++ b/Test/dafny0/Fuel.dfy.expect
@@ -0,0 +1,95 @@
+Fuel.dfy(17,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(65,28): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon6_Else
+Fuel.dfy(69,28): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon6_Then
+    (0,0): anon7_Then
+Fuel.dfy(92,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(94,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(120,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(122,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(129,39): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(132,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+Fuel.dfy(133,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+Fuel.dfy(157,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon10_Else
+    (0,0): anon9
+Fuel.dfy(200,56): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(245,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(247,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(280,27): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Then
+Fuel.dfy(335,27): Error: possible violation of function precondition
+Fuel.dfy(324,22): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(335,50): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(335,51): Error: index out of range
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(336,39): Error: index out of range
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(336,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(346,43): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+    (0,0): anon8_Then
+Fuel.dfy(397,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(398,23): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+Fuel.dfy(407,39): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 51 verified, 24 errors