KNOWN ISSUES with Kind...

(02/11/2009)

(Operation)

- Command line Yices has a limited buffer for its interactive mode.  It is 
recommended that you use the wrapper version if possible.

- By default Yices does little, if any, type checking.  On the off chance
that a typing issue gets past Kind and reaches Yices, it will probably
abort with an unhelpful error message (if at all).  Try running the resulting

- CVC3 can encounter a number of errors.  The most prominent of these is
a failure to instantiate some models, which breaks the Kind's abstraction/
refinement process with an Abort message (and possibly a not very intuitive
error message from the solver).  Try re-running without abstraction.

- Sometimes the solver will get stuck in its search.  Sorry, not much help 
for this.  Maybe try some alternate command flags for the solver to alter
its search behavior.

- Very large problems (especially with the -aggdef option) can run afoul
of various I/O buffer limitations.  This could result in Kind entering a
perpetual wait-state.  You can try using the -buffer_limit command line 
option.

- Currently lustre identifiers are only differenetiated out to 100 characters.

(Coding)

- Currently there is a certain amount of unnecessary backtracking done in the
induction process (due to previous investigation) that needs to be cleared
out.  Mostly this will be a question of altering loop parameters as 
appropriate, but missing one will introduce unsoundness or crashes.

- Indexing could be shifted to positive -- this may allow us to be more
incrementally efficient (may not shift globally -- currently assumed negative
indexing).

- CVC3 is having trouble with producing unsatisfiable cores (DUMP_ASSUMPTIONS).
Currently there is a work-around in place (treat all asserted variables as
the core), but this is highly inefficient from the refinement standpoint (at 
least assuming getting a core from CVC3 is not too intensive -- if nothing 
else, this process is simple and fast).

- Identifiers are current (32-bit) ints, so it is possible to exhaust
this on very, very large problems.

- Overall structure could use work, and could eliminate global variables
(though possibly at the cost of unwieldy function calls).  Too imperative.

- Several additions/modifications are planned.
