Skip to content

Commit d4ed123

Browse files
authored
Merge pull request #222 from diffblue/ebmc-smt2-no-outfile
ebmc: send output for --smt2 to console when no --outfile is given
2 parents e429921 + d950892 commit d4ed123

File tree

1 file changed

+23
-10
lines changed

1 file changed

+23
-10
lines changed

src/ebmc/ebmc_solver_factory.cpp

Lines changed: 23 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -110,16 +110,29 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
110110
if(smt2_solver.has_value())
111111
{
112112
return
113-
[smt2_solver](const namespacet &ns, message_handlert &message_handler)
114-
{
115-
return ebmc_solvert{std::make_unique<smt2_dect>(
116-
ns,
117-
"ebmc",
118-
"Generated by EBMC " EBMC_VERSION,
119-
"QF_AUFBV",
120-
smt2_solver.value(),
121-
message_handler)};
122-
};
113+
[smt2_solver](const namespacet &ns, message_handlert &message_handler) {
114+
if(smt2_solver == smt2_convt::solvert::GENERIC)
115+
{
116+
// --smt2 but no --outfile given. Send to std::cout.
117+
return ebmc_solvert{std::make_unique<smt2_convt>(
118+
ns,
119+
"ebmc",
120+
"Generated by EBMC " EBMC_VERSION,
121+
"QF_AUFBV",
122+
smt2_solver.value(),
123+
std::cout)};
124+
}
125+
else
126+
{
127+
return ebmc_solvert{std::make_unique<smt2_dect>(
128+
ns,
129+
"ebmc",
130+
"Generated by EBMC " EBMC_VERSION,
131+
"QF_AUFBV",
132+
smt2_solver.value(),
133+
message_handler)};
134+
}
135+
};
123136
}
124137
else
125138
{

0 commit comments

Comments
 (0)