From 645eda9080ee3f4451e2ff3fab74309dfc3f73f2 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 13 Jun 2018 17:05:44 +0100 Subject: [PATCH] Improve invariant message --- src/solvers/refinement/string_refinement_util.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/solvers/refinement/string_refinement_util.cpp b/src/solvers/refinement/string_refinement_util.cpp index a93df7b75ef..76a71ea9fca 100644 --- a/src/solvers/refinement/string_refinement_util.cpp +++ b/src/solvers/refinement/string_refinement_util.cpp @@ -413,10 +413,15 @@ void string_dependenciest::for_each_dependency( stack.emplace_back(if_expr->true_case()); stack.emplace_back(if_expr->false_case()); } - else if(const auto string_node = node_at(to_array_string_expr(current))) - f(*string_node); else - UNREACHABLE; + { + const auto string_node = node_at(to_array_string_expr(current)); + INVARIANT( + string_node, + "dependencies of the node should have been added to the graph at node creation " + + current.get().pretty()); + f(*string_node); + } } } }