diff --git a/jbmc/regression/janalyzer/too-many-args/A.class b/jbmc/regression/janalyzer/too-many-args/A.class
new file mode 100644
index 00000000000..af02287ac8e
Binary files /dev/null and b/jbmc/regression/janalyzer/too-many-args/A.class differ
diff --git a/jbmc/regression/janalyzer/too-many-args/A.java b/jbmc/regression/janalyzer/too-many-args/A.java
new file mode 100644
index 00000000000..29bb36d6543
--- /dev/null
+++ b/jbmc/regression/janalyzer/too-many-args/A.java
@@ -0,0 +1,2 @@
+public class A { }
+class B { }
diff --git a/jbmc/regression/janalyzer/too-many-args/B.class b/jbmc/regression/janalyzer/too-many-args/B.class
new file mode 100644
index 00000000000..7ca3e5dbbb7
Binary files /dev/null and b/jbmc/regression/janalyzer/too-many-args/B.class differ
diff --git a/jbmc/regression/janalyzer/too-many-args/test.desc b/jbmc/regression/janalyzer/too-many-args/test.desc
new file mode 100644
index 00000000000..2498c135033
--- /dev/null
+++ b/jbmc/regression/janalyzer/too-many-args/test.desc
@@ -0,0 +1,6 @@
+CORE
+A.class
+B.class
+^Only one \.class, \.jar or \.gbf file should be directly specified on the command-line
+^EXIT=1$
+^SIGNAL=0$
diff --git a/jbmc/regression/jbmc/classpath-two-classes/test_incorrect.desc b/jbmc/regression/jbmc/classpath-two-classes/test_incorrect.desc
deleted file mode 100644
index 06e74a8e0e9..00000000000
--- a/jbmc/regression/jbmc/classpath-two-classes/test_incorrect.desc
+++ /dev/null
@@ -1,10 +0,0 @@
-KNOWNBUG
-Test.class
-Test2.class
-^EXIT=6$
-^SIGNAL=0$
---
-Invariant check failed
---
-We don't allow two classes passed on the command line.
-Issue: 2864
diff --git a/jbmc/regression/jbmc/classpath-two-jars/test_incorrect.desc b/jbmc/regression/jbmc/classpath-two-jars/test_incorrect.desc
deleted file mode 100644
index a743428a54e..00000000000
--- a/jbmc/regression/jbmc/classpath-two-jars/test_incorrect.desc
+++ /dev/null
@@ -1,11 +0,0 @@
-KNOWNBUG
-libs/test.jar
-lib/test2.jar --main-class Test.class
-^EXIT=6$
-^SIGNAL=0$
---
-Invariant check failed
-the program has no entry point
---
-We don't allow two jar files passed on the command line.
-Issue: 2864
diff --git a/jbmc/regression/jbmc/string_field_aliasing/test.desc b/jbmc/regression/jbmc/string_field_aliasing/test.desc
index a152589bfed..12b08e38018 100644
--- a/jbmc/regression/jbmc/string_field_aliasing/test.desc
+++ b/jbmc/regression/jbmc/string_field_aliasing/test.desc
@@ -1,6 +1,6 @@
 CORE
 Cart.class
---cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --trace --java-max-vla-length 96 --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 Cart.class --function Cart.checkTax4 --string-printable
+--cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --trace --java-max-vla-length 96 --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 --function Cart.checkTax4 --string-printable
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc/too-many-args/A.class b/jbmc/regression/jbmc/too-many-args/A.class
new file mode 100644
index 00000000000..af02287ac8e
Binary files /dev/null and b/jbmc/regression/jbmc/too-many-args/A.class differ
diff --git a/jbmc/regression/jbmc/too-many-args/A.java b/jbmc/regression/jbmc/too-many-args/A.java
new file mode 100644
index 00000000000..29bb36d6543
--- /dev/null
+++ b/jbmc/regression/jbmc/too-many-args/A.java
@@ -0,0 +1,2 @@
+public class A { }
+class B { }
diff --git a/jbmc/regression/jbmc/too-many-args/B.class b/jbmc/regression/jbmc/too-many-args/B.class
new file mode 100644
index 00000000000..7ca3e5dbbb7
Binary files /dev/null and b/jbmc/regression/jbmc/too-many-args/B.class differ
diff --git a/jbmc/regression/jbmc/too-many-args/test.desc b/jbmc/regression/jbmc/too-many-args/test.desc
new file mode 100644
index 00000000000..bdf1ec07c85
--- /dev/null
+++ b/jbmc/regression/jbmc/too-many-args/test.desc
@@ -0,0 +1,6 @@
+CORE
+A.class
+B.class
+^Only one \.class, \.jar or \.gbf file should be directly specified on the command-line
+^EXIT=6$
+^SIGNAL=0$
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
index 2397065c41b..00e6645f376 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -355,6 +355,17 @@ int janalyzer_parse_optionst::doit()
 
   register_languages();
 
+  if(cmdline.args.size() > 1)
+  {
+    error() << "Only one .class, .jar or .gbf file should be directly "
+      "specified on the command-line. To force loading another another class "
+      "use '--java-load-class somepackage.SomeClass' or "
+      "'--lazy-methods-extra-entry-point somepackage.SomeClass.method' along "
+      "with '--classpath'"
+            << messaget::eom;
+    return CPROVER_EXIT_USAGE_ERROR;
+  }
+
   goto_model =
     initialize_goto_model(cmdline.args, get_message_handler(), options);
 
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
index 9fba0f32d33..4c895d2a3da 100644
--- a/jbmc/src/java_bytecode/java_bytecode_language.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -645,6 +645,15 @@ bool java_bytecode_languaget::typecheck(
   const std::string &)
 {
   PRECONDITION(language_options_initialized);
+  // There are various cases in the Java front-end where pre-existing symbols
+  // from a previous load are not handled. We just rule this case out for now;
+  // a user wishing to ensure a particular class is loaded should use
+  // --java-load-class (to force class-loading) or
+  // --lazy-methods-extra-entry-point (to ensure a method body is loaded)
+  // instead of creating two instances of the front-end.
+  INVARIANT(
+    symbol_table.begin() == symbol_table.end(),
+    "the Java front-end should only be used with an empty symbol table");
 
   java_internal_additions(symbol_table);
 
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index b0bc9e2e8e2..2c047108b34 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -530,6 +530,23 @@ int jbmc_parse_optionst::doit()
   stub_objects_are_not_null =
     options.get_bool_option("java-assume-inputs-non-null");
 
+  if(cmdline.args.empty())
+  {
+    error() << "Please provide a program to verify" << eom;
+    return 6;
+  }
+
+  if(cmdline.args.size() != 1)
+  {
+    error() << "Only one .class, .jar or .gbf file should be directly "
+      "specified on the command-line. To force loading another another class "
+      "use '--java-load-class somepackage.SomeClass' or "
+      "'--lazy-methods-extra-entry-point somepackage.SomeClass.method' along "
+      "with '--classpath'"
+            << messaget::eom;
+    return 6;
+  }
+
   if(!cmdline.isset("symex-driven-lazy-loading"))
   {
     std::unique_ptr<goto_modelt> goto_model_ptr;
@@ -716,12 +733,6 @@ int jbmc_parse_optionst::get_goto_program(
   std::unique_ptr<goto_modelt> &goto_model,
   const optionst &options)
 {
-  if(cmdline.args.empty())
-  {
-    error() << "Please provide a program to verify" << eom;
-    return 6;
-  }
-
   {
     lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object(
       *this, options, get_message_handler());