Failed to validate new core model

[jad-hamza]

Hello, here's an issue I got with the new core on 4.8.12 and master (9c7d9f0)

(set-option :produce-unsat-assumptions true)
(declare-datatypes () ((K (mkK (x Int)))))
(declare-datatypes () ((T (mkT (y Int)))))
(declare-datatypes () ((TP (mkTP (fst K) (snd T)))))
(declare-datatypes () ((CustomArray (mkCustomArray (aa (Array (_ BitVec 32) TP)) (sz (_ BitVec 32))))))
(declare-datatypes () ((Order (mkOrder (leq Int)))))
(declare-fun ar () CustomArray)
(declare-fun i () (_ BitVec 32))
(declare-fun order () Order)
(declare-fun j () (_ BitVec 32))
(declare-fun k () (_ BitVec 32))
(declare-fun l () (_ BitVec 32))
(declare-fun f (CustomArray Order (_ BitVec 32) (_ BitVec 32)) Bool)
(declare-fun rr () Bool)
(declare-fun e2 () Bool)
(declare-fun e3 () Bool)
(declare-fun r6 () Bool)
(declare-fun r7 () Bool)
(declare-fun r8 () Bool)
(declare-fun ll (Int K K) Bool)
(assert (bvsle #b00000000000000000000000000000000 k))
(assert (bvslt k (sz ar)))
(assert (bvsle #b00000000000000000000000000000000 l))
(assert (bvslt l (sz ar)))
(assert (bvslt k i))
(assert (bvslt l i))
(assert (bvslt i (bvsub (sz ar) #b00000000000000000000000000000001)))
(assert (bvslt i j))
(assert (f ar order i j))
(assert (= r7 (or (bvsgt #b00000000000000000000000000000000 i) (bvsge i (bvsub (sz (mkCustomArray (store (store (aa ar) k (select (aa ar) l)) l (select (aa ar) k)) (sz ar))) #b00000000000000000000000000000001)) (bvsge i j))))
(assert (=> (not r7) (= r8 (ll (leq order) (fst (select (aa (mkCustomArray (store (store (aa ar) k (select (aa ar) l)) l (select (aa ar) k)) (sz ar))) i)) (fst (select (aa (mkCustomArray (store (store (aa ar) k (select (aa ar) l)) l (select (aa ar) k)) (sz ar))) (bvadd i #b00000000000000000000000000000001)))))))
(assert (= (f ar order i j) e2))
(assert (=> rr (= e2 e3)))
(assert (=> rr (=> (not r6) (not e3))))
(assert (=> rr (= r6 (ll (leq order) (fst (select (aa ar) i)) (fst (select (aa ar) (bvadd i #b00000000000000000000000000000001)))))))
(check-sat)
(get-model)

z3-master tactic.default_tactic=smt sat.euf=true file.smt2 

Failed to validate 1588 84: (ll (leq order) (fst (select #78 i)) (fst (select #78 #81))) false
77: (leq order)
0
80: (fst (select (aa #64) i))
(mkK 0)
83: (fst (select (aa #64) (bvadd i bv[1:32])))
(mkK (- 7720))
sat
(
  (define-fun r7 () Bool
    false)
  (define-fun r8 () Bool
    true)
  (define-fun rr () Bool
    false)
  (define-fun l () (_ BitVec 32)
    #x292490bb)
  (define-fun k () (_ BitVec 32)
    #x1004888f)
  (define-fun j () (_ BitVec 32)
    #x6a5b7eee)
  (define-fun r6 () Bool
    true)
  (define-fun e2 () Bool
    true)
  (define-fun ar () CustomArray
    (let ((a!1 (store ((as const (Array (_ BitVec 32) TP)) (mkTP (mkK 0) (mkT 0)))
                  #x4d000000
                  (mkTP (mkK (- 7720)) (mkT 0)))))
  (mkCustomArray a!1 #x54d48823)))
  (define-fun e3 () Bool
    false)
  (define-fun order () Order
    (mkOrder 0))
  (define-fun i () (_ BitVec 32)
    #x4cffffff)
  (define-fun f ((x!1 CustomArray)
   (x!2 Order)
   (x!3 (_ BitVec 32))
   (x!4 (_ BitVec 32))) Bool
    (ite (and (= x!1 (mkCustomArray (_ as-array k!1) #x54d48823))
              (= x!2 (mkOrder 0))
              (= x!3 #x4cffffff)
              (= x!4 #x6a5b7eee))
      true
      #unspecified))
  (define-fun k!1 ((x!0 (_ BitVec 32))) TP
    (ite (= x!0 #x4d000000) (mkTP (mkK (- 7720)) (mkT 0))
      (mkTP (mkK 0) (mkT 0))))
  (define-fun ll ((x!1 Int) (x!2 K) (x!3 K)) Bool
    (ite (and (= x!1 0) (= x!2 (mkK 0)) (= x!3 (mkK (- 7720)))) false
    (ite (and (= x!1 0) (= x!2 (mkK 0)) (= x!3 (mkK 0))) true
      #unspecified)))
)

[NikolajBjorner]

most likely fixed as a result of dealing with #5512.
Currently does not complain.

[jad-hamza]

Great, thanks!