Invalid model in Array logic with smt.threads=5

[muchang]

Hi,
For this formula:

(declare-fun foo ((Array Int (Array Int Real)) Int) Bool)
(declare-fun n () Int)
(declare-fun a0 () (Array Int (Array Int Real)))
(declare-fun a4 () (Array Int (Array Int Real)))
(declare-fun e4 () Real)
(declare-fun a7 () (Array Int (Array Int Real)))
(declare-fun a8 () (Array Int (Array Int Real)))
(declare-fun e8 () Real)
(declare-fun a9 () (Array Int (Array Int Real)))
(declare-fun e9 () Real)
(declare-fun a10 () (Array Int (Array Int Real)))
(declare-fun e10 () Real)
(declare-fun a11 () (Array Int (Array Int Real)))
(declare-fun e11 () Real)
(declare-fun a12 () (Array Int (Array Int Real)))
(declare-fun e12 () Real)
(declare-fun a13 () (Array Int (Array Int Real)))
(declare-fun e13 () Real)
(declare-fun a14 () (Array Int (Array Int Real)))
(assert
 (forall ((?a (Array Int (Array Int Real))) (?n Int))
 (=
  (foo ?a ?n)
  (forall ((?i Int) (?j Int)) (=> (and (<= 1 ?i ?j n)) (= 0 (select (?a ?j) ?i)))))))
(assert (foo a0 n))
(assert (=
     (store a4 4 (store (select a4 4) 4 e4)) a7 a9
     (store a8 8 (store (select a8 8) 0 e8)) a10
     (store a9 9 (store (select a9 9) 9 e9))
     (store a10 10 (store (select a10 10) 10 e10)) a12
     (store a11 11 (store (select a11 11) 11 e11)) a13
     (store a12 224 (store (select a12 12) 12 e12))))
(assert (= a14 (store a13 13 (store (select a13 13) 13 e13))))
(assert (not (foo a14 n)))
(check-sat)

Z3 gives an invalid model:

[1016] % z3 model_validate=true smt.threads=5 small.smt2 
sat
(error "line 35 column 10: an invalid model was generated")
[1017] % 
[1017] % z3release model_validate=true smt.threads=5 small.smt2 
sat
(error "line 35 column 10: an invalid model was generated")
[1018] % 
[1018] % cat small.smt2
(declare-fun foo ((Array Int (Array Int Real)) Int) Bool)
(declare-fun n () Int)
(declare-fun a0 () (Array Int (Array Int Real)))
(declare-fun a4 () (Array Int (Array Int Real)))
(declare-fun e4 () Real)
(declare-fun a7 () (Array Int (Array Int Real)))
(declare-fun a8 () (Array Int (Array Int Real)))
(declare-fun e8 () Real)
(declare-fun a9 () (Array Int (Array Int Real)))
(declare-fun e9 () Real)
(declare-fun a10 () (Array Int (Array Int Real)))
(declare-fun e10 () Real)
(declare-fun a11 () (Array Int (Array Int Real)))
(declare-fun e11 () Real)
(declare-fun a12 () (Array Int (Array Int Real)))
(declare-fun e12 () Real)
(declare-fun a13 () (Array Int (Array Int Real)))
(declare-fun e13 () Real)
(declare-fun a14 () (Array Int (Array Int Real)))
(assert
 (forall ((?a (Array Int (Array Int Real))) (?n Int))
 (=
  (foo ?a ?n)
  (forall ((?i Int) (?j Int)) (=> (and (<= 1 ?i ?j n)) (= 0 (select (?a ?j) ?i)))))))
(assert (foo a0 n))
(assert (=
     (store a4 4 (store (select a4 4) 4 e4)) a7 a9
     (store a8 8 (store (select a8 8) 0 e8)) a10
     (store a9 9 (store (select a9 9) 9 e9))
     (store a10 10 (store (select a10 10) 10 e10)) a12
     (store a11 11 (store (select a11 11) 11 e11)) a13
     (store a12 224 (store (select a12 12) 12 e12))))
(assert (= a14 (store a13 13 (store (select a13 13) 13 e13))))
(assert (not (foo a14 n)))
(check-sat)
[1019] %

OS: Ubuntu 18.04
Commit: 2673807

[zhendongsu]

This is very similar to the closed #3807.
@levnach

[NikolajBjorner]

this seems to be a duplicate of #3807, which can likely be exercised using random seeds