From 8f36408ef99038f74094d5d333c5292813aefa4a Mon Sep 17 00:00:00 2001
From: Alex Beregszaszi <alex@rtfs.hu>
Date: Fri, 11 Sep 2020 20:41:39 +0100
Subject: [PATCH 1/2] Add test case for revert() in SMTChecker

---
 .../smtCheckerTests/control_flow/revert.sol   | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/control_flow/revert.sol

diff --git a/test/libsolidity/smtCheckerTests/control_flow/revert.sol b/test/libsolidity/smtCheckerTests/control_flow/revert.sol
new file mode 100644
index 000000000..278ffc345
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/control_flow/revert.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() pure public {
+		require(false);
+		// This is not reachable.
+		assert(false);
+	}
+
+	function g() pure public {
+		revert();
+		// This is not reachable.
+		assert(false);
+	}
+}
+// ----
+// Warning 5740: (211-224): Unreachable code.
+// Warning 6328: (211-224): Assertion violation happens here.
+// Warning 4588: (171-179): Assertion checker does not yet implement this type of function call.

From 783d66c1a44cc1d26b57939f444d4aaf050712e4 Mon Sep 17 00:00:00 2001
From: Alex Beregszaszi <alex@rtfs.hu>
Date: Fri, 11 Sep 2020 20:49:04 +0100
Subject: [PATCH 2/2] [SMTChecker] Support revert()

---
 Changelog.md                                  |  1 +
 libsolidity/formal/SMTEncoder.cpp             |  4 +++
 .../smtCheckerTests/control_flow/require.sol  | 33 +++++++++++++++++++
 .../smtCheckerTests/control_flow/revert.sol   | 26 ++++++++++++---
 .../control_flow/revert_complex_flow.sol      | 18 ++++++++++
 .../constant_condition_1.sol                  |  1 -
 .../constant_condition_2.sol                  |  1 -
 .../constant_condition_3.sol                  |  1 -
 8 files changed, 77 insertions(+), 8 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/control_flow/require.sol
 create mode 100644 test/libsolidity/smtCheckerTests/control_flow/revert_complex_flow.sol

diff --git a/Changelog.md b/Changelog.md
index 779aadbeb..37ac661bd 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -5,6 +5,7 @@ Language Features:
 
 Compiler Features:
  * Export compiler-generated utility sources via standard-json or combined-json.
+ * SMTChecker: Support ``revert()``.
  * SMTChecker: Support shifts.
  * SMTChecker: Support structs.
  * SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index bf9e02010..e2a35a0d8 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -631,6 +631,10 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::Require:
 		visitRequire(_funCall);
 		break;
+	case FunctionType::Kind::Revert:
+		// Revert is a special case of require and equals to `require(false)`
+		addPathImpliedExpression(smtutil::Expression(false));
+		break;
 	case FunctionType::Kind::GasLeft:
 		visitGasLeft(_funCall);
 		break;
diff --git a/test/libsolidity/smtCheckerTests/control_flow/require.sol b/test/libsolidity/smtCheckerTests/control_flow/require.sol
new file mode 100644
index 000000000..cef9074a6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/control_flow/require.sol
@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() pure public {
+		require(false);
+		// This is not reachable.
+		assert(false);
+	}
+
+	function g() pure public {
+		require(false, "require message");
+		// This is not reachable.
+		assert(false);
+	}
+
+	function h(bool b) pure public {
+		if (b)
+			require(false);
+		assert(!b);
+	}
+
+	// Check that arguments are evaluated.
+	bool x = false;
+	function m() view internal returns (string memory) {
+		assert(x != true);
+	}
+	function i() public {
+		x = true;
+		require(false, m());
+	}
+}
+// ----
+// Warning 6328: (448-465): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/control_flow/revert.sol b/test/libsolidity/smtCheckerTests/control_flow/revert.sol
index 278ffc345..2b516c3ad 100644
--- a/test/libsolidity/smtCheckerTests/control_flow/revert.sol
+++ b/test/libsolidity/smtCheckerTests/control_flow/revert.sol
@@ -2,18 +2,34 @@ pragma experimental SMTChecker;
 
 contract C {
 	function f() pure public {
-		require(false);
+		revert();
 		// This is not reachable.
 		assert(false);
 	}
 
 	function g() pure public {
-		revert();
+		revert("revert message");
 		// This is not reachable.
 		assert(false);
 	}
+
+	function h(bool b) pure public {
+		if (b)
+			revert();
+		assert(!b);
+	}
+
+	// Check that arguments are evaluated.
+	bool x = false;
+	function m() view internal returns (string memory) {
+		assert(x != true);
+	}
+	function i() public {
+		x = true;
+		revert(m());
+	}
 }
 // ----
-// Warning 5740: (211-224): Unreachable code.
-// Warning 6328: (211-224): Assertion violation happens here.
-// Warning 4588: (171-179): Assertion checker does not yet implement this type of function call.
+// Warning 5740: (116-129): Unreachable code.
+// Warning 5740: (221-234): Unreachable code.
+// Warning 6328: (427-444): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/control_flow/revert_complex_flow.sol b/test/libsolidity/smtCheckerTests/control_flow/revert_complex_flow.sol
new file mode 100644
index 000000000..35a0132a0
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/control_flow/revert_complex_flow.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool b, uint a) pure public {
+		require(a <= 256);
+		if (b)
+			revert();
+		uint c = a + 1;
+		if (b)
+			c--;
+		else
+			c++;
+		assert(c == a);
+	}
+}
+// ----
+// Warning 6328: (183-197): Assertion violation happens here.
+// Warning 6838: (155-156): Condition is always false.
diff --git a/test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol
index 00060c778..d64fc8fd5 100644
--- a/test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol
+++ b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_1.sol
@@ -6,4 +6,3 @@ contract C {
 }
 // ----
 // Warning 6838: (94-100): Condition is always true.
-// Warning 4588: (104-112): Assertion checker does not yet implement this type of function call.
diff --git a/test/libsolidity/smtCheckerTests/verification_target/constant_condition_2.sol b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_2.sol
index 9d52fa7c5..68f4bd8b2 100644
--- a/test/libsolidity/smtCheckerTests/verification_target/constant_condition_2.sol
+++ b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_2.sol
@@ -6,4 +6,3 @@ contract C {
 }
 // ----
 // Warning 6838: (109-115): Condition is always false.
-// Warning 4588: (119-127): Assertion checker does not yet implement this type of function call.
diff --git a/test/libsolidity/smtCheckerTests/verification_target/constant_condition_3.sol b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_3.sol
index ba6b7f0f6..709fcb1b4 100644
--- a/test/libsolidity/smtCheckerTests/verification_target/constant_condition_3.sol
+++ b/test/libsolidity/smtCheckerTests/verification_target/constant_condition_3.sol
@@ -6,4 +6,3 @@ contract C {
     }
 }
 // ----
-// Warning 4588: (136-144): Assertion checker does not yet implement this type of function call.