File tree Expand file tree Collapse file tree 1 file changed +4
-23
lines changed Expand file tree Collapse file tree 1 file changed +4
-23
lines changed Original file line number Diff line number Diff line change @@ -137,27 +137,8 @@ bool symex_bmc_incremental_one_loopt::resume(
137
137
}
138
138
void symex_bmc_incremental_one_loopt::log_unwinding (unsigned unwind)
139
139
{
140
- const std::string unwind_num = std::to_string (unwind);
141
- switch (output_ui)
142
- {
143
- case ui_message_handlert::uit::PLAIN:
144
- {
145
- log.statistics () << " Current unwinding: " << unwind_num << messaget::eom;
146
- break ;
147
- }
148
- case ui_message_handlert::uit::XML_UI:
149
- {
150
- xmlt xml (" current-unwinding" );
151
- xml.data = unwind_num;
152
- log.statistics () << xml << messaget::eom;
153
- break ;
154
- }
155
- case ui_message_handlert::uit::JSON_UI:
156
- {
157
- json_objectt json;
158
- json[" currentUnwinding" ] = json_numbert (unwind_num);
159
- log.statistics () << json << messaget::eom;
160
- break ;
161
- }
162
- }
140
+ structured_datat data{{{labelt ({" current" , " unwinding" }),
141
+ structured_data_entryt::data_node (
142
+ json_numbert{std::to_string (unwind)})}}};
143
+ log.statistics () << data;
163
144
}
You can’t perform that action at this time.
0 commit comments