Clean up and devellop z3 translation. Now models are supported by Boole. Begin evaluation in boole, change defenumtype -> defenum.