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


_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to