summaryrefslogtreecommitdiff
path: root/src/main/interactive_shell.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/interactive_shell.cpp')
-rw-r--r--src/main/interactive_shell.cpp6
1 files changed, 5 insertions, 1 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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback