fixed Z3-related bug (implication check was checking if a satisfying assignment existed rather than checking if implication held for all values)