Function nondetInterfaceSort

libsolidity/formal/PredicateSort.cpp:41–54

}

SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
{
	auto varSorts = stateSorts(_contract);
	std::vector<SortPointer> stateSort{_state.stateSort()};
	return std::make_shared<FunctionSort>(
		std::vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort()} +
			getBuiltInFunctionsSorts(_state) +
			stateSort +
			varSorts +
			stateSort +
			varSorts,
		SortProvider::boolSort
	);
}

SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState& _state)
{