Function getStateExpressionsForCall

libsolidity/formal/PredicateInstance.cpp:226–233

}

std::vector<smtutil::Expression> getStateExpressionsForCall(SymbolicState const& _state, bool _internal)
{
	if (_state.hasBytesConcatFunction())
		return {_state.errorFlag().currentValue(), _internal ? _state.thisAddress(0) : _state.thisAddress(),
			_state.abi(0), _state.bytesConcat(0), _state.crypto(0), _internal ? _state.tx(0) : _state.tx(), _state.state()};
	return {_state.errorFlag().currentValue(), _internal ? _state.thisAddress(0) : _state.thisAddress(),
			_state.abi(0), _state.crypto(0), _internal ? _state.tx(0) : _state.tx(), _state.state()};
}

std::vector<smtutil::Expression> getStateExpressionsForDefinition(SymbolicState const& _state)
{