summaryrefslogtreecommitdiff
path: root/src/main
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-01-30 15:43:33 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-01-30 15:43:56 -0500
commitfef10dcb3dce3454adca2ef19e1c0248e968645d (patch)
tree85c0045681b61b8439a58f308e06bebc9df04420 /src/main
parentdb1bbaa13a0cba41e3176441d0b816088fd964ce (diff)
correct output language bug with --dump-to
Diffstat (limited to 'src/main')
-rw-r--r--src/main/driver_unified.cpp1
1 files changed, 1 insertions, 0 deletions
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback