search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.43k stars 1.47k forks source link

Invalid model issue on QF_SLIA #6563

Closed depted closed 1 year ago

depted commented 1 year ago

Greetings, For this instance, an invalid bug occurred. We tried to make this instance as small as possible. We sincerely hope that our report would be helpful for the z3 team.

commit: 304b316

$ ./z3 ./small.smt2 model_validate=true
sat
(error "line 4 column 10: an invalid model was generated")

$ cat ./small.smt2
(declare-fun v () String)
(declare-fun m () Int)
(assert (< 0 (- (- (seq.last_indexof "JH" v)) m)))
(check-sat)
NikolajBjorner commented 1 year ago

File fuzz bugs into appropriate consolidated bugs (there is one for sequences).

depted commented 1 year ago

@NikolajBjorner Thanks for letting me know, I'll do it. However, I do not know what is 'appropriate consolidated bugs' that you mentioned. I found some issues in this repo related to seq however, I could not find something that has consolidated bugs. Could I know which one is the issue that I need to file?

NikolajBjorner commented 1 year ago

https://github.com/Z3Prover/z3/issues/6346