[UPDATE] Report added to our repository (TEX and BIBTEX). Abstract written. Z3 part started (introduction and theoretical limitations)