I occasionally found some comments for `evaluate` and `mustBeTrue` methods in "include/klee/Solver/Solver.h". The explanations are clear and make much sense. For `evaluate`, the function will determine if the expression is "expression is provably true, provably false or neither." That says the `UNKNOWN` result indicates the expression could be either sat or unsat, so for such a situation, klee needs to fork the state.
Please refer to the source code https://github.com/klee/klee/blob/master/include/klee/Solver/Solver.h. On Mon, Aug 26, 2024 at 4:50 AM Nguyễn Gia Phong <c...@loang.net> wrote: > On 2024-08-25 at 20:34-07:00, Yuzhou Fang wrote: > > On 2024-08-25 at 22:23+09:00, Nguyễn Gia Phong wrote: > > > SMT solver could give up on the constraint, hence the unknown result. > > > > I'm still quite confused by the situations when solvers will give up. > > Does it mean the constraints are too hard for solvers to solve? > > Yes, and also the caller (KLEE) limits the resources (e.g. memory and time) > in each evaluation because the goal is not solving a constraint precisely, > but rather to explore many paths effectively. > > On 2024-08-25 at 20:34-07:00, Yuzhou Fang wrote: > > it seems like `UNKNOWN` indicates the constraints could be > > either sat or unsat, but I'm not sure about that (just kind of guess). > > Could you share more thoughts on this? Thanks! > > I also understand it in such literal sense. The SMT-LIB standard > doesn't seem to specify anything further than "unknown" means "not > known." >
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
