Skip to content

Commit 4ac86f9

Browse files
Remove "Adding counter-examples" message
This can be confusing now that we don't necessarily add the counter-examples.
1 parent e5039dd commit 4ac86f9

File tree

1 file changed

+0
-6
lines changed

1 file changed

+0
-6
lines changed

src/solvers/refinement/string_refinement.cpp

-6
Original file line numberDiff line numberDiff line change
@@ -1638,8 +1638,6 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
16381638

16391639
if(use_counter_example)
16401640
{
1641-
stream << "Adding counter-examples: " << eom;
1642-
16431641
std::vector<exprt> lemmas;
16441642

16451643
for(const auto &v : violated)
@@ -1655,8 +1653,6 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
16551653
binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
16561654
replace_expr(axiom.univ_var(), val, bounds);
16571655
const implies_exprt counter(bounds, instance);
1658-
1659-
stream << " - " << format(counter) << eom;
16601656
lemmas.push_back(counter);
16611657
}
16621658

@@ -1673,8 +1669,6 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
16731669
indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
16741670
const exprt counter=::instantiate_not_contains(
16751671
axiom, indices, generator)[0];
1676-
1677-
stream << " - " << format(counter) << eom;
16781672
lemmas.push_back(counter);
16791673
}
16801674
return { false, lemmas };

0 commit comments

Comments
 (0)