HomeIsabelle/Phabricator

Elimination of all z3 calls