On Sep 2, 2010, at 9:29 AM, Daniel Dunbar wrote:

> There are two major sources of non-determinism related to using OS
> timing information to make decisions. The first uses timing
> information about queries to prioritize the search. Since that
> information isn't deterministic, the search strategy can quickly
> diverge even if all other sources of non-determinism are eliminated.

I'm aware of the Klee options for what you mentioned below, but what CLI 
options should I be passing to control what you just described?

> The other source is the options to terminate the STP queries after a
> certain amount of time. It is possible that some queries will be right
> on the border and will fail in some runs and pass in others, which
> would be a major divergence. This is very unfortunate as those options
> are very important for testing most large applications.

I'll have to see if this is my problem.  Thanks.

-Denis

Reply via email to