Skip to content

Commit 704f7df

Browse files
committed
Revert "output the iteration number in XML"
This reverts commit bacb22f.
1 parent 8000a2f commit 704f7df

File tree

2 files changed

+2
-12
lines changed

2 files changed

+2
-12
lines changed

src/solvers/refinement/bv_refinement_loop.cpp

-12
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,6 @@ Author: Daniel Kroening, [email protected]
88

99
#include "bv_refinement.h"
1010

11-
#include <iostream>
12-
13-
#include <util/xml.h>
14-
1511
bv_refinementt::bv_refinementt(const infot &info):
1612
bv_pointerst(*info.ns, *info.prop),
1713
progress(false),
@@ -40,14 +36,6 @@ decision_proceduret::resultt bv_refinementt::dec_solve()
4036

4137
status() << "BV-Refinement: iteration " << iteration << eom;
4238

43-
// output the very same information in a structured fashion
44-
if(config_.ui==ui_message_handlert::uit::XML_UI)
45-
{
46-
xmlt xml("refinement-iteration");
47-
xml.data=std::to_string(iteration);
48-
status() << xml << '\n';
49-
}
50-
5139
switch(prop_solve())
5240
{
5341
case resultt::D_SATISFIABLE:

src/solvers/refinement/string_refinement_util.h

+2
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@
99
#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
1010
#define CPROVER_SOLVERS_REFINEMENT_STRING_REFINEMENT_UTIL_H
1111

12+
#include <memory>
13+
1214
#include "string_builtin_function.h"
1315
#include "string_constraint.h"
1416
#include "string_constraint_generator.h"

0 commit comments

Comments
 (0)