Skip to content

Commit 645eda9

Browse files
Improve invariant message
1 parent 3c7a671 commit 645eda9

File tree

1 file changed

+8
-3
lines changed

1 file changed

+8
-3
lines changed

src/solvers/refinement/string_refinement_util.cpp

+8-3
Original file line numberDiff line numberDiff line change
@@ -413,10 +413,15 @@ void string_dependenciest::for_each_dependency(
413413
stack.emplace_back(if_expr->true_case());
414414
stack.emplace_back(if_expr->false_case());
415415
}
416-
else if(const auto string_node = node_at(to_array_string_expr(current)))
417-
f(*string_node);
418416
else
419-
UNREACHABLE;
417+
{
418+
const auto string_node = node_at(to_array_string_expr(current));
419+
INVARIANT(
420+
string_node,
421+
"dependencies of the node should have been added to the graph at node creation "
422+
+ current.get().pretty());
423+
f(*string_node);
424+
}
420425
}
421426
}
422427
}

0 commit comments

Comments
 (0)