Guards

src/cmd_parser.cpp

@@ -509,12 +509,20 @@ bool CmdParser::parseNextCommand()
         // not builtin symbols, thus we must assume they are defined by the user.
         // We assume that a symbol named "=" has been defined.
         Expr eq = d_state.getVar("=");
+        if (eq.isNull())
+        {
+          d_lex.parseError("Expected symbol '=' to be defined when parsing define-fun.");
+        }
         Expr rhs = expr;
         Expr t = ret;
         if (!vars.empty())
         {
           // We assume that a symbol named "lambda" has been defined as a binder.
           Expr lambda = d_state.getVar("lambda");
+          if (lambda.isNull())
+          {
+            d_lex.parseError("Expected symbol 'lambda' to be defined when parsing define-fun.");
+          }
           Expr bvl = d_state.mkBinderList(lambda.getValue(), vars);
           rhs = d_state.mkExpr(Kind::APPLY, {lambda, bvl, rhs});
           std::vector<Expr> types;