summaryrefslogtreecommitdiff
path: root/src/parser/cvc
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/cvc')
-rw-r--r--src/parser/cvc/Cvc.g4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index e604c7769..5d04a8cc0 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -943,7 +943,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
cmd->reset(
new DefineFunctionRecCommand(api::termVectorToExprs(funcs),
eformals,
- api::termVectorToExprs(formulas)));
+ api::termVectorToExprs(formulas), true));
}
| toplevelDeclaration[cmd]
;
@@ -1163,7 +1163,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
PARSER_STATE->defineVar(*i, f);
Command* decl =
- new DefineFunctionCommand(*i, func.getExpr(), f.getExpr());
+ new DefineFunctionCommand(*i, func.getExpr(), f.getExpr(), true);
seq->addCommand(decl);
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback