diff --git a/regression/cbmc-java/jar-file4/A.jar b/regression/cbmc-java/jar-file4/A.jar
new file mode 100644
index 00000000000..e721e6f32f9
Binary files /dev/null and b/regression/cbmc-java/jar-file4/A.jar differ
diff --git a/regression/cbmc-java/jar-file4/B.jar b/regression/cbmc-java/jar-file4/B.jar
new file mode 100644
index 00000000000..d381e413e74
Binary files /dev/null and b/regression/cbmc-java/jar-file4/B.jar differ
diff --git a/regression/cbmc-java/jar-file4/C.jar b/regression/cbmc-java/jar-file4/C.jar
new file mode 100644
index 00000000000..e318db6c413
Binary files /dev/null and b/regression/cbmc-java/jar-file4/C.jar differ
diff --git a/regression/cbmc-java/jar-file4/jar.json b/regression/cbmc-java/jar-file4/jar.json
new file mode 100644
index 00000000000..09df8008b8c
--- /dev/null
+++ b/regression/cbmc-java/jar-file4/jar.json
@@ -0,0 +1,12 @@
+{
+  "jar":
+  [
+    "A.jar",
+    "B.jar"
+  ],
+  "classFiles":
+  [
+    "jarfile3$A.class",
+    "jarfile3.class"
+  ]
+}
diff --git a/regression/cbmc-java/jar-file4/test.desc b/regression/cbmc-java/jar-file4/test.desc
new file mode 100644
index 00000000000..5c34bdcd5a8
--- /dev/null
+++ b/regression/cbmc-java/jar-file4/test.desc
@@ -0,0 +1,10 @@
+CORE
+C.jar
+--function jarfile3.f --java-cp-include-files "@jar.json"
+^EXIT=10$
+^SIGNAL=0$
+.*SUCCESS$
+.*FAILURE$
+^VERIFICATION FAILED
+--
+^warning: ignoring
diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile
index 79224766188..8132097565c 100644
--- a/src/cbmc/Makefile
+++ b/src/cbmc/Makefile
@@ -28,7 +28,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../solvers/solvers$(LIBEXT) \
       ../util/util$(LIBEXT) \
-      ../miniz/miniz$(OBJEXT)
+      ../miniz/miniz$(OBJEXT) \
+      ../json/json$(LIBEXT)
 
 INCLUDES= -I ..
 
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 7364752d093..5ed5d28054e 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -1155,6 +1155,7 @@ void cbmc_parse_optionst::help()
     // NOLINTNEXTLINE(whitespace/line_length)
     " --java-max-vla-length        limit the length of user-code-created arrays\n"
     // NOLINTNEXTLINE(whitespace/line_length)
+    " --java-cp-include-files      regexp or JSON list of files to load (with '@' prefix)\n"
     " --java-unwind-enum-static    try to unwind loops in static initialization of enums\n"
     "\n"
     "Semantic transformations:\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index adc6e2ee517..a3fc5e7e7d3 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -55,6 +55,7 @@ class optionst;
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(graphml-witness):" \
   "(java-max-vla-length):(java-unwind-enum-static)" \
+  "(java-cp-include-files):" \
   "(localize-faults)(localize-faults-method):" \
   "(lazy-methods)" \
   "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
diff --git a/src/cegis/Makefile b/src/cegis/Makefile
index 37fe5416953..f1a38ce4915 100644
--- a/src/cegis/Makefile
+++ b/src/cegis/Makefile
@@ -116,7 +116,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cbmc/cbmc_dimacs$(OBJEXT) ../cbmc/all_properties$(OBJEXT) \
       ../cbmc/fault_localization$(OBJEXT) \
       ../cbmc/symex_coverage$(OBJEXT) \
-      ../miniz/miniz$(OBJEXT)
+      ../miniz/miniz$(OBJEXT) \
+      ../json/json$(LIBEXT)
 
 INCLUDES= -I ..
 
diff --git a/src/goto-cc/Makefile b/src/goto-cc/Makefile
index 04261db95f0..3079e7ebb00 100644
--- a/src/goto-cc/Makefile
+++ b/src/goto-cc/Makefile
@@ -14,7 +14,8 @@ OBJ += ../big-int/big-int$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
-      ../miniz/miniz$(OBJEXT)
+      ../miniz/miniz$(OBJEXT) \
+      ../json/json$(LIBEXT)
 
 INCLUDES= -I ..
 
diff --git a/src/goto-diff/Makefile b/src/goto-diff/Makefile
index c003d0c96b0..fd18897aaea 100644
--- a/src/goto-diff/Makefile
+++ b/src/goto-diff/Makefile
@@ -14,7 +14,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../util/util$(LIBEXT) \
       ../solvers/solvers$(LIBEXT) \
-      ../miniz/miniz$(OBJEXT)
+      ../miniz/miniz$(OBJEXT) \
+      ../json/json$(LIBEXT)
 
 INCLUDES= -I ..
 
diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile
index f79b62d806f..4cbd6121b24 100644
--- a/src/goto-instrument/Makefile
+++ b/src/goto-instrument/Makefile
@@ -38,7 +38,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../xmllang/xmllang$(LIBEXT) \
       ../util/util$(LIBEXT) \
       ../solvers/solvers$(LIBEXT) \
-      ../miniz/miniz$(OBJEXT)
+      ../miniz/miniz$(OBJEXT) \
+      ../json/json$(LIBEXT)
 
 INCLUDES= -I ..
 
diff --git a/src/java_bytecode/jar_file.cpp b/src/java_bytecode/jar_file.cpp
index d679f21c070..07d7719e500 100644
--- a/src/java_bytecode/jar_file.cpp
+++ b/src/java_bytecode/jar_file.cpp
@@ -8,10 +8,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cstring>
 #include <cassert>
-#include <sstream>
+#include <unordered_set>
 
+#include <json/json_parser.h>
+#include <util/suffix.h>
 #include "jar_file.h"
-
 /*******************************************************************\
 
 Function: jar_filet::open
@@ -24,7 +25,9 @@ Function: jar_filet::open
 
 \*******************************************************************/
 
