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
signature.asc
Description: PGP signature
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
