diff options
Diffstat (limited to 'Test/test2')
| -rw-r--r-- | Test/test2/Answer | 4 | ||||
| -rw-r--r-- | Test/test2/Lambda.bpl | 8 |
2 files changed, 10 insertions, 2 deletions
diff --git a/Test/test2/Answer b/Test/test2/Answer index ca050273..f9d9a92e 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -363,7 +363,7 @@ Lambda.bpl(38,3): Error BP5001: This assertion might not hold. Execution trace:
Lambda.bpl(36,5): anon0
-Boogie program verifier finished with 4 verified, 2 errors
+Boogie program verifier finished with 5 verified, 2 errors
-------------------- LambdaPoly.bpl --------------------
LambdaPoly.bpl(28,5): Error BP5001: This assertion might not hold.
@@ -419,7 +419,7 @@ Lambda.bpl(38,3): Error BP5001: This assertion might not hold. Execution trace:
Lambda.bpl(36,5): anon0
-Boogie program verifier finished with 4 verified, 2 errors
+Boogie program verifier finished with 5 verified, 2 errors
-------------------- TypeEncodingM.bpl /typeEncoding:m --------------------
TypeEncodingM.bpl(24,3): Error BP5001: This assertion might not hold.
diff --git a/Test/test2/Lambda.bpl b/Test/test2/Lambda.bpl index 177900f4..477d0f36 100644 --- a/Test/test2/Lambda.bpl +++ b/Test/test2/Lambda.bpl @@ -55,3 +55,11 @@ procedure a() assert diff(a,b)[1]; assert !diff(a,b)[2]; } + +procedure nestedLambda() +{ + var a: [int][int]int; + + a := (lambda x: int :: (lambda y: int :: x+y)); +} + |