diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp
index e8a0dcdcbb5..02cb1e478b4 100644
--- a/src/solvers/prop/bdd_expr.cpp
+++ b/src/solvers/prop/bdd_expr.cpp
@@ -11,14 +11,11 @@ Author: Michael Tautschnig, michael.tautschnig@qmul.ac.uk
 
 #include "bdd_expr.h"
 
-#include <util/arith_tools.h>
 #include <util/expr_util.h>
 #include <util/format_expr.h>
 #include <util/invariant.h>
 #include <util/std_expr.h>
 
-#include <sstream>
-
 bddt bdd_exprt::from_expr_rec(const exprt &expr)
 {
   PRECONDITION(expr.type().id() == ID_bool);
@@ -112,7 +109,7 @@ exprt bdd_exprt::as_expr(
       return true_exprt();
   }
 
-  auto index = numeric_cast_v<std::size_t>(r.index());
+  auto index = narrow<std::size_t>(r.index());
   INVARIANT(index < node_map.size(), "Index should be in node_map");
   const exprt &n_expr = node_map[index];