[klee-dev] Building constraints with Expr

[Papapanagiotakis-Bousy, Iason]

Hello everyone,

I have a question regarding how to build constraints with the Expr class.
The question has been asked a while ago here: https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01513.html

I am interested to build an Expr constraint given (in the simplest case) something like "x == 0", how would I do that?
I have been looking at the code in include/klee/Expr.h but it doesn't seem intuitive to me how to proceed.

My goal is to express some constraints with Expr and subsequently query the solver with the getValue() function to check whether my constraints are satisfiable on a particular state under evaluation.
If you can think any other way of achieving that without building an Expr please feel free to suggest it.

Thank you in advance.

Regards,
Jason


-------------- next part --------------
HTML attachment scrubbed and removed