diff options
Diffstat (limited to 'src/parser/cvc')
-rw-r--r-- | src/parser/cvc/Cvc.g | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index d1fcc4e06..b504d290b 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -935,15 +935,8 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd] PARSER_STATE->parseError("Type mismatch in definition"); } } - std::vector<std::vector<Expr>> eformals; - for (unsigned i=0, fsize = formals.size(); i<fsize; i++) - { - eformals.push_back(api::termVectorToExprs(formals[i])); - } cmd->reset( - new DefineFunctionRecCommand(api::termVectorToExprs(funcs), - eformals, - api::termVectorToExprs(formulas), true)); + new DefineFunctionRecCommand(SOLVER, funcs, formals, formulas, true)); } | toplevelDeclaration[cmd] ; |