Problematic character constants in solver.toString() in Java API

[facferreira]

While trying the following snippet to check the final solver.toString():

Context context1 = new Context();
Solver solver1 = context1.mkSolver();

BoolExpr expr1 = context1.parseSMTLIB2String("(assert (= \"\\x41\" \"A\"))", null, null, null, null);
solver1.add(expr1);

BoolExpr expr2 = context1.parseSMTLIB2String("(assert (not (= \"\\x22\" \"A\")))", null, null, null, null);
solver1.add(expr2);

BoolExpr expr3 = context1.parseSMTLIB2String("(assert (not (= \"\\x7F\" \"A\")))", null, null, null, null);
solver1.add(expr3);

System.out.println(solver1.toString());

I noted that character constants were printed wrongly (double quotes) or in an unexpected way. For this snippet, solver.toString() returned:

(assert (= "A" "A"))
(assert (not (= """" "A")))
(assert (not (= "" "A")))

Despite the first assert has no problem, the second printed two double quotes (shouldn't it be just one double quote? even in that case, it wouldn't need to be escaped to not conflict with the encapsulating double quotes?). Finally, the third assert I expected it to print "\x7F" instead of "".

[facferreira]

To add more information to the issue: Possibly due to this, If I have in any place the line

(ite (str.contains s "\x01") (pct_encode_step1 (str.replace s "\x01" "\x0001"))

repeated replacing \x01 by each double hexadecimal digit. That is,

(ite (str.contains s "\x01") (pct_encode_step1 (str.replace s "\x01" "\x0001"))
(ite (str.contains s "\x02") (pct_encode_step1 (str.replace s "\x02" "\x0002"))
...
(ite (str.contains s "\xFF") (pct_encode_step1 (str.replace s "\xFF" "\x00FF"))

The the final solver.toString() is not complete. It doesn't finish the string correctly, it seems like it was truncated. Is it possibly due to some not escaped characters?

[NikolajBjorner]

We follow the SMT-LIB2 format for string literals. "" is an escape for ", so a single quote " is printed as a string """".

For \x7F, this is the "DEL" character and advertised as printable. The first 32 ascii characters are advertised as non-printable.

[NikolajBjorner]

closing as DEL is printed as I believe it should.