[klee-dev] Question about constraint

[felicia]

Hi,

I made a simple program to produce even number for any symbolic input x.

#include <assert.h>

int even(int x) {

  if( (x % 2) == 0) x = x + 2;
  else x = x + 1;

  assert(x % 2 == 0);
  return x;
}

int main() {
   int x;
   klee_make_symbolic(&x, sizeof(x), "x");
   return even(x);
}

I tried to understand how KLEE able to reason about x whether x is even 
or not.
My question is, how the operation of addition of x is store? and later 
use for reasoning
about x in the assertion formula.

I have printed the query used by the solver, such as:
array x[4] : w32 -> w8 = symbolic
(query [(Eq 0
              (And w32 (ReadLSB w32 0 x)
                       1))]
         false []
         [x])
#   OK -- Elapsed: 2.598763e-05
#   Solvable: true
#     x = [0,0,0,0]

But, the query is quite general and does not further describe the 
constraint of x.
I expect reasoning something like x%2 == 0 implies x == x+ 2 then x 
should be even.
Where in the code I should find the reasoning like this?

Thank you very much.