Fix bug 649 (errors to regular output channel)

From SMTLIB standard:

  "Regular output, including error messages, is printed on the
   regular output channel..."

For CVC language, the behavior is unchanged (i.e. errors go
to stderr by default).

diff --git a/src/main/main.cpp b/src/main/main.cpp
index a70c3c7c31036b4777ca4b90c74125e2db9dbcac..1c825bc35e14615417c592fd056553035efe959d 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -67,7 +67,7 @@ int main(int argc, char* argv[]) {
 #endif
     if(opts[options::outputLanguage] == output::LANG_SMTLIB_V2_0 ||
        opts[options::outputLanguage] == output::LANG_SMTLIB_V2_5) {
-      *opts[options::err] << "(error \"" << e << "\")" << endl;
+      *opts[options::out] << "(error \"" << e << "\")" << endl;
     } else {
       *opts[options::err] << "CVC4 Error:" << endl << e << endl;
     }