getString() results are ambiguous

[pointhi]

Simple a copy of a comment, to have a distinct bug report: #2286 (comment)

It seems String constants are not properly defined. This means, I'm able to create constants with different values, but reading them again causes one of the strings to alter in such a way to look like the other one. For example: \n and \\n will always read \\n.

    @Test
    public void shouldNotWorkTest() {
        Context ctx = new Context();

        Assert.assertEquals("\\n", ctx.mkString("\n").getString());
        Assert.assertEquals("\\n", ctx.mkString("\\n").getString());

        ctx.close();
    }

Unless, I use the API in a wrong way, this means Strings are not properly defined using the java interface. Actually, z3 should never try to escape strings, and simply return the internal representation. Otherwise every user needs to write a parser for escaped string constants.

[NikolajBjorner]

The java interface uses an underlying Z3_get_string function that produces an escaped string.
There is another API function Z3_get_lstring, which is for the non-escaped strings, but it may need a different prototype in order not to produce a java string, but a byte sequence that can be marshaled into a proper java string.

[NikolajBjorner]

Would be useful to get a hand on operating JNI conventions to finish this feature for Java.

[NikolajBjorner]

Seems there is no interest in fixing the Java bindings.
The python bindings now use Z3_get_lstring correctly.