Merge pull request #6635 from ethereum/smt_fix_fixedpoint

[SMTChecker] Fix ICE in fixed point operations

Changelog.md

@@ -10,6 +10,7 @@ Compiler Features:
 Bugfixes:
  * SMTChecker: Fix bad cast in base constructor modifier.
  * SMTChecker: Fix internal error when visiting state variable inherited from base class.
+ * SMTChecker: Fix internal error in fixed point operations.
 
 
 

libsolidity/formal/SMTChecker.cpp

@@ -1050,29 +1050,39 @@ bool SMTChecker::shortcutRationalNumber(Expression const& _expr)
 
 void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
 {
-	switch (_op.getOperator())
+	auto type = _op.annotation().commonType;
+	solAssert(type, "");
+	if (type->category() == Type::Category::Integer)
 	{
-	case Token::Add:
+		switch (_op.getOperator())
-	case Token::Sub:
+		{
-	case Token::Mul:
+		case Token::Add:
-	case Token::Div:
+		case Token::Sub:
-	case Token::Mod:
+		case Token::Mul:
-	{
+		case Token::Div:
-		defineExpr(_op, arithmeticOperation(
+		case Token::Mod:
-			_op.getOperator(),
+		{
-			expr(_op.leftExpression()),
+			defineExpr(_op, arithmeticOperation(
-			expr(_op.rightExpression()),
+				_op.getOperator(),
-			_op.annotation().commonType,
+				expr(_op.leftExpression()),
-			_op.location()
+				expr(_op.rightExpression()),
-		));
+				_op.annotation().commonType,
-		break;
+				_op.location()
+			));
+			break;
+		}
+		default:
+			m_errorReporter.warning(
+				_op.location(),
+				"Assertion checker does not yet implement this operator."
+			);
+		}
 	}
-	default:
+	else
 		m_errorReporter.warning(
 			_op.location(),
-			"Assertion checker does not yet implement this operator."
+			"Assertion checker does not yet implement this operator for type " + type->richIdentifier() + "."
 		);
-	}
 }
 
 smt::Expression SMTChecker::arithmeticOperation(