From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 30 Jan 2013 20:43:33 +0000 (-0500)
Subject: correct output language bug with --dump-to
X-Git-Tag: cvc5-1.0.0~7391^2~22
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fef10dcb3dce3454adca2ef19e1c0248e968645d;p=cvc5.git

correct output language bug with --dump-to
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index a9a7ef8c5..b429ad0c2 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -180,6 +180,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
   // important even for muzzled builds (to get result output right)
   *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
+  DumpChannel.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
 
   // Create the expression manager using appropriate options
 # ifndef PORTFOLIO_BUILD