diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 4072452112f..94d04b995cf 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/time_stopping.h>
 #include <util/message.h>
 #include <util/json.h>
+#include <util/cprover_prefix.h>
 
 #include <langapi/mode.h>
 #include <langapi/languages.h>
@@ -410,6 +411,12 @@ safety_checkert::resultt bmct::run(
   symex.set_message_handler(get_message_handler());
   symex.options=options;
 
+  {
+    const symbolt *init_symbol;
+    if(!ns.lookup(CPROVER_PREFIX "initialize", init_symbol))
+      symex.mode=init_symbol->mode;
+  }  
+
   status() << "Starting Bounded Model Checking" << eom;
 
   symex.last_source_location.make_nil();
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index 15f05453921..aede6b453ec 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -49,6 +49,7 @@ class goto_symext
     remaining_vccs(0),
     constant_propagation(true),
     new_symbol_table(_new_symbol_table),
+    mode(),
     ns(_ns),
     target(_target),
     atomic_section_counter(0),
@@ -95,9 +96,11 @@ class goto_symext
   optionst options;
   symbol_tablet &new_symbol_table;
 
+  irep_idt mode;
+
 protected:
   const namespacet &ns;
-  symex_targett &target;  
+  symex_targett &target;
   unsigned atomic_section_counter;
 
   friend class symex_dereference_statet;
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 007c74576a6..52e0eec28f7 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -295,7 +295,8 @@ void goto_symext::dereference_rec(
       ns,
       new_symbol_table,
       options,
-      symex_dereference_state);      
+      symex_dereference_state,
+      mode);      
     
     // std::cout << "**** " << from_expr(ns, "", tmp1) << std::endl;
     exprt tmp2=dereference.dereference(
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 6aeb3980a0b..34c428d6f4b 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -454,6 +454,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     // This is stuff like *((char *)5).
     // This is turned into an access to __CPROVER_memory[...].
 
+    if(language_mode==ID_java)
+    {
+      result.value=nil_exprt();
+      return result;
+    }
+    
     const symbolt &memory_symbol=ns.lookup(CPROVER_PREFIX "memory");    
     exprt symbol_expr=symbol_exprt(memory_symbol.name, memory_symbol.type);
 
diff --git a/src/pointer-analysis/value_set_dereference.h b/src/pointer-analysis/value_set_dereference.h
index 5f7f8b45612..ed8054be028 100644
--- a/src/pointer-analysis/value_set_dereference.h
+++ b/src/pointer-analysis/value_set_dereference.h
@@ -39,11 +39,13 @@ class value_set_dereferencet
     const namespacet &_ns,
     symbol_tablet &_new_symbol_table,
     const optionst &_options,
-    dereference_callbackt &_dereference_callback):
+    dereference_callbackt &_dereference_callback,
+    const irep_idt _language_mode = irep_idt()):
     ns(_ns),
     new_symbol_table(_new_symbol_table),
     options(_options),
-    dereference_callback(_dereference_callback)
+    dereference_callback(_dereference_callback),
+    language_mode(_language_mode)
   { }
 
   virtual ~value_set_dereferencet() { }
@@ -80,6 +82,7 @@ class value_set_dereferencet
   symbol_tablet &new_symbol_table;
   const optionst &options;
   dereference_callbackt &dereference_callback;
+  const irep_idt language_mode;
   static unsigned invalid_counter;
 
   bool dereference_type_compare(