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

[Nguyễn Gia Phong]

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 --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 248 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20240825/468b8bd9/attachment.sig>