diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-13 13:14:41 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-13 13:14:41 -0500 |
commit | fb2a0d9aa09aa21f465aa8d62eab8492610052c3 (patch) | |
tree | 6567fc9f3824ecf0b0aa55843db239262873ab46 /src/smt/smt_engine.cpp | |
parent | e6f55a60a3a65c55c04cb8bd88d47d6207677a29 (diff) |
More basic fix for dumping synth-fun (#4886)
The commit (079a04b) appears to have broken the nightlies due to compile issues related a necessary addition to the Dump class (so that std::string could be printing on Dump streams).
This changes the temporary solution so that we simply print a string on the standard output, when the Dump is enabled. This is required for temporarily keeping dump=raw-benchmark working for synth-fun commands.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7f6d3db9d..7374c8ca9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1350,8 +1350,11 @@ void SmtEngine::declareSynthFun(const std::string& id, : TypeNode::fromType(func.getType()), isInv, TypeNode::fromType(sygusType)); - - Dump("raw-benchmark") << ss.str(); + + // must print it on the standard output channel since it is not possible + // to print anything except for commands with Dump. + std::ostream& out = *d_options.getOut(); + out << ss.str() << std::endl; } // sygus conjecture is now stale |