From 60c8296a0feab63721c29b36a9c6e5969d8009cb Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 13 Apr 2018 15:05:23 +0100 Subject: [PATCH] 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. --- src/solvers/refinement/string_refinement.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 84659d6d0ba..19e3e90c0d1 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -647,9 +647,6 @@ decision_proceduret::resultt string_refinementt::dec_solve() output_equations(debug(), equations, ns); #endif - // The object `dependencies` is also used by get, so we have to use it as a - // class member but we make sure it is cleared at each `dec_solve` call. - dependencies.clear(); debug() << "dec_solve: compute dependency graph and remove function " << "applications captured by the dependencies:" << eom; std::vector local_equations; @@ -658,6 +655,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() if(!add_node(dependencies, eq, generator.array_pool)) local_equations.push_back(eq); } + equations.clear(); #ifdef DEBUG dependencies.output_dot(debug());