Spacer reimplementation of a part of the Spacer model checker using Z3 and OCaml (this project still have a few bugs to fix)