[klee-dev] Klee path statistics and merging options

[Dan Liew]

> Is the number of completed paths same as number of feasible paths in the
> program ?
>
> 2> Does Klee invoke a SAT query at every branch point in the program by
> default to determine
> the eager infeasibility of a path ? Or is there other heuristics to
> selectively chose branch points ?

AFAIK KLEE issues a query at every branch point. This does not
necessarily trigger a call to the underlying solver though as KLEE has
some caching mechanisms that may fire.

> 3>  Does Klee support SAT solvers in the backend like MiniSAT etc ?

You are looking at the wrong level. KLEE works at the level of SMT
solvers, not SAT solvers as it needs a logic over bitvectors, not
booleans. Typically an SMT solver will be implemented in terms of a
SAT solver but KLEE does not know this. STP itself supports two
backends MiniSat and CryptoMinisat4. KLEE doesn't currently set the
backend to use in STP but support could be added. I would happily
review a pull request that added this.

KLEE supports a few other SMT solvers via the MetaSMT interface
(untested) and I am currently working on native Z3 support.

> believe that the default SMT solver
> used is STP. The follow-up to this question is that are there options to
> dump the path-constraints
> in DIMACS format to use with a SAT solver.

KLEE supports emission of the constraints in its own custom language
(KQuery) and as SMT-LIBv2.

HTH,
Dan.