added workaround for decidability issues with z3
several bug fixes to prevent assertion failures in cast checking client on dacapo benchmarks