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

[Yuzhou Fang]

Dear Klee community,

I was recently reading the source code of `klee` and found that there are
two methods `mustBeTrue` and `evaluate` of class `TimingSolver`, which are
both used to determine the satisfiability of constraints.

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? I see
`evaluate` is used when state forking and `mustBeTrue` is for finding a
concrete solution. Can I say that the appropriate option to determine the
sat of constraints is to use `mustBeTrue`? Is `evaluate` only used to
determine the feasibility of then and else branches when forking? Thank you!

Best regards,
Yuzhou Fang
-------------- next part --------------
HTML attachment scrubbed and removed