working version for stateful contracts
working version with additional asserts to make the axiom work
first version working with stateless contracts
start instrumenting the main C function
comment dead code with (* XXX: UNUSED *) disclaimer
another step towards refactoring
refactoring first step