Method clearIndices

libsolidity/formal/SMTEncoder.cpp:2710–2723

}

void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
{
	solAssert(_contract, "");
	for (auto var: stateVariablesIncludingInheritedAndPrivate(*_contract))
		m_context.variable(*var)->resetIndex();
	if (_function)
	{
		for (auto const& var: _function->parameters() + _function->returnParameters())
			m_context.variable(*var)->resetIndex();
		for (auto const& var: localVariablesIncludingModifiers(*_function, _contract))
			m_context.variable(*var)->resetIndex();
	}
	state().reset();
}

Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess)
{