diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 15:40:47 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 15:40:47 -0400 |
| commit | db271d4698a0963e8d684002a69ffbb77653c6d4 (patch) | |
| tree | d232a80e7f989b3397c116ce6783d78483d8e0ad | |
| parent | eedfa4073125ca334fa5f05265b3cd1e971b6eb0 (diff) | |
| parent | 60ae9e3334e74b04f9ad0287ecaa2a847e54ae1a (diff) | |
Merge branch '1.4.x'
| -rw-r--r-- | src/parser/smt1/Smt1.g | 8 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 3 |
2 files changed, 7 insertions, 4 deletions
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g index ae06ddc01..a885fe990 100644 --- a/src/parser/smt1/Smt1.g +++ b/src/parser/smt1/Smt1.g @@ -205,13 +205,13 @@ benchAttribute returns [CVC4::Command* smt_command = NULL] { ((CommandSequence*) smt_command)->addCommand(c); } )+ RPAREN_TOK | EXTRAPREDS_TOK LPAREN_TOK - ( { smt_command = new CommandSequence(); } - predicateDeclaration[c] + { smt_command = new CommandSequence(); } + ( predicateDeclaration[c] { ((CommandSequence*) smt_command)->addCommand(c); } )+ RPAREN_TOK | EXTRASORTS_TOK LPAREN_TOK - ( { smt_command = new CommandSequence(); } - sortDeclaration[c] + { smt_command = new CommandSequence(); } + ( sortDeclaration[c] { ((CommandSequence*) smt_command)->addCommand(c); } )+ RPAREN_TOK | NOTES_TOK STRING_LITERAL diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 421518fed..c9db1eece 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -171,6 +171,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::BUILTIN: out << smtKindString(n.getConst<Kind>()); break; + case kind::CHAIN_OP: + out << smtKindString(n.getConst<Chain>().getOperator()); + break; case kind::CONST_RATIONAL: { Rational r = n.getConst<Rational>(); if(r < 0) { |