implemented the extraction lemma (extract_dealloc and extract_alloc in lib/analysis/atomic/atomic_Utils.ml)
used it in the rules of spacial atomic commands
added two simplifications (ZeroNormalForm and BoundVarEqual) to make the resulting formulae more readable (the extraction lemma introduces lots of extra stuff, most of which gets removed by these two steps)
extract_deallocandextract_allocinlib/analysis/atomic/atomic_Utils.ml)ZeroNormalFormandBoundVarEqual) to make the resulting formulae more readable (the extraction lemma introduces lots of extra stuff, most of which gets removed by these two steps)