String.format produces errors in set_to

[allredj]

The tests introduced in #1105 (but almost certainly elsewhere) generate type inconsistencies.
For instance, the test cbmc/regression/strings-smoke-tests/java_format2/test.desc:

public class test
{
    public static String main(String str)
    {
        String s = String.format("foo %s", str);
        assert(s.equals("foo ".concat(str)));
        assert(!s.equals("foo ".concat(str)));
        return s;
    }
}

with the following command line:

cbmc test.class --refine-strings --string-max-length 20 --verbosity 9

generates the following warnings:

converting SSA
ignoring tmp_object$18!0#1 == &dynamic_object3 [inconsistent types]
ignoring tmp_object$33!0#1 == &dynamic_object4 [inconsistent types]
ignoring tmp_object$48!0#1 == &dynamic_object5 [inconsistent types]
ignoring tmp_object$63!0#1 == &dynamic_object6 [inconsistent types]
ignoring tmp_object$78!0#1 == &dynamic_object7 [inconsistent types]
ignoring tmp_object$93!0#1 == &dynamic_object8 [inconsistent types]
ignoring tmp_object$108!0#1 == &dynamic_object9 [inconsistent types]
ignoring tmp_object$123!0#1 == &dynamic_object10 [inconsistent types]
ignoring tmp_object$138!0#1 == &dynamic_object11 [inconsistent types]
ignoring tmp_object$153!0#1 == &dynamic_object12 [inconsistent types]

[allredj]

This is a fairly serious issue, as some equalities are not added to the solver and could explain some of the non-terminating cases that we have.

[allredj]

This issue was created on the wrong repository. The test-gen issue is here:
https://github.com/diffblue/test-gen/issues/913

[TGWDB]

"[C]reated on the wrong repository.", closing.