From 9e75ac74267e7259fab20a465d4fdb44a5698cc3 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 22 Feb 2018 09:39:16 +0000
Subject: [PATCH 1/3] Replace java_int_type by tyep deduced from array

This makes the function more robust and avoid dependencies on java
types.
---
 src/solvers/refinement/string_refinement.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 882b2b28e5d..56faa9b6576 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -1391,6 +1391,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);
@@ -1399,7 +1400,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(

From 2f6a3bf665c13456154c9a85aa4855993f086a8e Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 21 Feb 2018 14:36:36 +0000
Subject: [PATCH 2/3] Get rid of java_bytecode includes

---
 src/solvers/refinement/string_constraint_generator_main.cpp | 1 -
 src/solvers/refinement/string_refinement.cpp                | 1 -
 2 files changed, 2 deletions(-)

diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp
index 77d6d600a68..20b5c0ce3d9 100644
--- a/src/solvers/refinement/string_constraint_generator_main.cpp
+++ b/src/solvers/refinement/string_constraint_generator_main.cpp
@@ -21,7 +21,6 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 
 #include <limits>
 #include <ansi-c/string_constant.h>
-#include <java_bytecode/java_types.h>
 #include <solvers/refinement/string_refinement_invariant.h>
 #include <util/arith_tools.h>
 #include <util/pointer_predicates.h>
diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 56faa9b6576..75ef63041db 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(

From ceae231e67f0a0f14298a4ca75f87158a0ed4ad0 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 21 Feb 2018 14:38:08 +0000
Subject: [PATCH 3/3] Get rid of java_bytecode in solver CMakeList

---
 src/solvers/CMakeLists.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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)