Corrected z3 interface: some expressions were unhashable; replaced them with their string representation

Added a knight and knaves test to z3_examples

TODO: fix the correspondence between boole and z3 names!