Improve invariant message

NathanJPhillips · Jun 18, 2018 · 645eda9 · 645eda9
1 parent 3c7a671
commit 645eda9
Showing 1 changed file with 8 additions and 3 deletions.
diff --git 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);
+      }
     }
   }
 }