Skip to content

Commit df1caca

Browse files
romainbrenguierJoel Allred
authored and
Joel Allred
committed
Adding namespace to arguments of from_expr in debug diffblue/test-gen#201
Not finding a symbol in from_expr can cause some exception to be thrown. This was happening while outputing debug information in some examples when --refine-strings was activated.
1 parent 935825e commit df1caca

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

src/solvers/refinement/string_refinement.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -475,8 +475,8 @@ void string_refinementt::set_to(const exprt &expr, bool value)
475475

476476
// Preprocessing to remove function applications.
477477
const exprt &lhs=eq_expr.lhs();
478-
debug() << "(sr::set_to) " << from_expr(lhs)
479-
<< " = " << from_expr(eq_expr.rhs()) << eom;
478+
debug() << "(sr::set_to) " << from_expr(ns, "", lhs)
479+
<< " = " << from_expr(ns, "", eq_expr.rhs()) << eom;
480480

481481
// TODO: See if this happens at all.
482482
if(lhs.id()!=ID_symbol)
@@ -545,7 +545,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
545545
for(std::pair<exprt, bool> &pair : non_string_axioms)
546546
{
547547
replace_expr(symbol_resolve, pair.first);
548-
debug() << "super::set_to " << from_expr(pair.first) << eom;
548+
debug() << "super::set_to " << from_expr(ns, "", pair.first) << eom;
549549
supert::set_to(pair.first, pair.second);
550550
}
551551

0 commit comments

Comments
 (0)