GPUVerify: use a Formal for procedure predicates

1 files changed, 4 insertions, 3 deletions

diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/GPUVerify/BlockPredicator.cs
index 80d97ebc..99c36af7 100644
--- a/Source/GPUVerify/BlockPredicator.cs
+++ b/Source/GPUVerify/BlockPredicator.cs
@@ -195,9 +195,10 @@ class BlockPredicator {
     foreach (var decl in p.TopLevelDeclarations) {
       if (decl is DeclWithFormals && !(decl is Function)) {
         var dwf = (DeclWithFormals)decl;
-        var fpVar = new LocalVariable(Token.NoToken,
-                                    new TypedIdent(Token.NoToken, "fp",
-                                                   Microsoft.Boogie.Type.Bool));
+        var fpVar = new Formal(Token.NoToken,
+                               new TypedIdent(Token.NoToken, "fp",
+                                              Microsoft.Boogie.Type.Bool),
+                               /*incoming=*/true);
         dwf.InParams = new VariableSeq((dwf.InParams + new VariableSeq(fpVar))
                        .Cast<Variable>().ToArray());
       }