From 49d3804de443f9f6123b1e1b64b2dca1b49034ba Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Tue, 1 Sep 2020 11:35:25 +0200
Subject: [PATCH] [SMTChecker] Fix rational number short circuit

---
 libsolidity/formal/SMTEncoder.cpp                 |  7 +++++--
 .../operators/bitwise_rational_1.sol              | 12 ++++++++++++
 .../operators/bitwise_rational_2.sol              | 15 +++++++++++++++
 3 files changed, 32 insertions(+), 2 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol

diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 8cbed6712..0418de737 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -452,11 +452,14 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 
 void SMTEncoder::endVisit(UnaryOperation const& _op)
 {
-	if (TokenTraits::isBitOp(_op.getOperator()))
-		return bitwiseNotOperation(_op);
+	/// We need to shortcut here due to potentially unknown
+	/// rational number sizes.
 	if (_op.annotation().type->category() == Type::Category::RationalNumber)
 		return;
 
+	if (TokenTraits::isBitOp(_op.getOperator()))
+		return bitwiseNotOperation(_op);
+
 	createExpr(_op);
 
 	auto const* subExpr = innermostTuple(_op.subExpression());
diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol
new file mode 100644
index 000000000..97343e235
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_1.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		uint x = uint(~1);
+		// This assertion fails because type conversion is still unsupported.
+		assert(x == 2**256 - 2);
+		assert(~1 == -2);
+	}
+}
+// ----
+// Warning 6328: (169-192): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol
new file mode 100644
index 000000000..94bb5cc83
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/bitwise_rational_2.sol
@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f() public pure {
+		assert(~1 | (~0xff & 0) == -2);
+		int x = ~1 | (~0xff ^ 0);
+		/// Result is negative, assertion fails.
+		assert(x > 0);
+		int y = ~x | (0xff & 1);
+		assert(y > 0);
+		assert(y & (0xffffffffffffffffff & 1) == 1);
+	}
+}
+// ----
+// Warning 6328: (181-194): Assertion violation happens here