1 files changed, 32 insertions, 0 deletions
diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
new file mode 100644
index 00000000..27548ac9
--- /dev/null
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
@@ -0,0 +1,32 @@
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression "y > 0":
+   /!\ No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression "y < 0":
+   /!\ No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression "y > 0":
+   /!\ No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression "y < 0":
+   /!\ No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,34): Related location
+Execution trace:
+    (0,0): anon0
+splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,25): Related location
+Execution trace:
+    (0,0): anon0
+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,34): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon4_Else
+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,25): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon4_Else
+
+Dafny program verifier finished with 4 verified, 4 errors