projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e6f55a6) | patch
More basic fix for dumping synth-fun (#4886)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 13 Aug 2020 18:14:41 +0000 (13:14 -0500)
committerGitHub <noreply@github.com>
Thu, 13 Aug 2020 18:14:41 +0000 (13:14 -0500)
commitfb2a0d9aa09aa21f465aa8d62eab8492610052c3
tree6567fc9f3824ecf0b0aa55843db239262873ab46tree
parente6f55a60a3a65c55c04cb8bd88d47d6207677a29commit | 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.
src/smt/dump.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history