[507] % z3-4.8.10 model_validate=true small.smt2
sat
[508] % z3release model_validate=true small.smt2
sat
(error "line 37 column 10: an invalid model was generated")
[509] % 
[509] % cat small.smt2
(set-option :rewriter.expand_nested_stores true)
(set-option :rewriter.expand_store_eq true)
(set-option :smt.threads 2)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun c () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun d () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun o () (_ BitVec 1))
(declare-fun e () (_ BitVec 1))
(declare-fun f () (_ BitVec 1))
(declare-fun q () (_ BitVec 1))
(declare-fun g () (_ BitVec 1))
(declare-fun h () (_ BitVec 1))
(declare-fun i () (_ BitVec 1))
(declare-fun p () (_ BitVec 32))
(declare-fun j () (_ BitVec 32))
(declare-fun k () (_ BitVec 32))
(declare-fun l () (_ BitVec 32))
(declare-fun m () (_ BitVec 32))
(declare-fun n () (_ BitVec 32))
(assert (= (_ bv1 1) (bvshl (bvand (bvand (bvand (bvand (bvand (bvand
  (bvand (ite (= o (ite (= d (store (store (store (store c p ((_
  extract 7 0) (bvlshr l (_ bv24 32)))) (bvshl p (_ bv2 32)) ((_
  extract 7 0) (bvlshr l (_ bv16 32)))) (bvadd (_ bv1 32)) ((_ extract
  7 0) (bvlshr l (_ bv8 32)))) p ((_ extract 7 0) l))) (_ bv1 1) (_
  bv0 1))) (_ bv1 1) (_ bv0 1))) (ite (= e (ite (= p (bvsub j (_ bv4
  32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))) (ite (= f (ite (=
  c (store (store (store (store b j ((_ extract 7 0) (bvlshr m (_ bv24
  32)))) (bvadd (_ bv2 32)) ((_ extract 7 0) (bvlshr m (_ bv16 32))))
  (bvadd (_ bv1 32)) ((_ extract 7 0) (bvlshr m (_ bv8 32)))) j ((_
  extract 7 0) m))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))) (ite
  (= q g) (_ bv1 1) (_ bv0 1))) (ite (= g i) (_ bv1 1) (_ bv0 1)))
  (ite (= h (ite (= b (store (store (store (store a k ((_ extract 7 0)
  (bvlshr n (_ bv24 32)))) k ((_ extract 7 0) (bvlshr n (_ bv16 32))))
  (bvadd k (_ bv1 32)) ((_ extract 7 0) (bvlshr n (_ bv8 32)))) k ((_
  extract 7 0) n))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)))))
(check-sat)
[510] %