Various cleanups

Author: peterschrammel

src/main/java/java/lang/Double.java

@@ -816,7 +816,7 @@ public static int hashCode(double value) {
      * @diffblue.fullSupport
      *
      * Until the native method doubleToRawLongBits(D) is implemented in
-     * CBMC, this model will allow test generation for checking equality
+     * CBMC, this model will allow JBMC for checking equality
      * between two Doubles.
      */
     public boolean equals(Object obj) {

src/main/java/java/lang/Float.java

@@ -716,7 +716,7 @@ public static int hashCode(float value) {
      * @diffblue.fullSupport
      *
      * Until the native method floatToRawIntBits(F) is implemented in
-     * CBMC, this model will allow test generation for checking equality
+     * CBMC, this model will allow JBMC for checking equality
      * between two Floats.
      */
     public boolean equals(Object obj) {

src/main/java/java/lang/Math.java

@@ -364,12 +364,10 @@ public static double log10(double a) {
      * result of sqrt is equal to the original number, which is not always
      * true. As a result, the solver will return UNSAT in many cases.
      * For instance, {@code Math.sqrt(2.0)} will cause the solver to be UNSAT.
-     * Reported in: TG-5598
      *
      * Also, there are precision issues on very small numbers. For instance,
      * for values between 0 and {@code 0x0.0000000000001p-900}, the sqrt method
      * is likely to not be equal to the result of the real Math.sqrt method.
-     * Reported in: TG-5602
      */
     public static double sqrt(double a) {
         // return StrictMath.sqrt(a); // default impl. delegates to StrictMath

src/main/java/java/lang/StringBuffer.java

@@ -333,7 +333,7 @@ public synchronized void setCharAt(int index, char ch) {
 
     /**
      * @diffblue.limitedSupport
-     * This method can be slow to generate tests due to TG-2866 and is
+     * This method can be slow to generate tests due to an issue and is
      * also limited by which {@code toString()} methods have been modelled.
      */
     @Override

src/main/java/java/lang/StringBuilder.java

@@ -156,7 +156,7 @@ public StringBuilder(CharSequence seq) {
 
     /**
      * @diffblue.limitedSupport
-     * This method can be slow to generate tests due to TG-2866 and is
+     * This method can be slow to generate tests due to an issue and is
      * also limited by which {@code toString()} methods have been modelled.
      */
     @Override

src/main/java/java/util/Random.java

@@ -188,7 +188,7 @@ public Random(long seed) {
      *
      * @diffblue.mock
      * @diffblue.limitedSupport
-     * We currently ignore seeds and make test-generator pick return values
+     * We currently ignore seeds and make JBMC pick return values
      * for the methods in this class nondeterministically rather than
      * calculating them according to a probability distribution. So this
      * method is simply modelled as a no-op.
@@ -374,7 +374,7 @@ public void nextBytes(byte[] bytes) {
      *
      * @diffblue.fullSupport
      * This method returns a nondeterministic {@code int} value.
-     * The nondeterminism is introduced by test-generator itself, and
+     * The nondeterminism is introduced by JBMC itself, and
      * probability distributions are ignored.
      *
      * @diffblue.mock
@@ -441,9 +441,9 @@ public int nextInt() {
      * @diffblue.limitedSupport
      * This method returns a nondeterministic {@code int} value between 0
      * (inclusive) and {@code bound} (exclusive).
-     * The nondeterminism is introduced by test-generator itself, and
+     * The nondeterminism is introduced by JBMC itself, and
      * probability distributions are ignored.
-     * Exceptions for mocked methods are currently not supported, see TG-1387.
+     * Exceptions for mocked methods are currently not supported.
      *
      * @diffblue.mock
      */
@@ -522,7 +522,7 @@ public long nextLong() {
      *
      * @diffblue.fullSupport
      * This method returns a nondeterministic {@code boolean} value.
-     * The nondeterminism is introduced by test-generator itself, and
+     * The nondeterminism is introduced by JBMC itself, and
      * probability distributions are ignored.
      *
      * @diffblue.mock
@@ -572,7 +572,7 @@ public boolean nextBoolean() {
      * @diffblue.fullSupport
      * This method returns a nondeterministic {@code float} value between 0.0
      * (inclusive) and 1.0 (exclusive).
-     * The nondeterminism is introduced by test-generator itself, and
+     * The nondeterminism is introduced by JBMC itself, and
      * probability distributions are ignored.
      *
      * @diffblue.mock
@@ -626,7 +626,7 @@ public float nextFloat() {
      * @diffblue.fullSupport
      * This method returns a nondeterministic {@code double} value between 0.0
      * (inclusive) and 1.0 (exclusive).
-     * The nondeterminism is introduced by test-generator itself, and
+     * The nondeterminism is introduced by JBMC itself, and
      * probability distributions are ignored.
      *
      * @diffblue.mock
@@ -688,7 +688,7 @@ public double nextDouble() {
      *
      * @diffblue.fullSupport
      * This method returns a nondeterministic {@code double} value.
-     * The nondeterminism is introduced by test-generator itself, and
+     * The nondeterminism is introduced by JBMC itself, and
      * probability distributions are ignored.
      *
      * @diffblue.mock