Minor change to how SyGus commands are translated to SmtEngine commands. This ensures...

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 3deffe703123bb3f55f2ac61b86f7f63e9e987c8..29f5072388d6a0fc1d4d2d67c41b5e16987de0fc 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -626,6 +626,9 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
       }
       // allow overloading for synth fun
       synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type, ExprManager::VAR_FLAG_NONE, true);
+      // we add a declare function command here
+      // this is the single unmuted command in the sequence generated by this smt2 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 =
             sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
@@ -736,7 +739,10 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
         }
         std::vector<DatatypeType> datatypeTypes =
             PARSER_STATE->mkMutualDatatypeTypes(datatypes);
-        seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
+        Command * cdd = new DatatypeDeclarationCommand(datatypeTypes);
+        // we set this command muted since there should only be one success printed
+        cdd->setMuted(true);
+        seq->addCommand(cdd);
         if( sorts[0]!=range ){
           PARSER_STATE->parseError(std::string("Bad return type in grammar for "
                                                "SyGuS function ") + fun);