From f5c96ea6dad22b75f4305852cdc501d6fee92b4d Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 16 Dec 2020 17:58:49 +0100
Subject: [PATCH] Fix constant evaluation build

---
 libsolidity/formal/SMTEncoder.cpp             | 24 +++++++++----------
 libsolidity/formal/SMTEncoder.h               |  2 +-
 .../operators/constant_propagation_2.sol      | 14 +++++++++++
 3 files changed, 26 insertions(+), 14 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/operators/constant_propagation_2.sol

diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index da91d799548f..8b7bbcc8e0d3 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1626,16 +1626,14 @@ void SMTEncoder::defineGlobalVariable(string const& _name, Expression const& _ex
 
 bool SMTEncoder::shortcutRationalNumber(Expression const& _expr)
 {
-	auto type = isConstant(_expr);
-	if (!type)
+	RationalNumberType const* rationalType = isConstant(_expr);
+	if (!rationalType)
 		return false;
 
-	solAssert(type->category() == Type::Category::RationalNumber, "");
-	auto const& rationalType = dynamic_cast<RationalNumberType const&>(*type);
-	if (rationalType.isNegative())
-		defineExpr(_expr, smtutil::Expression(u2s(rationalType.literalValue(nullptr))));
+	if (rationalType->isNegative())
+		defineExpr(_expr, smtutil::Expression(u2s(rationalType->literalValue(nullptr))));
 	else
-		defineExpr(_expr, smtutil::Expression(rationalType.literalValue(nullptr)));
+		defineExpr(_expr, smtutil::Expression(rationalType->literalValue(nullptr)));
 	return true;
 }
 
@@ -2658,12 +2656,9 @@ map<ContractDefinition const*, vector<ASTPointer<frontend::Expression>>> SMTEnco
 	return baseArgs;
 }
 
-TypePointer SMTEncoder::isConstant(Expression const& _expr)
+RationalNumberType const* SMTEncoder::isConstant(Expression const& _expr)
 {
-	if (
-		auto type = _expr.annotation().type;
-		type->category() == Type::Category::RationalNumber
-	)
+	if (auto type = dynamic_cast<RationalNumberType const*>(_expr.annotation().type))
 		return type;
 
 	// _expr may not be constant evaluable.
@@ -2671,7 +2666,10 @@ TypePointer SMTEncoder::isConstant(Expression const& _expr)
 	// as it will return nullptr in case of failure.
 	ErrorList l;
 	ErrorReporter e(l);
-	return ConstantEvaluator(e).evaluate(_expr);
+	if (auto t = ConstantEvaluator::evaluate(e, _expr))
+		return TypeProvider::rationalNumber(t->value);
+
+	return nullptr;
 }
 
 void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index b6f65bcd7511..14a1556d59bb 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -85,7 +85,7 @@ class SMTEncoder: public ASTConstVisitor
 
 	/// @returns a valid RationalNumberType pointer if _expr has type
 	/// RationalNumberType or can be const evaluated, and nullptr otherwise.
-	static TypePointer isConstant(Expression const& _expr);
+	static RationalNumberType const* isConstant(Expression const& _expr);
 
 protected:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
diff --git a/test/libsolidity/smtCheckerTests/operators/constant_propagation_2.sol b/test/libsolidity/smtCheckerTests/operators/constant_propagation_2.sol
new file mode 100644
index 000000000000..2aadde8e93de
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/constant_propagation_2.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint constant x = 7;
+	uint constant y = 3;
+	uint constant z = x / y;
+
+	function f() public pure {
+		assert(z == 2);
+		assert(z == x / 3);
+		assert(z == 7 / y);
+		assert(z * 3 != 7);
+	}
+}