diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4b8c52841..b52be77bb 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -353,8 +353,17 @@ command [std::unique_ptr<CVC4::Command>* cmd] "be declared in logic "); } // we allow overloading for function declarations - Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); - cmd->reset(new DeclareFunctionCommand(name, func, t)); + if (PARSER_STATE->sygus()) + { + // it is a higher-order universal variable + PARSER_STATE->mkSygusVar(name, t); + cmd->reset(new EmptyCommand()); + } + else + { + Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); + cmd->reset(new DeclareFunctionCommand(name, func, t)); + } } | /* function definition */ DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } |