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
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
