diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.h b/jbmc/src/janalyzer/janalyzer_parse_options.h
index 54d85d6c050..15c0530668b 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.h
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.h
@@ -108,8 +108,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
-#include <analyses/goto_check_java.h>
-
+#include <java_bytecode/goto_check_java.h>
 #include <java_bytecode/java_bytecode_language.h>
 
 class abstract_goto_modelt;
diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile
index 3dd396bf345..c5a4fdf8623 100644
--- a/jbmc/src/java_bytecode/Makefile
+++ b/jbmc/src/java_bytecode/Makefile
@@ -9,6 +9,7 @@ SRC = assignments_from_json.cpp \
       expr2java.cpp \
       generic_parameter_specialization_map.cpp \
       generic_parameter_specialization_map_keys.cpp \
+      goto_check_java.cpp \
       jar_file.cpp \
       jar_pool.cpp \
       java_bmc_util.cpp \
diff --git a/src/analyses/goto_check_java.cpp b/jbmc/src/java_bytecode/goto_check_java.cpp
similarity index 99%
rename from src/analyses/goto_check_java.cpp
rename to jbmc/src/java_bytecode/goto_check_java.cpp
index 0e62371603d..76eb7816abf 100644
--- a/src/analyses/goto_check_java.cpp
+++ b/jbmc/src/java_bytecode/goto_check_java.cpp
@@ -41,8 +41,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_model.h>
 #include <goto-programs/remove_skip.h>
 
-#include "guard.h"
-#include "local_bitvector_analysis.h"
+#include <analyses/local_bitvector_analysis.h>
 
 class goto_check_javat
 {
@@ -84,7 +83,6 @@ class goto_check_javat
   const namespacet &ns;
   std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis;
   goto_programt::const_targett current_target;
-  guard_managert guard_manager;
   messaget log;
 
   /// Check an address-of expression:
diff --git a/src/analyses/goto_check_java.h b/jbmc/src/java_bytecode/goto_check_java.h
similarity index 100%
rename from src/analyses/goto_check_java.h
rename to jbmc/src/java_bytecode/goto_check_java.h
diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h
index 9bc514732e7..ea55144dcbc 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.h
+++ b/jbmc/src/jbmc/jbmc_parse_options.h
@@ -19,8 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/language.h>
 
-#include <analyses/goto_check_java.h>
-
 #include <goto-checker/bmc_util.h>
 
 #include <goto-programs/class_hierarchy.h>
@@ -29,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <solvers/strings/string_refinement.h>
 
+#include <java_bytecode/goto_check_java.h>
 #include <java_bytecode/java_bytecode_language.h>
 #include <java_bytecode/java_trace_validation.h>
 
diff --git a/jbmc/src/jdiff/jdiff_parse_options.h b/jbmc/src/jdiff/jdiff_parse_options.h
index 8fe7ebb7205..a37baeaf0bc 100644
--- a/jbmc/src/jdiff/jdiff_parse_options.h
+++ b/jbmc/src/jdiff/jdiff_parse_options.h
@@ -12,7 +12,7 @@ Author: Peter Schrammel
 #ifndef CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H
 #define CPROVER_JDIFF_JDIFF_PARSE_OPTIONS_H
 
-#include <analyses/goto_check_java.h>
+#include <java_bytecode/goto_check_java.h>
 
 #include <util/parse_options.h>
 #include <util/timestamper.h>
diff --git a/src/analyses/Makefile b/src/analyses/Makefile
index de976713e23..3388111f22b 100644
--- a/src/analyses/Makefile
+++ b/src/analyses/Makefile
@@ -14,7 +14,6 @@ SRC = ai.cpp \
       global_may_alias.cpp \
       goto_check.cpp \
       goto_check_c.cpp \
-      goto_check_java.cpp \
       goto_rw.cpp \
       guard_bdd.cpp \
       guard_expr.cpp \
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 9c030082016..5300dfb26ab 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_check.h"
 
 #include "goto_check_c.h"
-#include "goto_check_java.h"
 
 #include <util/symbol.h>
 
@@ -30,11 +29,6 @@ void goto_check(
     goto_check_c(
       function_identifier, goto_function, ns, options, message_handler);
   }
-  else if(function_symbol.mode == ID_java)
-  {
-    goto_check_java(
-      function_identifier, goto_function, ns, options, message_handler);
-  }
 }
 
 void goto_check(
@@ -44,7 +38,6 @@ void goto_check(
   message_handlert &message_handler)
 {
   goto_check_c(ns, options, goto_functions, message_handler);
-  goto_check_java(ns, options, goto_functions, message_handler);
 }
 
 void goto_check(
@@ -53,5 +46,4 @@ void goto_check(
   message_handlert &message_handler)
 {
   goto_check_c(options, goto_model, message_handler);
-  goto_check_java(options, goto_model, message_handler);
 }