Function interface

libsolidity/formal/PredicateInstance.cpp:36–41

}

smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{
	auto const& state = _context.state();
	std::vector<smtutil::Expression> stateExprs = getStateExpressionsForInterface(state);
	return _pred(stateExprs + currentStateVariables(_contract, _context));
}

smtutil::Expression nondetInterface(
	Predicate const& _pred,