Merge pull request #10636 from ethereum/smt_fix_constant

Fix constant evaluation build

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,20 +2656,20 @@ 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.
 	// In that case we ignore any warnings emitted by the constant evaluator,
 	// 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)

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,

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);
+	}
+}