Timeout on Simple String Formula

[levinwinter]

z3 is able to solve seed.smt2 nearly instantly but cannot solve the even simpler bug.smt2.

$ cat seed.smt2 
(set-logic QF_S)
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert (= (str.++ (str.++ (str.++ a "bcc") b) c) (str.++ (str.++ (str.++ b "ba") a) "ab")))
(check-sat)
$ time z3 seed.smt2 
unsat

real    0m0.032s
user    0m0.023s
sys     0m0.009s

The formula is unsat, therefore we can replace a free variable with a concrete value, wich preserve unsatisfiability and reduce the search space. Ultimately, the new formula should be at most as difficult to solve as the original one, expecting equivalent or shorter wallclock time. However, z3 is not able to solve the subsituted formula anymore.

$ sed 's/(declare-fun a () String)/(define-fun a () String "")/g' seed.smt2 > bug.smt2
$ diff seed.smt2 bug.smt2
 (set-logic QF_S)
-(declare-fun a () String)
+(define-fun a () String "")
 (declare-fun b () String)
 (declare-fun c () String)
 (assert (= (str.++ (str.++ (str.++ a "bcc") b) c) (str.++ (str.++ (str.++ b "ba") a) "ab")))
$ timeout -s 9 120 z3 bug.smt2
Killed

z3 version/commit: b2b3bab (master)
Operating system: Debian GNU/Linux 12 (bookworm)

[NikolajBjorner]

Contrary to the file name, it is not a bug. Z3 uses a set of decomposition rules for solving equalities. It so happens that the rule for when you have variables a, b, c is more powerful than rules where there are only two variables in the equation. This is an implementation limitation.

@CEisenhofer

[levinwinter]

Sorry for the imprecise wording, you are absolutely right! Am I correctly assuming that whatever makes the rules for three variables powerful could also be implemented in the two variables rule?

This report is output of a performance fuzzing project which aimed to uncover formulas that Z3 “should" be able to solve but cannot. Does the Z3 project value such contributions that could help to make the solver more complete or is this not a priority? If so, we could post a few more cases here on GitHub involving other theories.