Skip to content

Commit 60c8296

Browse files
Clear string_refinement equations (not dependencies)
We clear the equations once dec_solve finished using them, this avoids accumulating them in the next call to dec_solve. This means we should not clear the dependencies anymore, as thes can be lost.
1 parent f84753d commit 60c8296

File tree

1 file changed

+1
-3
lines changed

1 file changed

+1
-3
lines changed

src/solvers/refinement/string_refinement.cpp

+1-3
Original file line numberDiff line numberDiff line change
@@ -647,9 +647,6 @@ decision_proceduret::resultt string_refinementt::dec_solve()
647647
output_equations(debug(), equations, ns);
648648
#endif
649649

650-
// The object `dependencies` is also used by get, so we have to use it as a
651-
// class member but we make sure it is cleared at each `dec_solve` call.
652-
dependencies.clear();
653650
debug() << "dec_solve: compute dependency graph and remove function "
654651
<< "applications captured by the dependencies:" << eom;
655652
std::vector<exprt> local_equations;
@@ -658,6 +655,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
658655
if(!add_node(dependencies, eq, generator.array_pool))
659656
local_equations.push_back(eq);
660657
}
658+
equations.clear();
661659

662660
#ifdef DEBUG
663661
dependencies.output_dot(debug());

0 commit comments

Comments
 (0)