z3 says: unsat
