Add the ability to "mute" commands, needed for SMT-LIB compliance.

2 files changed, 5 insertions, 1 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a390cf452..387a24fe1 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -952,6 +952,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       std::string attr_name = attr;
       attr_name.erase( attr_name.begin() );
       Command* c = new SetUserAttributeCommand( attr_name, expr );
+      c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     } else {
       PARSER_STATE->attributeNotSupported(attr);
@@ -979,6 +980,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       // bind name to expr with define-fun
       Command* c =
         new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
+      c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     }
   ;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index e1f977890..5d104531f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -290,7 +290,9 @@ void Smt2::checkThatLogicIsSet() {
 
       setLogic("ALL_SUPPORTED");
 
-      preemptCommand(new SetBenchmarkLogicCommand("ALL_SUPPORTED"));
+      Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
+      c->setMuted(true);
+      preemptCommand(c);
     }
   }
 }