Z3: str.indexof выдает неожиданный ответ, почему?

mjblackhorse спросил: 07 октября 2018 в 11:21 в: string

Я попытался решить следующую проблему с Z3:

(declare-const b String)
(assert (= 3 (str.indexof "abcdef" b)))
(check-sat)
(get-model)

я получил результат:

sat
(model
  (define-fun b () String 
    "de")
)

Однако, когда я попытался решить следующую проблему с Z3:

(declare-const b String)
(assert (= 4 (str.indexof "abcdef" b)))
(check-sat)
(get-model)

Но я получил результат:

unknown
Z3(4, 10): ERROR: model is not available

Это ошибка?


0 ответов