MkStringLt/MkStringLe does not seem to work...

[jiong-sapientai]

I did a simple test program for it,
@test
void stringComparisonTest() {
Expr<SeqSort> stringExpr1 = context.mkConst("a", context.getStringSort());
Expr<SeqSort> stringExpr2 = context.mkConst("b", context.getStringSort());
BoolExpr b = context.MkStringLe(stringExpr1.getSort(), stringExpr2.getSort());
Model m = z3ContextManager.solveValuesWithoutUuid();
System.out.println(m.evaluate(b, true));
}

and it gives me an assertion failure in Z3:

ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 415
UNEXPECTED CODE WAS REACHED.
Z3 4.11.2.0

any pointers on this?

[NikolajBjorner]

You should repro it with the current version of Z3 (pull bits from the nightly build).
https://github.com/Z3Prover/z3/releases/tag/Nightly

Then before you create the context invoke Log.open("z3.log")

Then share the file z3.log for repro

[jiong-sapientai]

Thanks. Attached please see the log, I still see the same issue there.
z3.log