diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/My.class b/jbmc/regression/jbmc/assume-inputs-non-null/My.class
new file mode 100644
index 00000000000..ee262398832
Binary files /dev/null and b/jbmc/regression/jbmc/assume-inputs-non-null/My.class differ
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/My.java b/jbmc/regression/jbmc/assume-inputs-non-null/My.java
new file mode 100644
index 00000000000..82b660a109f
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/My.java
@@ -0,0 +1,41 @@
+class My {
+
+  String field;
+
+  public static void stringArrayArg(String[] arg) {
+    if (arg == null) {
+      assert false;
+    } else {
+      assert false;
+    }
+  }
+
+  public static void stringArg(String arg) {
+    if (arg == null) {
+      assert false;
+    } else {
+      assert false;
+    }
+  }
+
+  public static void classArg(Other arg) {
+    if (arg == null) {
+      assert false;
+    } else if (arg.stringField != null) {
+      assert false;
+    } else if (arg.otherField != null) {
+      assert false;
+    } else if (arg.other2Field != null) {
+      assert false;
+    }
+  }
+
+  public void field() {
+    if (field == null) {
+      assert false;
+    } else {
+      assert false;
+    }
+  }
+
+}
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other.class b/jbmc/regression/jbmc/assume-inputs-non-null/Other.class
new file mode 100644
index 00000000000..5e090a36a8e
Binary files /dev/null and b/jbmc/regression/jbmc/assume-inputs-non-null/Other.class differ
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other.java b/jbmc/regression/jbmc/assume-inputs-non-null/Other.java
new file mode 100644
index 00000000000..29147a4b146
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/Other.java
@@ -0,0 +1,7 @@
+class Other {
+
+  String stringField;
+  Other otherField;
+  Other2 other2Field;
+
+}
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other2.class b/jbmc/regression/jbmc/assume-inputs-non-null/Other2.class
new file mode 100644
index 00000000000..29d7b35b2b8
Binary files /dev/null and b/jbmc/regression/jbmc/assume-inputs-non-null/Other2.class differ
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/Other2.java b/jbmc/regression/jbmc/assume-inputs-non-null/Other2.java
new file mode 100644
index 00000000000..f6ede9ec397
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/Other2.java
@@ -0,0 +1,5 @@
+class Other2 {
+
+  String string2Field;
+
+}
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc
new file mode 100644
index 00000000000..5500fde1a3a
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc
@@ -0,0 +1,16 @@
+CORE
+My.class
+--function My.classArg --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::My.classArg:\(LOther;\)V.assertion.1\].*SUCCESS
+\[java::My.classArg:\(LOther;\)V.assertion.2\].*FAILURE
+\[java::My.classArg:\(LOther;\)V.assertion.3\].*FAILURE
+\[java::My.classArg:\(LOther;\)V.assertion.4\].*FAILURE
+--
+^warning: ignoring
+--
+Check that --java-assume-inputs-non-null restricts inputs to non-null user-
+defined objects.
+Also verify that fields of input object are NOT constrained to be non-null.
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/field_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/field_assume.desc
new file mode 100644
index 00000000000..22392dbcdd5
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/field_assume.desc
@@ -0,0 +1,13 @@
+CORE
+My.class
+--function My.field --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::My.field:\(\)V.assertion.1\].*FAILURE
+\[java::My.field:\(\)V.assertion.2\].*FAILURE
+--
+^warning: ignoring
+--
+Check that --java-assume-inputs-non-null does NOT constrain the fields of the
+containing object to be non-null.
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc
new file mode 100644
index 00000000000..380155662ce
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_assume.desc
@@ -0,0 +1,12 @@
+CORE
+My.class
+--function My.stringArrayArg --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::My.stringArrayArg:\(\[Ljava/lang/String;\)V.assertion.1\].*SUCCESS
+\[java::My.stringArrayArg:\(\[Ljava/lang/String;\)V.assertion.2\].*FAILURE
+--
+^warning: ignoring
+--
+Check that --java-assume-inputs-non-null restricts inputs to non-null arrays
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc
new file mode 100644
index 00000000000..31d9ced1e21
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_array_no_assume.desc
@@ -0,0 +1,13 @@
+CORE
+My.class
+--function My.stringArrayArg
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::My.stringArrayArg:\(\[Ljava/lang/String;\)V.assertion.1\].*FAILURE
+\[java::My.stringArrayArg:\(\[Ljava/lang/String;\)V.assertion.2\].*FAILURE
+--
+^warning: ignoring
+--
+Sanity check: null inputs are allowed when not using
+--java-assume-inputs-non-null.
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc
new file mode 100644
index 00000000000..7f0bfac98ce
--- /dev/null
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/string_assume.desc
@@ -0,0 +1,12 @@
+CORE
+My.class
+--function My.stringArg --java-assume-inputs-non-null
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+\[java::My.stringArg:\(Ljava/lang/String;\)V.assertion.1\].*SUCCESS
+\[java::My.stringArg:\(Ljava/lang/String;\)V.assertion.2\].*FAILURE
+--
+^warning: ignoring
+--
+Check that --java-assume-inputs-non-null restricts inputs to non-null strings