From fef10dcb3dce3454adca2ef19e1c0248e968645d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 30 Jan 2013 15:43:33 -0500 Subject: [PATCH] correct output language bug with --dump-to --- src/main/driver_unified.cpp | 1 + 1 file changed, 1 insertion(+) 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 -- 2.30.2