diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
index 6fd78fba152..bad8b8ff430 100644
--- a/src/solvers/CMakeLists.txt
+++ b/src/solvers/CMakeLists.txt
@@ -104,6 +104,6 @@ elseif("${sat_impl}" STREQUAL "glucose")
     target_link_libraries(solvers glucose-condensed)
 endif()
 
-target_link_libraries(solvers java_bytecode util)
+target_link_libraries(solvers util)
 
 generic_includes(solvers)
diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index 1c42fb768f9..067968af907 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -20,7 +20,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 #include <solvers/refinement/string_constraint_generator.h>
 
 #include <limits>
-#include <java_bytecode/java_types.h>
+
 #include <solvers/refinement/string_refinement_invariant.h>
 
 #include <util/arith_tools.h>
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 95df34885cc..d2a028b4c10 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -27,7 +27,6 @@ Author: Alberto Griggio, alberto.griggio@gmail.com
 #include <util/simplify_expr.h>
 #include <solvers/sat/satcheck.h>
 #include <solvers/refinement/string_constraint_instantiation.h>
-#include <java_bytecode/java_types.h>
 #include <unordered_set>
 
 static bool is_valid_string_constraint(
@@ -1221,6 +1220,7 @@ static exprt substitute_array_access(
     &symbol_generator)
 {
   const typet &char_type = array_expr.type().subtype();
+  const typet &index_type = to_array_type(array_expr.type()).size().type();
   const std::vector<exprt> &operands = array_expr.operands();
 
   exprt result = symbol_generator("out_of_bound_access", char_type);
@@ -1229,7 +1229,7 @@ static exprt substitute_array_access(
   {
     // Go in reverse order so that smaller indexes appear first in the result
     const std::size_t pos = operands.size() - 1 - i;
-    const equal_exprt equals(index, from_integer(pos, java_int_type()));
+    const equal_exprt equals(index, from_integer(pos, index_type));
     if(operands[pos].type() != char_type)
     {
       INVARIANT(