Make unsupported case notModelled instead of using assume

Under-approximated models can lead to spurious UNSAT results
in JBMC; however, we can mark over-approximated cases as
notModelled and JBMC will detect them and give a warning that
behaviour is over-approximating when reporting SAT.

Author: peterschrammel

src/main/java/java/lang/String.java

@@ -2996,8 +2996,7 @@ public String replaceAll(String regex, String replacement)
     {
         // return Pattern.compile(regex).matcher(this).replaceAll(replacement);
         // DIFFBLUE MODELS LIBRARY: we assume the expression is just a string literal
-        CProver.assume(
-            regex.indexOf('[') == -1 &&
+        if (regex.indexOf('[') == -1 &&
             regex.indexOf(']') == -1 &&
             regex.indexOf('.') == -1 &&
             regex.indexOf('\\') == -1 &&
@@ -3010,8 +3009,12 @@ public String replaceAll(String regex, String replacement)
             regex.indexOf('}') == -1 &&
             regex.indexOf('|') == -1 &&
             regex.indexOf('(') == -1 &&
-            regex.indexOf(')') == -1);
-        return replace(regex, replacement);
+            regex.indexOf(')') == -1) {
+            return replace(regex, replacement);
+        } else {
+            CProver.notModelled();
+            return CProver.nondetWithNullForNotModelled();
+        }
     }
 
     /**