Performance degradation in Z3 on QF_SLIA instances with fixed-length strings and prefix/suffix constraints

[wingsyuyi-satori]

The following instance is a QF_SLIA formula consisting of fixed-length constraints on three string variables together with a prefix/suffix/containment constraint:

(set-logic QF_SLIA)
(declare-const s0 String)
(declare-const s1 String)
(declare-const s2 String)
(assert (= (str.len s0) x))
(assert (= (str.len s1) x))
(assert (= (str.len s2) x))
(assert (or
  (and
    (str.prefixof "JJJJJ" s0)
    (str.suffixof "JJJJJ" s2)
  )
  (str.contains s1 "JJJJJ")
))
(check-sat)
(get-model)
(exit)

The instance was executed using z3 test.smt2 -st and /usr/bin/time -v cvc5 test.smt2 --produce-models.
While keeping the formula structure unchanged and only increasing the parameter x, Z3 exhibits significant performance degradation.

As x increases, the behavior of Z3 and cvc5 is summarized as follows.

Z3 results:

x (string length)	Result	Total Time (s)	Max Memory (MB)	Current Memory (MB)
20	sat	0.16	37.37	18.74
30	sat	29.14	163.93	28.93
40	sat	274.28	552.98	82.79
50	sat	486.29	525.23	82.88
60	sat	2002.72	1457.14	154.27

In contrast, cvc5 consistently solves the same instances in approximately 0.02 seconds, with a peak memory usage of around 23 MB across all tested values of x.

The version of Z3 used in this experiment is:
Z3 [version 4.15.5 - 64 bit] (C) Copyright 2006–2016 Microsoft Corp.