Z3 might be inconsistent when solving this string problem?

Question

I just encountered a SMTLIB problem in string theory that Z3 might have answered inconsistently. When envoking Z3 to solve the problem: with argument smt.string_solver=z3str3 it returns unsat; without any arguments it returns sat.

I also used CVC4 to solve the problem. It returned a solution, which seems to be a valid model as I checked it by manually replacing the variable assignments into the problem.

Since I'm trying to do a research using Z3, I would like to know if this is a known behavior of Z3. Thanks to anyone that could help! :)

Edit: I was using Z3 4.7.1 on WSL Ubuntu 16.04.

Answer 1

I'd say that getting unsat or sat, depending on Z3's configuration, sounds like a bug to me. Check the Z3 issue tracker for issues that describe a similar behaviour, and if nothing pops up, file an issue there. Ideally with a minimal example to reproduce the problem with, your current one is rather long.