diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-21 14:30:32 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-21 16:25:13 -0400 |
commit | ed40bbae19622ff29e1ca6eb873d20262ed21926 (patch) | |
tree | a3f1954f8311cf96a5a30eadf59786e80b8693c4 /src/parser/smt2/Smt2.g | |
parent | 332772cb9ec225587d2107881d3b6f119e332b84 (diff) |
Add the ability to "mute" commands, needed for SMT-LIB compliance.
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 2 |
1 files changed, 2 insertions, 0 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); } ; |