Skip to content

Commit b0c6528

Browse files
Use boolbvt for getting counter examples
We use this counter examples in the string solver but the formula given there don't use arrays so it is enough to use boolbvt.
1 parent 5b3a1a4 commit b0c6528

File tree

1 file changed

+1
-8
lines changed

1 file changed

+1
-8
lines changed

src/solvers/refinement/string_refinement.cpp

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2168,14 +2168,7 @@ static optionalt<exprt> find_counter_example(
21682168
const symbol_exprt &var)
21692169
{
21702170
satcheck_no_simplifiert sat_check;
2171-
bv_refinementt::infot info;
2172-
info.ns=&ns;
2173-
info.prop=&sat_check;
2174-
info.refine_arithmetic=true;
2175-
info.refine_arrays=true;
2176-
info.max_node_refinement=5;
2177-
info.ui=ui;
2178-
bv_refinementt solver(info);
2171+
boolbvt solver(ns, sat_check);
21792172
solver << axiom;
21802173

21812174
if(solver()==decision_proceduret::resultt::D_SATISFIABLE)

0 commit comments

Comments
 (0)