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

[Nguyễn Gia Phong]

On 2024-08-25 at 20:34-07:00, Yuzhou Fang wrote:
> On 2024-08-25 at 22:23+09:00, Nguyễn Gia Phong wrote:
> > SMT solver could give up on the constraint, hence the unknown result.
>
> I'm still quite confused by the situations when solvers will give up.
> Does it mean the constraints are too hard for solvers to solve?

Yes, and also the caller (KLEE) limits the resources (e.g. memory and time)
in each evaluation because the goal is not solving a constraint precisely,
but rather to explore many paths effectively.

On 2024-08-25 at 20:34-07:00, Yuzhou Fang wrote:
> it seems like `UNKNOWN` indicates the constraints could be
> either sat or unsat, but I'm not sure about that (just kind of guess).
> Could you share more thoughts on this? Thanks!

I also understand it in such literal sense.  The SMT-LIB standard
doesn't seem to specify anything further than "unknown" means "not
known."
-------------- 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/20240826/718d97cd/attachment.sig>