Skip to content

Commit ef3f429

Browse files
author
Daniel Kroening
committed
switch show_vcc_plain to mstreamt
1 parent 68a5555 commit ef3f429

File tree

1 file changed

+11
-4
lines changed

1 file changed

+11
-4
lines changed

src/goto-symex/show_vcc.cpp

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ Author: Daniel Kroening, [email protected]
2525
#include <util/ui_message.h>
2626

2727
void show_vcc_plain(
28-
std::ostream &out,
28+
messaget::mstreamt &out,
2929
const namespacet &ns,
3030
const symex_target_equationt &equation)
3131
{
@@ -94,6 +94,8 @@ void show_vcc_plain(
9494
out << '{' << count << "} " << format(disjunct) << '\n';
9595
count++;
9696
}
97+
98+
out << messaget::eom;
9799
}
98100
}
99101

@@ -190,13 +192,18 @@ void show_vcc(
190192
break;
191193

192194
case ui_message_handlert::uit::PLAIN:
193-
msg.status() << "VERIFICATION CONDITIONS:\n" << messaget::eom;
194195
if(have_file)
195-
show_vcc_plain(out, ns, equation);
196+
{
197+
msg.status() << "Verification conditions written to file"
198+
<< messaget::eom;
199+
stream_message_handlert mout_handler(out);
200+
messaget mout(mout_handler);
201+
show_vcc_plain(mout.status(), ns, equation);
202+
}
196203
else
197204
{
205+
msg.status() << "VERIFICATION CONDITIONS:\n" << messaget::eom;
198206
show_vcc_plain(msg.status(), ns, equation);
199-
msg.status() << messaget::eom;
200207
}
201208
break;
202209
}

0 commit comments

Comments
 (0)