[klee-dev] `MustBeTrue` and `evaluate` methods in solver.

[Yuzhou Fang]

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 <cnx at loang.net> 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
>
-------------- next part --------------
HTML attachment scrubbed and removed