diff --git a/jbmc/regression/jbmc/unicode-class-filename/test.desc b/jbmc/regression/jbmc/unicode-class-filename/test.desc
new file mode 100644
index 00000000000..3bc410091b9
--- /dev/null
+++ b/jbmc/regression/jbmc/unicode-class-filename/test.desc
@@ -0,0 +1,8 @@
+CORE
+ЮЛ
+--
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+Test that .class suffix is properly stripped for Unicode class names
\ No newline at end of file
diff --git "a/jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.class" "b/jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.class"
new file mode 100644
index 00000000000..1b4f30f4770
Binary files /dev/null and "b/jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.class" differ
diff --git "a/jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.java" "b/jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.java"
new file mode 100644
index 00000000000..4b92533b12c
--- /dev/null
+++ "b/jbmc/regression/jbmc/unicode-class-filename/\320\256\320\233.java"
@@ -0,0 +1,12 @@
+public class ЮЛ
+{
+  static void f()
+  {
+    assert false;
+  }
+
+  public static void main(String[] args)
+  {
+    ЮЛ.f();
+  }
+}
\ No newline at end of file
diff --git a/jbmc/regression/jbmc/unicode-class-name/test.desc b/jbmc/regression/jbmc/unicode-class-name/test.desc
new file mode 100644
index 00000000000..9581d9f964e
--- /dev/null
+++ b/jbmc/regression/jbmc/unicode-class-name/test.desc
@@ -0,0 +1,8 @@
+CORE
+ЮЛ
+--
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+Test Unicode characters in Java class names
diff --git "a/jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.class" "b/jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.class"
new file mode 100644
index 00000000000..1d50a7d016c
Binary files /dev/null and "b/jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.class" differ
diff --git "a/jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.java" "b/jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.java"
new file mode 100644
index 00000000000..e77f72fb4d3
--- /dev/null
+++ "b/jbmc/regression/jbmc/unicode-class-name/\320\256\320\233.java"
@@ -0,0 +1,13 @@
+public class ЮЛ
+{
+  void f()
+  {
+    assert false;
+  }
+
+  public static void main(String[] args)
+  {
+    ЮЛ obj = new ЮЛ();
+    obj.f();
+  }
+}
diff --git a/jbmc/regression/jbmc/unicode-method-name/f.class b/jbmc/regression/jbmc/unicode-method-name/f.class
new file mode 100644
index 00000000000..89ece316f8f
Binary files /dev/null and b/jbmc/regression/jbmc/unicode-method-name/f.class differ
diff --git a/jbmc/regression/jbmc/unicode-method-name/f.java b/jbmc/regression/jbmc/unicode-method-name/f.java
new file mode 100644
index 00000000000..64c05f51bc6
--- /dev/null
+++ b/jbmc/regression/jbmc/unicode-method-name/f.java
@@ -0,0 +1,13 @@
+public class f
+{
+  void ЮЛ()
+  {
+    assert false;
+  }
+
+  public static void main(String[] args)
+  {
+    f obj = new f();
+    obj.ЮЛ();
+  }
+}
\ No newline at end of file
diff --git a/jbmc/regression/jbmc/unicode-method-name/test.desc b/jbmc/regression/jbmc/unicode-method-name/test.desc
new file mode 100644
index 00000000000..dc97ccf00ea
--- /dev/null
+++ b/jbmc/regression/jbmc/unicode-method-name/test.desc
@@ -0,0 +1,8 @@
+CORE
+f
+--
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+Test Unicode characters in Java method names (should already work)
\ No newline at end of file
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
index 79b712d55d1..8d64148c94c 100644
--- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp
+++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/exit_codes.h>
 #include <util/help_formatter.h>
 #include <util/options.h>
+#include <util/suffix.h>
 #include <util/version.h>
 
 #include <goto-programs/goto_check.h>
@@ -355,6 +356,11 @@ int janalyzer_parse_optionst::doit()
   if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree"))
   {
     std::string main_class = cmdline.args[0];
+
+    // Strip .class suffix if present (to support filenames like "ClassName.class")
+    if(has_suffix(main_class, ".class"))
+      main_class.resize(main_class.size() - 6);
+
     // `java` accepts slashes and dots as package separators
     std::replace(main_class.begin(), main_class.end(), '/', '.');
     config.java.main_class = main_class;
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
index 7ed4105af63..a16a3aa0172 100644
--- a/jbmc/src/jbmc/jbmc_parse_options.cpp
+++ b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/exit_codes.h>
 #include <util/help_formatter.h>
 #include <util/invariant.h>
+#include <util/suffix.h>
 #include <util/version.h>
 #include <util/xml.h>
 
@@ -433,6 +434,11 @@ int jbmc_parse_optionst::doit()
   if((cmdline.args.size() == 1) && !cmdline.isset("show-parse-tree"))
   {
     std::string main_class = cmdline.args[0];
+
+    // Strip .class suffix if present (to support filenames like "ClassName.class")
+    if(has_suffix(main_class, ".class"))
+      main_class.resize(main_class.size() - 6);
+
     // `java` accepts slashes and dots as package separators
     std::replace(main_class.begin(), main_class.end(), '/', '.');
     config.java.main_class = main_class;