Можно ли использовать Z3 для рассуждений о подстроках?

Я пытаюсь использовать Z3, чтобы рассуждать о подстроках, и наткнулся на некоторые не- интуитивное поведение. Z3 возвращает «sat», когда его спрашивают, присутствует ли «xy» в «xy», но возвращает «unknown», когда его спрашивают, находится ли «x» в «x» или «x» находится в «xy».

Я прокомментировал следующий код, чтобы проиллюстрировать это поведение:

(set-logic AUFLIA)
(declare-sort Char 0)

;characters to build strings are _x_ and _y_
(declare-fun _x_ () Char)
(declare-fun _y_ () Char)
(assert (distinct _x_ _y_))

;string literals
(declare-fun findMeX () (Array Int Char))  
(declare-fun findMeXY () (Array Int Char))  
(declare-fun x () (Array Int Char))
(declare-fun xy () (Array Int Char))
(declare-fun length ( (Array Int Char) ) Int )

;set findMeX = 'x'
(assert (= (select findMeX 0) _x_))
(assert (= (length findMeX) 1))

;set findMeXY = 'xy'
(assert (= (select findMeXY 0) _x_))
(assert (= (select findMeXY 1) _y_))
(assert (= (length findMeXY) 2))

;set x = 'x'
(assert (= (select x 0) _x_))
(assert (= (length x) 1))

;set xy = 'xy'
(assert (= (select xy 0) _x_))
(assert (= (select xy 1) _y_))
(assert (= (length xy) 2))

Теперь, когда проблема установлена, мы пытаемся найти подстроки:

;search for findMeX='x' in x='x' 

(push 1)
(assert 
  (exists 
    ((offset Int)) 
    (and 
      (<= offset (- (length x) (length findMeX))) 
      (>= offset 0) 
      (forall 
        ((index Int)) 
        (=> 
          (and 
            (< index (length findMeX)) 
            (>= index 0)) 
          (= 
            (select x (+ index offset)) 
            (select findMeX index)))))))

(check-sat) ;'sat' expected, 'unknown' returned
(pop 1)

Если вместо этого мы ищем findMeXY в xy , решающая программа возвращает "sat", как и ожидалось. Казалось бы, поскольку решатель может обрабатывать этот запрос для «xy», он должен иметь возможность обрабатывать его для «x». Кроме того, при поиске findMeX = 'x' в 'xy =' xy ' возвращается «неизвестно».

Может ли кто-нибудь предложить объяснение или, возможно, альтернативную модель для выражения этой проблемы в решателе SMT?