diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp index d4dcb9df..5c0c2676 100644 --- a/src/cmd_parser.cpp +++ b/src/cmd_parser.cpp @@ -736,6 +736,14 @@ bool CmdParser::parseNextCommand() std::vector argTypes = d_eparser.parseTypeList(); Expr retType = d_eparser.parseType(); Expr progType = retType; + Expr tup = d_state.mkExpr(Kind::TUPLE, argTypes); + std::vector pargs = Expr::getVariables(tup); + Expr fv = d_eparser.findFreeVar(progType, pargs); + if (!fv.isNull()) + { + d_lex.parseError( + "Program type is not well scoped"); + } if (!argTypes.empty()) { progType = d_state.mkProgramType(argTypes, retType);