Opened 17 years ago
Closed 17 years ago
#52 closed defect (fixed)
matrixMultiplication compare returns false
| Reported by: | zirkel | Owned by: | ywei, zirkel |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | examples | Version: | 1.0 |
| Keywords: | examples, matrixMultiplication | Cc: |
Description (last modified by )
Compare on the matrixMultiplication returns false. The problems are:
Possible violation detected with specification at State 95
Possible incorrect final value for implementation output variable C at State 239
The complete output is too long to put here, and the text files are too big to attach.
Change History (2)
comment:1 by , 17 years ago
| Description: | modified (diff) |
|---|---|
| Summary: | matrixMultiplication → matrixMultiplication compare returns false |
comment:2 by , 17 years ago
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
Note:
See TracTickets
for help on using tickets.
I have finished translating the equality comparison of two arrays to forall expressions. The example now returns functionally equivalent.