> 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. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev