Method arithmeticOperation

libsolidity/formal/SMTEncoder.cpp:1815–1845

}

void SMTEncoder::arithmeticOperation(BinaryOperation const& _op)
{
	auto type = _op.annotation().commonType;
	solAssert(type, "");
	solAssert(type->category() == Type::Category::Integer || type->category() == Type::Category::FixedPoint, "");
	switch (_op.getOperator())
	{
	case Token::Add:
	case Token::Sub:
	case Token::Mul:
	case Token::Div:
	case Token::Mod:
	{
		auto values = arithmeticOperation(
			_op.getOperator(),
			expr(_op.leftExpression()),
			expr(_op.rightExpression()),
			_op.annotation().commonType,
			_op
		);
		defineExpr(_op, values.first);
		break;
	}
	default:
		m_unsupportedErrors.warning(
			5188_error,
			_op.location(),
			"Assertion checker does not yet implement this operator."
		);
	}
}

std::pair<smtutil::Expression, smtutil::Expression> SMTEncoder::arithmeticOperation(
	Token _op,