-void jar_filet::open(const std::string &filename)
+void jar_filet::open(
+  std::string &java_cp_include_files,
+  const std::string &filename)
 {
   if(!mz_ok)
   {
@@ -35,11 +38,37 @@ void jar_filet::open(const std::string &filename)
 
   if(mz_ok)
   {
+    // '@' signals file reading with list of class files to load
+    bool regex_match=java_cp_include_files[0]!='@';
+    std::regex regex_matcher;
+    std::smatch string_matcher;
+    std::unordered_set<std::string> set_matcher;
+    jsont json_cp_config;
+    if(regex_match)
+      regex_matcher=std::regex(java_cp_include_files);
+    else
+    {
+      assert(java_cp_include_files.length()>1);
+      if(parse_json(
+           java_cp_include_files.substr(1),
+           get_message_handler(),
+           json_cp_config))
+        throw "cannot read JSON input configuration for JAR loading";
+      if(!json_cp_config.is_object())
+        throw "the JSON file has a wrong format";
+      jsont include_files=json_cp_config["classFiles"];
+      if(!include_files.is_array())
+        throw "the JSON file has a wrong format";
+      for(const jsont &file_entry : include_files.array)
+      {
+        assert(file_entry.is_string());
+        set_matcher.insert(file_entry.value);
+      }
+    }
+
     std::size_t number_of_files=
       mz_zip_reader_get_num_files(&zip);
 
-    index.reserve(number_of_files);
-
     for(std::size_t i=0; i<number_of_files; i++)
     {
       mz_uint filename_length=mz_zip_reader_get_filename(&zip, i, nullptr, 0);
@@ -48,8 +77,23 @@ void jar_filet::open(const std::string &filename)
         mz_zip_reader_get_filename(&zip, i, filename_char, filename_length);
       assert(filename_length==filename_len);
       std::string file_name(filename_char);
+
+      // non-class files are loaded in any case
+      bool add_file=!has_suffix(file_name, ".class");
+      // load .class file only if they match regex
+      if(regex_match)
+        add_file|=std::regex_match(file_name, string_matcher, regex_matcher);
+      // load .class file only if it is in the match set
+      else
+        add_file|=set_matcher.find(file_name)!=set_matcher.end();
+      if(add_file)
+      {
+        if(has_suffix(file_name, ".class"))
+          status() << "read class file " << file_name
+                   << " from " << filename << eom;
+        filtered_jar[file_name]=i;
+      }
       delete[] filename_char;
-      index.push_back(file_name);
     }
   }
 }
@@ -87,25 +131,27 @@ Function: jar_filet::get_entry
 
 \*******************************************************************/
 
-std::string jar_filet::get_entry(std::size_t i)
+std::string jar_filet::get_entry(const irep_idt &name)
 {
   if(!mz_ok)
     return std::string("");
 
-  assert(i<index.size());
-
   std::string dest;
 
+  auto entry=filtered_jar.find(name);
+  assert(entry!=filtered_jar.end());
+
+  size_t real_index=entry->second;
   mz_zip_archive_file_stat file_stat;
   memset(&file_stat, 0, sizeof(file_stat));
-  mz_bool stat_ok=mz_zip_reader_file_stat(&zip, i, &file_stat);
+  mz_bool stat_ok=mz_zip_reader_file_stat(&zip, real_index, &file_stat);
   if(stat_ok!=MZ_TRUE)
     return std::string();
   std::vector<char> buffer;
   size_t bufsize=file_stat.m_uncomp_size;
   buffer.resize(bufsize);
   mz_bool read_ok=
-    mz_zip_reader_extract_to_mem(&zip, i, buffer.data(), bufsize, 0);
+    mz_zip_reader_extract_to_mem(&zip, real_index, buffer.data(), bufsize, 0);
   if(read_ok!=MZ_TRUE)
     return std::string();
 
@@ -128,24 +174,11 @@ Function: jar_filet::get_manifest
 
 jar_filet::manifestt jar_filet::get_manifest()
 {
-  std::size_t i=0;
-  bool found=false;
-
-  for(const auto &e : index)
-  {
-    if(e=="META-INF/MANIFEST.MF")
-    {
-      found=true;
-      break;
-    }
-
-    i++;
-  }
-
-  if(!found)
+  auto entry=filtered_jar.find("META-INF/MANIFEST.MF");
+  if(entry==filtered_jar.end())
     return manifestt();
 
-  std::string dest=get_entry(i);
+  std::string dest=get_entry(entry->first);
   std::istringstream in(dest);
 
   manifestt manifest;
diff --git a/src/java_bytecode/jar_file.h b/src/java_bytecode/jar_file.h
index 53f673102bf..9407e711128 100644
--- a/src/java_bytecode/jar_file.h
+++ b/src/java_bytecode/jar_file.h
@@ -15,29 +15,26 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <string>
 #include <vector>
 #include <map>
+#include <regex>
+#include <util/message.h>
 
-class jar_filet
+class jar_filet:public messaget
 {
 public:
   jar_filet():mz_ok(false) { }
 
-  inline explicit jar_filet(const std::string &file_name)
-  {
-    open(file_name);
-  }
-
   ~jar_filet();
 
-  void open(const std::string &);
+  void open(std::string &java_cp_include_files, const std::string &);
 
   // Test for error; 'true' means we are good.
-  inline explicit operator bool() const { return true;  // TODO
-  }
+  explicit operator bool() const { return mz_ok; }
 
-  typedef std::vector<std::string> indext;
-  indext index;
+  // map internal index to real index in jar central directory
+  typedef std::map<irep_idt, size_t> filtered_jart;
+  filtered_jart filtered_jar;
 
-  std::string get_entry(std::size_t i);
+  std::string get_entry(const irep_idt &);
 
   typedef std::map<std::string, std::string> manifestt;
   manifestt get_manifest();
@@ -47,16 +44,24 @@ class jar_filet
   bool mz_ok;
 };
 
-class jar_poolt
+class jar_poolt:public messaget
 {
 public:
+  void set_java_cp_include_files(std::string &_java_cp_include_files)
+  {
+    java_cp_include_files=_java_cp_include_files;
+  }
+
   jar_filet &operator()(const std::string &file_name)
   {
+    if(java_cp_include_files.empty())
+      throw "class regexp cannot be empty";
     file_mapt::iterator it=file_map.find(file_name);
     if(it==file_map.end())
     {
       jar_filet &jar_file=file_map[file_name];
-      jar_file.open(file_name);
+      jar_file.set_message_handler(get_message_handler());
+      jar_file.open(java_cp_include_files, file_name);
       return jar_file;
     }
     else
@@ -66,6 +71,7 @@ class jar_poolt
 protected:
   typedef std::map<std::string, jar_filet> file_mapt;
   file_mapt file_map;
+  std::string java_cp_include_files;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_JAR_FILE_H
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 79295995662..0e2eb25d0ec 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/cmdline.h>
 #include <util/string2int.h>
+#include <json/json_parser.h>
 
 #include <goto-programs/class_hierarchy.h>
 
@@ -55,6 +56,36 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
     lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE;
   else
     lazy_methods_mode=LAZY_METHODS_MODE_EAGER;
+
+  if(cmd.isset("java-cp-include-files"))
+  {
+    java_cp_include_files=cmd.get_value("java-cp-include-files");
+    // load file list from JSON file
+    if(java_cp_include_files[0]=='@')
+    {
+      jsont json_cp_config;
+      if(parse_json(
+           java_cp_include_files.substr(1),
+           get_message_handler(),
+           json_cp_config))
+        throw "cannot read JSON input configuration for JAR loading";
+
+      if(!json_cp_config.is_object())
+        throw "the JSON file has a wrong format";
+      jsont include_files=json_cp_config["jar"];
+      if(!include_files.is_array())
+         throw "the JSON file has a wrong format";
+
+      // add jars from JSON config file to classpath
+      for(const jsont &file_entry : include_files.array)
+      {
+        assert(file_entry.is_string() && has_suffix(file_entry.value, ".jar"));
+        config.java.classpath.push_back(file_entry.value);
+      }
+    }
+  }
+  else
+    java_cp_include_files=".*";
 }
 
 /*******************************************************************\
@@ -129,6 +160,7 @@ bool java_bytecode_languaget::parse(
   const std::string &path)
 {
   java_class_loader.set_message_handler(get_message_handler());
+  java_class_loader.set_java_cp_include_files(java_cp_include_files);
 
   // look at extension
   if(has_suffix(path, ".class"))
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index 643eacd5b7f..77689d6e12a 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -105,6 +105,7 @@ class java_bytecode_languaget:public languaget
   lazy_methodst lazy_methods;
   lazy_methods_modet lazy_methods_mode;
   bool string_refinement_enabled;
+  std::string java_cp_include_files;
 };
 
 languaget *new_java_bytecode_language();
diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp
index dc4330aa00c..c8e6bbf5bb4 100644
--- a/src/java_bytecode/java_class_loader.cpp
+++ b/src/java_bytecode/java_class_loader.cpp
@@ -98,7 +98,7 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree(
       debug() << "Getting class `" << class_name << "' from JAR "
               << jf << eom;
 
-      std::string data=jar_pool(jf).get_entry(jm_it->second.index);
+      std::string data=jar_pool(jf).get_entry(jm_it->second.class_file_name);
 
       std::istringstream istream(data);
 
@@ -129,7 +129,7 @@ java_bytecode_parse_treet &java_class_loadert::get_parse_tree(
         debug() << "Getting class `" << class_name << "' from JAR "
                 << cp << eom;
 
-        std::string data=jar_pool(cp).get_entry(jm_it->second.index);
+        std::string data=jar_pool(cp).get_entry(jm_it->second.class_file_name);
 
         std::istringstream istream(data);
 
@@ -223,11 +223,10 @@ void java_class_loadert::read_jar_file(const irep_idt &file)
   debug() << "adding JAR file `" << file << "'" << eom;
 
   auto &jm=jar_map[file];
-  std::size_t number_of_files=jar_file.index.size();
 
-  for(std::size_t i=0; i<number_of_files; i++)
+  for(auto &jar_entry : jar_file.filtered_jar)
   {
-    std::string file_name=jar_file.index[i];
+    std::string file_name=id2string(jar_entry.first);
 
     // does it end on .class?
     if(has_suffix(file_name, ".class"))
@@ -235,7 +234,7 @@ void java_class_loadert::read_jar_file(const irep_idt &file)
       irep_idt class_name=file_to_class_name(file_name);
 
       // record
-      jm.entries[class_name].index=i;
+      jm.entries[class_name].class_file_name=file_name;
     }
   }
 }
diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h
index b2a4953445a..7a8f6da2b5c 100644
--- a/src/java_bytecode/java_class_loader.h
+++ b/src/java_bytecode/java_class_loader.h
@@ -21,6 +21,12 @@ class java_class_loadert:public messaget
 public:
   java_bytecode_parse_treet &operator()(const irep_idt &);
 
+  void set_java_cp_include_files(std::string &java_cp_include_files)
+  {
+    jar_pool.set_java_cp_include_files(java_cp_include_files);
+    jar_pool.set_message_handler(get_message_handler());
+  }
+
   // maps class names to the parse trees
   typedef std::map<irep_idt, java_bytecode_parse_treet> class_mapt;
   class_mapt class_map;
@@ -42,7 +48,7 @@ class java_class_loadert:public messaget
   public:
     struct entryt
     {
-      std::size_t index;
+      std::string class_file_name;
     };
 
     // class name to index map
diff --git a/src/symex/Makefile b/src/symex/Makefile
index f177e91bc07..e887ca55352 100644
--- a/src/symex/Makefile
+++ b/src/symex/Makefile
@@ -17,7 +17,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
        ../pointer-analysis/dereference$(OBJEXT) \
        ../goto-instrument/cover$(OBJEXT) \
        ../path-symex/path-symex$(LIBEXT) \
-       ../miniz/miniz$(OBJEXT)
+       ../miniz/miniz$(OBJEXT) \
+       ../json/json$(LIBEXT)
 
 INCLUDES= -I ..