[klee-dev] Adding assignments to state constraints

[felicia]

Hi,

I would like to ask on how to collect assignments in the state's 
constraints.
Because currently KLEE only collect the constraints at the branch 
condition.
I have tried to add the assignment expression in the state constraints.
For example, x = x + 1 has assignment expression like this (Add w32 1 
(ReadLSB w32 0 x)).
Then, I add (Add w32 1 (ReadLSB w32 0 x)) at state constraints.
However, this way always give me an assertion error.Please let me know 
if you have any suggestion regarding this.

Thank you.