Skip to content

Commit c905c2c

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

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
@@ -1641,8 +1641,6 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
16411641

16421642
if(use_counter_example)
16431643
{
1644-
stream << "Adding counter-examples: " << eom;
1645-
16461644
std::vector<exprt> lemmas;
16471645

16481646
for(const auto &v : violated)
@@ -1658,8 +1656,6 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
16581656
binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
16591657
replace_expr(axiom.univ_var(), val, bounds);
16601658
const implies_exprt counter(bounds, instance);
1661-
1662-
stream << " - " << format(counter) << eom;
16631659
lemmas.push_back(counter);
16641660
}
16651661

@@ -1676,8 +1672,6 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
16761672
indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
16771673
const exprt counter=::instantiate_not_contains(
16781674
axiom, indices, generator)[0];
1679-
1680-
stream << " - " << format(counter) << eom;
16811675
lemmas.push_back(counter);
16821676
}
16831677
return { false, lemmas };

0 commit comments

Comments
 (0)