1 files changed, 23 insertions, 0 deletions
diff --git a/Test/test1/CallForallResolve.bpl b/Test/test1/CallForallResolve.bpl
new file mode 100644
index 00000000..374db174
--- /dev/null
+++ b/Test/test1/CallForallResolve.bpl
@@ -0,0 +1,23 @@
+procedure P(x: int) returns (y: int);
+
+procedure CallP()
+{
+  call forall P(5);  // P is allowed here, even if it has out parameters
+}
+
+var global: bool;
+
+procedure Q(x: int);
+  modifies global;
+
+procedure CallQ()
+{
+  call forall Q(5);  // error: P is not allowed here, because it has a modifies clause
+}
+
+procedure R(x: int);
+
+procedure CallR()
+{
+  call forall R(5);  // no problem that R has no body, though
+}