diff --git a/regression/cbmc-java/assertion_error_constructors/AssertionIssue.class b/regression/cbmc-java/assertion_error_constructors/AssertionIssue.class
new file mode 100644
index 00000000000..a9312303951
Binary files /dev/null and b/regression/cbmc-java/assertion_error_constructors/AssertionIssue.class differ
diff --git a/regression/cbmc-java/assertion_error_constructors/AssertionIssue.java b/regression/cbmc-java/assertion_error_constructors/AssertionIssue.java
new file mode 100644
index 00000000000..b82d7b46df3
--- /dev/null
+++ b/regression/cbmc-java/assertion_error_constructors/AssertionIssue.java
@@ -0,0 +1,13 @@
+public class AssertionIssue {
+
+    public static void throwAssertion() {
+        throw new AssertionError("Something went terribly wrong.", new ThrowableAssertion());
+    }
+
+    public static class ThrowableAssertion extends Throwable {
+        @Override
+        public String getMessage() {
+            return "How did we get here?";
+        }
+    }
+}
diff --git a/regression/cbmc-java/assertion_error_constructors/test.desc b/regression/cbmc-java/assertion_error_constructors/test.desc
new file mode 100644
index 00000000000..fde9624618f
--- /dev/null
+++ b/regression/cbmc-java/assertion_error_constructors/test.desc
@@ -0,0 +1,8 @@
+CORE
+AssertionIssue.class
+--function AssertionIssue.throwAssertion
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 35e67c16b5e..c7cfe83fda4 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -969,11 +969,11 @@ void goto_convertt::do_function_call_symbol(
 
     copy(function_call, FUNCTION_CALL, dest);
 
-    if(arguments.size()!=1 && arguments.size()!=2)
+    if(arguments.size() != 1 && arguments.size() != 2 && arguments.size() != 3)
     {
       error().source_location=function.find_source_location();
       error() << "`" << identifier
-              << "' expected to have one or two arguments" << eom;
+              << "' expected to have one, two or three arguments" << eom;
       throw 0;
     }