Non-Terminating Z3Str3 from z3-4.8.9-x64-ubuntu-16.04

I am having a problem when trying to use the Z3Str3 from z3-4.8.9-x64-ubuntu-16.04 notably if I substitute the com.microsoft.z3.jar to the one in z3-4.8.8-x64-ubuntu-16.04 I no longer have that issue. The problem is that the Z3 process never comes back with a result, despite the simplicity of the query. I noticed though that it returns the valid answer when I kill my program. I am not noticing that behavior when I am trying to run the same query on the executable, so I am guessing there is something about using the jar file that I might need to tweak one way or the other.

Here is my code. I am using Ubuntu 16.04 LTS, and IntelliJ version ultimate 2020.3.

Many thanks!

import com.microsoft.z3.*;
public class Z3String3Processor_reduced {
    public static void main(String[] args) {
        StringBuilder currentQuery = new StringBuilder("\n" +
                "(declare-const string0 String)\n" +
                "(assert (= (str.indexof string0 \"a\" 1) 6))\n" +
                "(check-sat)\n" +
                "(get-model)\n" +
                "\n");
        Context context1 = new Context();
        Solver solver1 = context1.mkSolver();
        Params params = context1.mkParams();
        params.add("smt.string_solver", "z3str3");
        solver1.setParameters(params);
        StringBuilder finalQuery = new StringBuilder(currentQuery.toString());

        // attempt to parse the query, if successful continue with checking satisfiability
        try {

            // throws z3 exception if malformed or unknown constant/operation
            BoolExpr[] assertions = context1.parseSMTLIB2String(finalQuery.toString(), null, null, null, null);
            solver1.add(assertions);
            // check sat, if so we can go ahead and get the model....
            if (solver1.check() == Status.SATISFIABLE) {
                System.out.println("sat");
            } else
                System.out.println("not sat");
            context1.close();
        } catch (Z3Exception e) {
            System.out.println("Z3 exception: " + e.getMessage());
        }
    }
}

Solution

I don't think this has anything to do with Java. Let's extract your query and put it in a file named a.smt2:

$ cat a.smt2
(declare-const string0 String)
(assert (= (str.indexof string0 "a" 1) 6))
(check-sat)
(get-model)

Now, if I run:

$ z3 a.smt2
sat
(
  (define-fun string0 () String
    "FBCADEaGaa")
)

That's good. But if I run:

$ z3  smt.string_solver=z3str3 a.smt2
... does not terminate ..

So, bottom line, your query (as simple as it looks), gives hard time to the z3str3 solver.

I see that you already reported this as a bug at https://github.com/Z3Prover/z3/issues/5673

Given that the default string-solver can handle the query just fine, why not just use that one? If you have to use z3str3 for some other reason, then you've found a case where it doesn't handle this query well; I'm not sure how inclined the z3 folks will be to fix this given the query is handled by the default solver rather quickly. Please report what you find out!