From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 21 Aug 2015 07:02:32 +0000 (-0400)
Subject: Fix bug 649 (errors to regular output channel)
X-Git-Tag: cvc5-1.0.0~6254
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0072ab29c7e9213ca6773b89e393f381bca0126;p=cvc5.git

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 a70c3c7c3..1c825bc35 100644
--- 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;
     }