Bug #59
Account for k-max in trace-checking engines
| Status: | New | Start date: | 09/08/2011 | |
|---|---|---|---|---|
| Priority: | Normal | Due date: | ||
| Assignee: | Grégoire Sutre | % Done: | 0% |
|
| Category: | - | |||
| Target version: | 1.3 |
Description
Trace-checking engines APInv/UPInv should abort if they must increase k beyond k_max to compute a trace invariant.