diff --git a/src/tests/NullCharsetTest.java b/src/tests/NullCharsetTest.java
new file mode 100644
index 00000000..d0233eeb
--- /dev/null
+++ b/src/tests/NullCharsetTest.java
@@ -0,0 +1,23 @@
+import gov.nasa.jpf.util.test.TestJPF;
+import org.junit.Test;
+import java.nio.file.Path;
+
+public class NullCharsetTest extends TestJPF
+{ 
+    @Test
+    public void testDirectPathEntry()
+    { 
+        if (verifyNoPropertyViolation())
+        { 
+            try { 
+                Path.of("/tmp");
+            } catch (IllegalArgumentException iae)
+            { 
+                if ("Null charset name".equals(e.getMessage()))
+                { 
+                    fail("IllegalArgumentException with 'Null charset name' encountered");
+                }
+            }
+        }
+    }
+}
\ No newline at end of file