From b57b8daf0ac6ca303a31cc30b8e128b14b74676a Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Tue, 18 May 2021 19:15:08 +0200
Subject: [PATCH] Replace implies by =>

---
 libsmtutil/CVC4Interface.cpp | 2 +-
 libsmtutil/SolverInterface.h | 4 ++--
 libsmtutil/Z3Interface.cpp   | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/libsmtutil/CVC4Interface.cpp b/libsmtutil/CVC4Interface.cpp
index daac2ab71..bdde4eefe 100644
--- a/libsmtutil/CVC4Interface.cpp
+++ b/libsmtutil/CVC4Interface.cpp
@@ -170,7 +170,7 @@ 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")
+		else if (n == "=>")
 			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]);
diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h
index fb2fa643d..5fdcf2694 100644
--- a/libsmtutil/SolverInterface.h
+++ b/libsmtutil/SolverInterface.h
@@ -86,7 +86,7 @@ public:
 			{"not", 1},
 			{"and", 2},
 			{"or", 2},
-			{"implies", 2},
+			{"=>", 2},
 			{"=", 2},
 			{"<", 2},
 			{"<=", 2},
@@ -126,7 +126,7 @@ public:
 	static Expression implies(Expression _a, Expression _b)
 	{
 		return Expression(
-			"implies",
+			"=>",
 			std::move(_a),
 			std::move(_b),
 			Kind::Bool
diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp
index 8d7a03392..b7831297b 100644
--- a/libsmtutil/Z3Interface.cpp
+++ b/libsmtutil/Z3Interface.cpp
@@ -189,7 +189,7 @@ 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")
+		else if (n == "=>")
 			return z3::implies(arguments[0], arguments[1]);
 		else if (n == "=")
 			return arguments[0] == arguments[1];