Invalid model for string index when symbolic string is not contained in the other string

[tlringer]

Hi again, I have another invalid model with strings. Here I am checking that whenever one string does not contain the other, there is no index at which the other string appears as a substring of the first string:

(set-option :model-validate true)

(declare-fun c0 () String)
(declare-fun c1 () String)
(declare-fun c2 () Int)
(assert (<= 0 (str.indexof c0 c1 c2)))
(assert (not (str.contains c0 c1)))
(assert (< c2 (str.len c0)))
(check-sat)

(get-model)

Z3 returns a negative index, then recognizes that it is an invalid model:

sat
(error "line 9 column 10: an invalid model was generated")
(model 
  (define-fun c2 () Int
    (- 1))
  (define-fun c0 () String
    "")
  (define-fun c1 () String
    "\x00")
)

I know that str.at is undefined with negative offset -- here it looks like Z3 is generating a negative offset for string.index. Is this defined? The line that fails with that model is:

(assert (<= 0 (str.indexof c0 c1 c2)))

Should I be constraining c2 to always be greater than or equal to zero myself?

Thanks again!

Talia

[tlringer]

If I add an extra line that constrains c2 to be greater than or equal to zero:

(set-option :model-validate true)

(declare-fun c0 () String)
(declare-fun c1 () String)
(declare-fun c2 () Int)
(assert (<= 0 (str.indexof c0 c1 c2)))
(assert (not (str.contains c0 c1)))
(assert (< c2 (str.len c0)))
(assert (<= 0 c2))
(check-sat)

(get-model)

Then Z3 times out. (Maybe that is just generally a hard query, though.)

[NikolajBjorner]

My axiomatization had some things left to be desired. Perhaps still have, but it now addresses the issues you report.

[NikolajBjorner]

this is fixed.