[SMTChecker] Use smtlib's implies instead of \!a or b

libsolidity/formal/CVC4Interface.cpp

@@ -145,6 +145,8 @@ CVC4::Expr CVC4Interface::toCVC4Expr(Expression const& _expr)
 		return arguments[0].andExpr(arguments[1]);
 	else if (n == "or")
 		return arguments[0].orExpr(arguments[1]);
+	else if (n == "implies")
+		return m_context.mkExpr(CVC4::kind::IMPLIES, arguments[0], arguments[1]);
 	else if (n == "=")
 		return m_context.mkExpr(CVC4::kind::EQUAL, arguments[0], arguments[1]);
 	else if (n == "<")

libsolidity/formal/SolverInterface.h

@@ -133,6 +133,7 @@ public:
 			{"not", 1},
 			{"and", 2},
 			{"or", 2},
+			{"implies", 2},
 			{"=", 2},
 			{"<", 2},
 			{"<=", 2},
@@ -160,7 +161,12 @@ public:
 
 	static Expression implies(Expression _a, Expression _b)
 	{
-		return !std::move(_a) || std::move(_b);
+		return Expression(
+			"implies",
+			std::move(_a),
+			std::move(_b),
+			Kind::Bool
+		);
 	}
 
 	/// select is the SMT representation of an array index access.

libsolidity/formal/Z3Interface.cpp

@@ -144,6 +144,8 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		return arguments[0] && arguments[1];
 	else if (n == "or")
 		return arguments[0] || arguments[1];
+	else if (n == "implies")
+		return z3::implies(arguments[0], arguments[1]);
 	else if (n == "=")
 		return arguments[0] == arguments[1];
 	else if (n == "<")