diff options
| author |  qadeer <unknown> | 2013-11-22 11:19:15 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2013-11-22 11:19:15 -0800 |
| commit | f0d11b78f3453b5cfbb524e6d0c7214442814351 (patch) | |
| tree | 9dc4edc2cba5e3e1a0cce26194bf880b8679f57d /Test/test21 | |
| parent | 479fe0571200196552e3d415ab3b90e30083b1b2 (diff) | |
do monomorphic checking
Diffstat (limited to 'Test/test21')
| -rw-r--r-- | Test/test21/Answer | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Test/test21/Answer b/Test/test21/Answer index 28aa4e8b..3ae659ec 100644 --- a/Test/test21/Answer +++ b/Test/test21/Answer @@ -400,8 +400,11 @@ Boogie program verifier finished with 1 verified, 0 errors Colors.bpl(13,3): Error BP5001: This assertion might not hold.
Execution trace:
Colors.bpl(12,3): anon0
+Colors.bpl(20,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ Colors.bpl(19,3): anon0
-Boogie program verifier finished with 1 verified, 1 error
+Boogie program verifier finished with 0 verified, 2 errors
--------------------- File HeapAbstraction.bpl ----------------------------
HeapAbstraction.bpl(15,3): Error BP5001: This assertion might not hold.
Execution trace:
|