Invalid model for String formula (z3str3)

[rainoftime]

Hi, for the following formula

(set-option :model_validate true)
(set-option :model true)
(set-option :smt.string_solver z3str3)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const i8 Int)
(declare-const i0 Int)
(declare-const Str3 String)
(declare-const Str8 String)
(declare-const Str9 String)
(declare-const Str11 String)
(declare-const Str12 String)
(declare-const Str13 String)
(declare-const Str14 String)
(declare-const Str15 String)
(declare-const Str16 String)
(declare-const Str17 String)
(assert (xor (< 31 i0) v0 v4 (str.<= Str8 Str17) v2 v3 v3 v2 v2))
(declare-const v5 Bool)
(assert (xor v5 (= Str3 Str9 Str15 Str16 Str13) v0 v0 (str.<= Str8 Str17) v0 v2))
(assert (not (str.<= Str8 Str17)))
(check-sat)

z3 commit 5516e420a138 gives an invalid model

[rainoftime]

Reduced input

(set-option :model_validate true)
(set-option :smt.string_solver z3str3)
(declare-const Str17 String)
(assert (not (str.<= "" Str17)))
(check-sat)

[NikolajBjorner]

Is str.<= supported in z3str3?

[rainoftime]

Here is another case that uses str.<.

(set-option :model_validate true)
(set-option :smt.string_solver z3str3)
(declare-const Str1 String)
(assert (str.< Str1 ""))
(check-sat)

[zhendongsu]

There are, in fact, quite some open bugs in z3str3, which would be nice to get resolved first if possible. @mtrberzi

[NikolajBjorner]

I wonder what to do with z3str3 with respect to the support model.

From the bug reports it seems not stable enough for general consumption. There are now many bugs filed against z3str3 and it is taking time to address them.

There are formulas it can solve much better than seq, but other feedback on this issues thread have suggested it needed significant improvements.

The seq solver also desires many improvements; it could likely be improved a few order of magnitudes in performance with some care. It has shown to contain many bugs (correctness bugs that were filed are to my knowledge fixed, but I am sure more will be filed).

So from a usability perspective we are not in a great state: z3str3 has some good heuristics, but lacks quality and responsiveness to bug reports. seq gets retrofitted on demand and is made available as a default.

The general guideline for contributions to z3 has been responsiveness to bug reports and striving a higher quality bar. In this respect I wonder if it makes sense to disable z3str3 from the master branch, and reenable it if it reaches good a state of stability. Users who want it would have to compile a version where it isn't disabled. Disabling it is simple smt_setup.cpp determines which solvers are used. So it is done in one place.

[mtrberzi]

str.< and str.<= are not supported in Z3str3, but I can investigate adding support once some of the more pressing issues are addressed. I would suggest leaving Z3str3 available so that we can get feedback on these issues. Z3str3 is not the default solver and most users who want to use it are using the smt.string_solver option to select it and expect it to be available. I definitely agree that these existing issues should be addressed, and I am currently tackling several of the older open bugs.