Known Issues for KeY 1.6.0
==========================
 
1) No support for recursion
    
    Description: 

    Recursive methods cannot be proven.

    Workaround: n/a

    Plan: 

      Proof obligations for recursive methods will be released in one
      of the next technical preview versions.

2) Proof cannot be loaded

   Description: 

     Loading of a proof fails.

   Workaround: 

     First make sure that you haven't changed anything in your
     implementation or specification. If this is not the case, there
     are some situations where saving and loading of proofs fails, but
     in most cases the saved proof can be recovered by manual
     editing. Please ask the KeY team for support.

3) Variable renaming confusing

   Description: 

     Introduction of new variable names and renaming lack transparency.
   
   Explanation: 

     When introducing new program variables the chosen names have to
     be unique. In order to guarantee this, names of the kind
     "basename#number" are introduced. When the declaration of such a
     new variable is removed by symbolic execution, renaming takes
     place in order to get rid of the hash symbol.
   
   Plan: 

     The process of renaming is sound thus it is not a real bug, but
     this kind of implicit renaming may confuse the user. We need to
     collect more experience.

4) Correctness proof obligations for taclets are unsound.

   Description: 

     Not all taclet features are supported by the generator of proof
     obligations that ensure soundness of user-defined lemma
     taclets. Taclets with such unsupported feature are not in all
     cases rejected, however. This makes it possible to load unsound
     taclets as lemmas during a proof.

   Plan: 

     The check will be made restrictive so that only proof-obligations 
     for taclets are generated that can be actually treated.

5) Eclipse plug-in only usable for Linux


6) Some JML features from KeY 1.2 are missing (e.g. history
constraints)
   

7) Missing GUI support for classpath directive and other project
settings