diff options
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 6 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 96c0933d8..22cf368eb 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -705,8 +705,10 @@ mainCommand[CVC4::Command*& cmd] | { PARSER_STATE->parseError("No filename given to INCLUDE command"); } ) - | ( DUMP_PROOF_TOK - | DUMP_ASSUMPTIONS_TOK + | DUMP_PROOF_TOK + { cmd = new GetProofCommand(); } + + | ( DUMP_ASSUMPTIONS_TOK | DUMP_SIG_TOK | DUMP_TCC_TOK | DUMP_TCC_ASSUMPTIONS_TOK diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 7fb671bb0..974de29b2 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -297,7 +297,7 @@ command returns [CVC4::Command* cmd = NULL] { cmd = new GetAssertionsCommand; } | /* get-proof */ GET_PROOF_TOK - { UNSUPPORTED("get-proof command not yet supported"); } + { cmd = new GetProofCommand; } | /* get-unsat-core */ GET_UNSAT_CORE_TOK { UNSUPPORTED("unsat cores not yet supported"); } |