o changed the tools
o made the comp-calc test pass by updating Z3 and adding a theory of predicate calculus (Dijkstra style