Bug #59

Account for k-max in trace-checking engines

Added by Grégoire Sutre over 5 years ago.

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.

Also available in: Atom PDF