diff options
Diffstat (limited to 'Test/linear/f1.bpl')
| -rw-r--r-- | Test/linear/f1.bpl | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/linear/f1.bpl b/Test/linear/f1.bpl index e18fab9f..0d255149 100644 --- a/Test/linear/f1.bpl +++ b/Test/linear/f1.bpl @@ -21,7 +21,7 @@ axiom(!b6); axiom(!b7);
axiom(b8);
-procedure {:entrypoint} main({:linear "1"} x_in: [int]bool)
+procedure main({:linear_in "1"} x_in: [int]bool)
requires b0 ==> x_in == mapconstbool(true);
requires b1 ==> x_in != mapconstbool(false);
{
@@ -35,7 +35,7 @@ procedure {:entrypoint} main({:linear "1"} x_in: [int]bool) assert b8 ==> x == mapconstbool(false);
}
-procedure foo({:linear "1"} x_in: [int]bool)
+procedure foo({:linear_in "1"} x_in: [int]bool)
requires b2 ==> x_in == mapconstbool(true);
requires b3 ==> x_in != mapconstbool(false);
{
|