Method divModWithSlacks

libsolidity/formal/SMTEncoder.cpp:2079–2110

}

std::pair<smtutil::Expression, smtutil::Expression> SMTEncoder::divModWithSlacks(
	smtutil::Expression _left,
	smtutil::Expression _right,
	IntegerType const& _type
)
{
	if (m_settings.divModNoSlacks)
		return {_left / _right, _left % _right};

	IntegerType const* intType = &_type;
	std::string suffix = "div_mod_" + std::to_string(m_context.newUniqueId());
	smt::SymbolicIntVariable dSymb(intType, intType, "d_" + suffix, m_context);
	smt::SymbolicIntVariable rSymb(intType, intType, "r_" + suffix, m_context);
	auto d = dSymb.currentValue();
	auto r = rSymb.currentValue();

	// x / y = d and x % y = r iff d * y + r = x and
	// either x >= 0 and 0 <= r < abs(y) (or just 0 <= r < y for unsigned)
	// or     x < 0 and -abs(y) < r <= 0
	m_context.addAssertion(((d * _right) + r) == _left);
	if (_type.isSigned())
		m_context.addAssertion(
			(_left >= 0 && 0 <= r && (_right == 0 || r < smtutil::abs(_right))) ||
			(_left < 0 && ((_right == 0 || 0 - smtutil::abs(_right) < r) && r <= 0))
		);
	else // unsigned version
		m_context.addAssertion(0 <= r && (_right == 0 || r < _right));

	auto divResult = smtutil::Expression::ite(_right == 0, 0, d);
	auto modResult = smtutil::Expression::ite(_right == 0, 0, r);
	return {divResult, modResult};
}

void SMTEncoder::assignment(Expression const& _left, smtutil::Expression const& _right)
{