Hi Nguyễn, Thanks for your reply!
I like to think mustBeTrue is supposed to check if the constraint > evaluates to neither false or unknown. > I think it does really make sense! Thanks a lot! 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? >From my debugging experience, the `UNKNOWN` results would appear when executing forking the states, and it seems like `UNKNOWN` indicates the constraints could either be sat or unsat, but I'm not sure about that (just kind of guess). Could you share more thoughts on this? Thanks! Yuzhou On Sun, Aug 25, 2024 at 6:23 AM Nguyễn Gia Phong <[email protected]> wrote: > Greetings, > > On 2024-08-23 at 14:12-07:00, Yuzhou Fang wrote: > > I see the return values are slightly different. Method `mustBeTrue` will > > merely return true and false while `evaluate` would give an extra > > `unknown`. Could you briefly explain the difference between them? > > SMT solver could give up on the constraint, hence the unknown result. > I like to think mustBeTrue is supposed to check if the constraint > evaluates to neither false or unknown. > > Kind regards, > Phong >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
