next up previous contents
Next: Known Bugs Up: Release Notes Previous: Version 1.6   Contents

Version 1.0

This is (was) the first version of the system for logic with equality.

In this version there are no specific redundancy provers for the cases when equality and/or ordering constraints are inherited. Also for the general case, more powerful redundancy notions are being developed.

Since ordering constraint solving is NP-complete, sometimes for very large constraints (say, more than one screen full) it is not possible to decide satisfiability in a reasonable time. In a future version some time-out mechanism has to be provided for these cases. You can circumvent the problem by setting the constraint inheritance mode to [], cf. command saci. In this case, a less complete and less time consuming constraint solving mode is applied.



Harald Ganzinger 2002-12-04

Imprint | Data Protection