From a057fe65b27e9d89a7c0db5b9fbd3db13eb85210 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Thu, 31 Aug 2017 23:12:17 +0100
Subject: [PATCH] HAVE_BV_REFINEMENT and HAVE_JAVA_BYTECODE are no longer
 needed

---
 src/clobber/Makefile                  | 11 +----------
 src/goto-diff/Makefile                |  6 +-----
 src/goto-diff/goto_diff_languages.cpp |  4 ----
 src/goto-instrument/Makefile          |  6 +-----
 src/symex/Makefile                    | 11 +----------
 5 files changed, 4 insertions(+), 34 deletions(-)

diff --git a/src/clobber/Makefile b/src/clobber/Makefile
index f3a4c8aed20..74a133782c6 100644
--- a/src/clobber/Makefile
+++ b/src/clobber/Makefile
@@ -3,6 +3,7 @@ SRC = clobber_main.cpp \
       # Empty last line
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../cpp/cpp$(LIBEXT) \
+       ../java_bytecode/java_bytecode$(LIBEXT) \
        ../linking/linking$(LIBEXT) \
        ../big-int/big-int$(LIBEXT) \
        ../goto-programs/goto-programs$(LIBEXT) \
@@ -30,16 +31,6 @@ CLEANFILES = clobber$(EXEEXT)
 
 all: clobber$(EXEEXT)
 
-ifneq ($(wildcard ../bv_refinement/Makefile),)
-  OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
-endif
-
-ifneq ($(wildcard ../java_bytecode/Makefile),)
-  OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
-endif
-
 ifneq ($(wildcard ../specc/Makefile),)
   OBJ += ../specc/specc$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_SPECC
diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile
index b11cb008b3a..17b2d253561 100644
--- a/src/goto-diff/Makefile
+++ b/src/goto-diff/Makefile
@@ -9,6 +9,7 @@ SRC = change_impact.cpp \
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
+      ../java_bytecode/java_bytecode$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \
@@ -33,11 +34,6 @@ CLEANFILES = goto-diff$(EXEEXT)
 
 all: goto-diff$(EXEEXT)
 
-ifneq ($(wildcard ../java_bytecode/Makefile),)
-  OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
-endif
-
 ifneq ($(wildcard ../specc/Makefile),)
   OBJ += ../specc/specc$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_SPECC
diff --git a/src/goto-diff/goto_diff_languages.cpp b/src/goto-diff/goto_diff_languages.cpp
index c55f82e637e..c930f20e77b 100644
--- a/src/goto-diff/goto_diff_languages.cpp
+++ b/src/goto-diff/goto_diff_languages.cpp
@@ -20,9 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <specc/specc_language.h>
 #endif
 
-#ifdef HAVE_JAVA_BYTECODE
 #include <java_bytecode/java_bytecode_language.h>
-#endif
 
 void goto_diff_languagest::register_languages()
 {
@@ -33,7 +31,5 @@ void goto_diff_languagest::register_languages()
   register_language(new_specc_language);
   #endif
 
-  #ifdef HAVE_JAVA_BYTECODE
   register_language(new_java_bytecode_language);
-  #endif
 }
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index bc3cb10f1b3..6d54c94fae3 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -65,6 +65,7 @@ SRC = accelerate/accelerate.cpp \
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \
+      ../java_bytecode/java_bytecode$(LIBEXT) \
       ../linking/linking$(LIBEXT) \
       ../big-int/big-int$(LIBEXT) \
       ../goto-programs/goto-programs$(LIBEXT) \
@@ -90,11 +91,6 @@ include ../common
 
 all: goto-instrument$(EXEEXT)
 
-ifneq ($(wildcard ../java_bytecode/Makefile),)
-  OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
-endif
-
 ifneq ($(LIB_GLPK),)
   LIBS += $(LIB_GLPK)
   CP_CXXFLAGS += -DHAVE_GLPK
diff --git a/src/symex/Makefile b/src/symex/Makefile
index 672b2e07fc2..46236715d9c 100644
--- a/src/symex/Makefile
+++ b/src/symex/Makefile
@@ -6,6 +6,7 @@ SRC = path_search.cpp \
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../cpp/cpp$(LIBEXT) \
+       ../java_bytecode/java_bytecode$(LIBEXT) \
        ../linking/linking$(LIBEXT) \
        ../big-int/big-int$(LIBEXT) \
        ../goto-programs/goto-programs$(LIBEXT) \
@@ -34,16 +35,6 @@ CLEANFILES = symex$(EXEEXT)
 
 all: symex$(EXEEXT)
 
-ifneq ($(wildcard ../bv_refinement/Makefile),)
-  OBJ += ../bv_refinement/bv_refinement$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_BV_REFINEMENT
-endif
-
-ifneq ($(wildcard ../java_bytecode/Makefile),)
-  OBJ += ../java_bytecode/java_bytecode$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_JAVA_BYTECODE
-endif
-
 ifneq ($(wildcard ../specc/Makefile),)
   OBJ += ../specc/specc$(LIBEXT)
   CP_CXXFLAGS += -DHAVE_SPECC