Skip to content

Commit f6a153e

Browse files
Check type before adding dependencies
We check that the type is that of a string before adding the dependence.
1 parent 0139424 commit f6a153e

File tree

1 file changed

+6
-5
lines changed

1 file changed

+6
-5
lines changed

src/solvers/refinement/string_refinement_util.cpp

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -256,11 +256,11 @@ static void add_unknown_dependency_to_string_subexprs(
256256
{
257257
std::for_each(
258258
expr.depth_begin(), expr.depth_end(), [&](const exprt &e) { // NOLINT
259-
const auto &string_struct = expr_try_dynamic_cast<struct_exprt>(e);
260-
if(string_struct && string_struct->operands().size() == 2)
259+
if(is_refined_string_type(e.type()))
261260
{
261+
const auto &string_struct = expr_checked_cast<struct_exprt>(e);
262262
const array_string_exprt string =
263-
array_pool.find(string_struct->op1(), string_struct->op0());
263+
array_pool.find(string_struct.op1(), string_struct.op0());
264264
dependencies.add_unknown_dependency(string);
265265
}
266266
});
@@ -290,9 +290,10 @@ static void add_dependency_to_string_subexprs(
290290
expr.depth_begin(),
291291
expr.depth_end(),
292292
[&](const exprt &e) { // NOLINT
293-
if(const auto structure = expr_try_dynamic_cast<struct_exprt>(e))
293+
if(is_refined_string_type(e.type()))
294294
{
295-
const array_string_exprt string = array_pool.of_argument(*structure);
295+
const auto string_struct = expr_checked_cast<struct_exprt>(e);
296+
const auto string = array_pool.of_argument(string_struct);
296297
dependencies.add_dependency(string, builtin_function_node);
297298
}
298299
});

0 commit comments

Comments
 (0)