summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r--src/parser/smt2/Smt2.g1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 05faf040e..4d39c7635 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -626,6 +626,7 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type);
// we add a declare function command here
// this is the single unmuted command in the sequence generated by this smt2 command
+ // TODO (as part of #1170) : make this a standard command.
seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type));
PARSER_STATE->pushScope(true);
for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback