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