diff options
| author |  MichalMoskal <unknown> | 2011-02-11 19:55:36 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-11 19:55:36 +0000 |
| commit | 1d83074ef6903514110415f24b092e52740aa7bf (patch) | |
| tree | 7b36d372ef54804923c7e4314b1b70e71162756e /Test/test2 | |
| parent | 4760c55b4a09e4b11039e9537371a98f657d7704 (diff) | |
Fix a bug in cloning of nested lambda expressions in AI engine
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)); +} + |