StringBuilderConstructors01 exposes in fact a violation_witness due to overflow when following Java Spec

[pointhi]

Creation of a StringBuilder with an input string of size Integer.MAX_INT-15 will cause an NegativeArraySizeException during construction:

sv-benchmarks/java/jbmc-regression/StringBuilderConstructors01/Main.java

Lines 13 to 19 in f86649d

	String arg = Verifier.nondetString();
	if (arg.length() < 1)
	return;
	StringBuilder buffer1 = new StringBuilder();
	StringBuilder buffer2 = new StringBuilder(10);
	StringBuilder buffer3 = new StringBuilder(arg);

Looking into the library the constructors are defined as follows:

    public StringBuilder(String str) {
        super(str.length() + 16);
        append(str);
    }

    AbstractStringBuilder(int capacity) {
        value = new char[capacity];
    }

The term of str.length() + 16 is not some implementation specific detail, but is defined in the Java documentation:

https://docs.oracle.com/javase/8/docs/api/java/lang/StringBuilder.html#StringBuilder-java.lang.String-

Constructs a string builder initialized to the contents of the specified string. The initial capacity of the string builder is 16 plus the length of the string argument.

[pointhi]

Likely related to #884

[mmuesly]

As said for #1096, given the current rule set this does not classify as violation_witness as it is not an assertion violation. We might add the NegativeArraySizeException to the property definition in the future.