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 th
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
