diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 09:54:15 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-17 09:54:15 -0400 |
commit | 3afbf810287fb3f1a99ef907f91f5e93c3b93226 (patch) | |
tree | 7272a8579e1dd49c18591b1edef64c9c8fad5609 /src/main | |
parent | 36dd801660bad8fe1d967c887363f15dbe1bcc63 (diff) |
Better error on illegal (pop N); also more compliant SMT-LIB error messages in some places
Thanks to David Cok for reporting these issues.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/interactive_shell.cpp | 6 | ||||
-rw-r--r-- | src/main/main.cpp | 8 |
2 files changed, 12 insertions, 2 deletions
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 3376e9d0b..5c9f8af21 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -313,7 +313,11 @@ restart: line += "\n"; goto restart; } catch(ParserException& pe) { - d_out << pe << endl; + if(d_options[options::outputLanguage] == output::LANG_SMTLIB_V2) { + d_out << "(error \"" << pe << "\")" << endl; + } else { + d_out << pe << endl; + } // We can't really clear out the sequence and abort the current line, // because the parse error might be for the second command on the // line. The first ones haven't yet been executed by the SmtEngine, diff --git a/src/main/main.cpp b/src/main/main.cpp index 7b61b48aa..a4c4b9c0a 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -37,10 +37,12 @@ #include "util/output.h" #include "util/result.h" #include "util/statistics.h" +#include "util/language.h" using namespace std; using namespace CVC4; using namespace CVC4::main; +using namespace CVC4::language; /** * CVC4's main() routine is just an exception-safe wrapper around CVC4. @@ -64,7 +66,11 @@ int main(int argc, char* argv[]) { #ifdef CVC4_COMPETITION_MODE *opts[options::out] << "unknown" << endl; #endif - *opts[options::err] << "CVC4 Error:" << endl << e << endl; + if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2) { + *opts[options::err] << "(error \"" << e << "\")" << endl; + } else { + *opts[options::err] << "CVC4 Error:" << endl << e << endl; + } if(opts[options::statistics] && pExecutor != NULL) { pTotalTime->stop(); pExecutor->flushStatistics(*opts[options::err]); |