[555] % z3release model_validate=true small.smt2 
sat
[556] % z3release rewriter.flat=false model_validate=true small.smt2 
sat
(error "line 168 column 10: an invalid model was generated")
[557] % 
[557] % cat small.smt2 
(declare-fun e () Bool)
(declare-fun a_LSBRCK_0_RSBRCK_ () Int)
(declare-fun f () Bool)
(declare-fun a_LSBRCK_1_RSBRCK_ () Int)
(declare-fun g () Bool)
(declare-fun cj () Int)
(declare-fun h () Bool)
(declare-fun a_LSBRCK_3_RSBRCK_ () Int)
(declare-fun i () Bool)
(declare-fun a_LSBRCK_4_RSBRCK_ () Int)
(declare-fun a () Int)
(declare-fun j () Bool)
(declare-fun b_LSBRCK_0_RSBRCK_ () Int)
(declare-fun k () Bool)
(declare-fun b_LSBRCK_1_RSBRCK_ () Int)
(declare-fun l () Bool)
(declare-fun bz () Int)
(declare-fun m () Bool)
(declare-fun b_LSBRCK_3_RSBRCK_ () Int)
(declare-fun n () Bool)
(declare-fun cf () Int)
(declare-fun b () Int)
(declare-fun o () Bool)
(declare-fun p () Bool)
(declare-fun q () Bool)
(declare-fun r () Bool)
(declare-fun s () Bool)
(declare-fun t () Bool)
(declare-fun u () Bool)
(declare-fun v () Bool)
(declare-fun w () Bool)
(declare-fun x () Bool)
(declare-fun y () Bool)
(declare-fun z () Bool)
(declare-fun aa () Bool)
(declare-fun ab () Bool)
(declare-fun ac () Bool)
(declare-fun ad () Bool)
(declare-fun ae () Bool)
(declare-fun af () Bool)
(declare-fun ag () Bool)
(declare-fun ah () Bool)
(declare-fun c_LSBRCK_0_RSBRCK_ () Int)
(declare-fun ai () Bool)
(declare-fun c_LSBRCK_1_RSBRCK_ () Int)
(declare-fun aj () Bool)
(declare-fun c_LSBRCK_2_RSBRCK_ () Int)
(declare-fun ak () Bool)
(declare-fun cg () Int)
(declare-fun al () Bool)
(declare-fun ch () Int)
(declare-fun am () Bool)
(declare-fun an () Int)
(declare-fun c () Int)
(declare-fun ao () Bool)
(declare-fun ap () Int)
(declare-fun aq () Bool)
(declare-fun d () Int)
(assert (and (>= a 0) (<= a 31) (= (- (- (- (- (- a
   a_LSBRCK_0_RSBRCK_) (* 2 a_LSBRCK_1_RSBRCK_)) (* 4 cj)) (* 8
   a_LSBRCK_3_RSBRCK_)) (* 16 a_LSBRCK_4_RSBRCK_)) 0) (>=
   a_LSBRCK_0_RSBRCK_ 0) (<= a_LSBRCK_0_RSBRCK_ 1) (or (not e) (=
   a_LSBRCK_0_RSBRCK_ 1)) (or e (= a_LSBRCK_0_RSBRCK_ 0)) (>=
   a_LSBRCK_1_RSBRCK_ 0) (<= a_LSBRCK_1_RSBRCK_ 1) (or (not f) (=
   a_LSBRCK_1_RSBRCK_ 1)) (or f (= a_LSBRCK_1_RSBRCK_ 0)) (>= cj 0)
   (<= cj 1) (or (not g) (= cj 1)) (or g (= cj 0)) (>=
   a_LSBRCK_3_RSBRCK_ 0) (<= a_LSBRCK_3_RSBRCK_ 1) (or (not h) (=
   a_LSBRCK_3_RSBRCK_ 1)) (or h (= a_LSBRCK_3_RSBRCK_ 0)) (>=
   a_LSBRCK_4_RSBRCK_ 0) (<= a_LSBRCK_4_RSBRCK_ 1) (or (not i) (=
   a_LSBRCK_4_RSBRCK_ (* 4 cj))) (or i (= a_LSBRCK_4_RSBRCK_ 0)) (>= b
   0) (<= b 31) (= (- (- (- (- (- b b_LSBRCK_0_RSBRCK_) 0) (* 4 bz))
   8) (* 6 cf)) 0) (>= b_LSBRCK_0_RSBRCK_ 0) (<= b_LSBRCK_0_RSBRCK_ 1)
   (or (not j) (= b_LSBRCK_0_RSBRCK_ 1)) (or j (= b_LSBRCK_0_RSBRCK_
   0)) (>= (* b_LSBRCK_0_RSBRCK_ ch) 0) (<= b_LSBRCK_1_RSBRCK_ 1) (or
   (ite (or (not ah) q) (and (and (and (and (and (and (and (and (and
   (and (and (and (and (and (and (and (and (and (and (and (and (and
   (and (and (and (and (and (and (and (and (and (and (and (and (and
   (and (and (and (and (and (and (and (and (and (and (and (and (and
   (and (and (and (and (and (and (and (and (and (and (and (and (and
   (and (and (and (and (and (and (and (and (and (and (and (and (and
   (and (and (and (and (and (and (and (= (- (- (- (- (- a
   a_LSBRCK_0_RSBRCK_) a_LSBRCK_1_RSBRCK_)) (* 8 a_LSBRCK_3_RSBRCK_)))
   0) (>= a_LSBRCK_0_RSBRCK_ 0)) (<= a_LSBRCK_0_RSBRCK_ 1)) (or (not
   e) (= a_LSBRCK_0_RSBRCK_ 1))) (or e (= a_LSBRCK_0_RSBRCK_ 0))) (>=
   a_LSBRCK_1_RSBRCK_ 0)) (<= a_LSBRCK_1_RSBRCK_ 1)) (or (not f) (=
   a_LSBRCK_1_RSBRCK_ 1))) (or f (= a_LSBRCK_1_RSBRCK_ 0))) (>= cj 0))
   (<= cj 1)) (or (not g) (= cj 1))) (or g (= cj 0))) (>=
   a_LSBRCK_3_RSBRCK_ 0)) (<= a_LSBRCK_3_RSBRCK_ 1)) (or (not h) (=
   a_LSBRCK_3_RSBRCK_ 1))) (or h (= a_LSBRCK_3_RSBRCK_ 0))) (>=
   a_LSBRCK_4_RSBRCK_ 0)) (<= a_LSBRCK_4_RSBRCK_ 1)) (or (not i) (=
   a_LSBRCK_4_RSBRCK_ 1))) (or i (= a_LSBRCK_4_RSBRCK_ 0))) (>= b 0))
   (<= b 31)) (= (- (- (- (- (- b b_LSBRCK_0_RSBRCK_))) (* 8
   b_LSBRCK_3_RSBRCK_)) (* 6 cf)) 0)) (>= b_LSBRCK_0_RSBRCK_ 0)) (<=
   b_LSBRCK_0_RSBRCK_ 1)) (or (not j) (= b_LSBRCK_0_RSBRCK_ 1))) (or j
   (= b_LSBRCK_0_RSBRCK_ 0))) (>= b_LSBRCK_1_RSBRCK_ 0)) (<=
   b_LSBRCK_1_RSBRCK_ 1)) (or (= b_LSBRCK_1_RSBRCK_ 1))) k) (>= bz 0))
   (<= bz 1)) (or (not l) (= bz 1))) (or (= bz 0))) (>=
   b_LSBRCK_3_RSBRCK_ 0)) (<= b_LSBRCK_3_RSBRCK_ 1)) (or (=
   b_LSBRCK_3_RSBRCK_ 1))) m) (>= cf 0)) (<= cf 1)) (= cf 0)) (>= c
   0)) (<= c 31)) (= (- (- (- (- (- c c_LSBRCK_0_RSBRCK_) (* 2
   c_LSBRCK_1_RSBRCK_)) (* 4 c_LSBRCK_2_RSBRCK_))) (* 16 ch)) 0)) (>=
   c_LSBRCK_0_RSBRCK_ 0)) (<= c_LSBRCK_0_RSBRCK_ 1)) (or (not ah) (=
   c_LSBRCK_0_RSBRCK_ 1))) (or ah (= c_LSBRCK_0_RSBRCK_ 0))) (>=
   c_LSBRCK_1_RSBRCK_ 0)) (<= c_LSBRCK_1_RSBRCK_ 1)) (not ai)) (or ai
   (= c_LSBRCK_1_RSBRCK_ 0))) (>= c_LSBRCK_2_RSBRCK_ 0)) (<=
   c_LSBRCK_2_RSBRCK_ 1)) (or (not aj) (= c_LSBRCK_2_RSBRCK_ 1))) (or
   aj (= c_LSBRCK_2_RSBRCK_ 0))) (>= cg 0)) (<= cg 1)) (or (not ak) (=
   cg 1))) ak) (>= ch 0)) (<= ch 1)) (or (not al) (= ch 1))) al) (or
   (or (not q) e) j)) (or (or (not q) (not e)) (not j))) (or (or q
   (not e)) j)) (or (or q e) (not j))) (or (or o (not e)) (not j)))
   (or (not o) e)) (or (not o) j)) (or (not ah) q)) (not am)) (or ah
   (not q))) (not am)) (not am)) (not p)) (not p)) (or (or (not ad) p)
   o)) (not p)) (and (and (and (and (and (and (and (and (and (and (and
   (and (and (and (and (and (and (and (and (and (and (and (and (and
   (and (and (and (and (and (and (and (and (and (and (and (and (and
   (and (and (and (and (and (and (and (and (and (and (and (and (and
   (and (and (and (and (and (and (and (and (and (and (and (and (and
   (and (and (and (and (and (and (and (and (or (or ai (= 0 (- (-
   c_LSBRCK_1_RSBRCK_ c_LSBRCK_2_RSBRCK_)) cj)) ad) (not ad)) (not
   ad)) (not s)) (not s)) r) (not r)) r) (not r)) l) (not l)) l) (not
   l)) (not l)) (not u)) (not u)) e) (not ae)) e) (not ae)) (not ae))
   (not v)) (not v)) u) (not u)) u) (not u)) m) (not m)) m) (not m))
   (not m)) (not x)) (not x)) f) (not af)) f) (not af)) (not af)) (not
   y)) (not y)) x) (not x)) x) (not x)) n) (not n)) n) (not n)) (not
   n)) (not aa)) (not aa)) ag) (not ag)) ag) (not ag)) (not ag)) ab)
   ab) aa) (not aa)) aa) (not aa)) (= d 0)) (= d 1)) (= an 0)) (= an
   1)) (= ap 0)) (<= ap 1)) (not am)) am) (>= (+ (+ a b) an) 32))) (=
   b_LSBRCK_1_RSBRCK_ 0)) (>= bz 0) (or (not l) (= bz 1)) (or l (= bz
   0)) (<= b_LSBRCK_3_RSBRCK_ 1) (or (not m) (= b_LSBRCK_3_RSBRCK_ 1))
   m (= cf 0) (distinct (- (- a a_LSBRCK_0_RSBRCK_) (* 2
   a_LSBRCK_1_RSBRCK_)) b_LSBRCK_1_RSBRCK_) (<= c 31) (= (- (- (- (-
   (- c c_LSBRCK_0_RSBRCK_) (* 2 c_LSBRCK_1_RSBRCK_)) (* 4
   c_LSBRCK_2_RSBRCK_)) (* 8 cg)) 16) 0) (>= c_LSBRCK_0_RSBRCK_ 0) (<=
   c_LSBRCK_0_RSBRCK_ 1) (or (not ah) (= c_LSBRCK_0_RSBRCK_ 1)) (or ah
   (= c_LSBRCK_0_RSBRCK_ 0)) (>= c_LSBRCK_1_RSBRCK_ 0) (<=
   c_LSBRCK_1_RSBRCK_ 1) (or (not ai) (= c_LSBRCK_1_RSBRCK_ 1)) (or ai
   (= c_LSBRCK_1_RSBRCK_ 0)) (>= c_LSBRCK_2_RSBRCK_ 0) (<=
   c_LSBRCK_2_RSBRCK_ 1) (or (not aj) (= c_LSBRCK_2_RSBRCK_ 1)) (or aj
   (= c_LSBRCK_2_RSBRCK_ 0)) (>= cg 0) (<= cg 1) (or (not ak) (= cg
   1)) ak (>= ch 0) (<= ch 1) (or (not al) (= ch 1)) al (or (or (not
   q) e) j) (or (or (not q) (not e)) (not j)) (or (or q (not e)) j)
   (or (or q e) (not j)) (or (or o (not e)) (not j)) (or (not o) e)
   (or (not o) j) (or (not ah) q) (or ah (not q)) (or (not p) am) (or
   (or (not ad) p) o) (or f k) (or (or (not t) (not f)) (not k)) (or
   (or t (not f)) k) (or (or t f) (not k)) (or (or r (not f)) (not k))
   (or (not r) f) (or (or (not ai) t) ad) (or (or (not ai) (not t))
   (not ad)) (or (or ai (not t)) ad) (or (or ai t) (not ad)) (or s
   (not t)) (or (not s) t) (or (or (not ae) s) r) (or (or (not ae)
   (not s)) (not r)) (or (or ae (not s)) r) (or (or ae s) (not r)) (or
   (or (not w) g) l) (or (or (not w) (not g)) (not l)) (or (or w (not
   g)) l) (or (or w g) (or u (not g)) (not l)) (or (not u) l) (or (or
   (not aj) w) ae) (or (or (not aj) (not w)) (not ae)) (or (or aj (not
   w)) ae) (or (or aj w) (not ae)) (or (or v (not w)) (not ae)) (or
   (not v) w) (or (not v) ae) (or (or (not af) v) u) (or (or (not af)
   (not v)) (not u)) (or (or (> (- b b_LSBRCK_0_RSBRCK_) 0 (- (- (- (-
   a a_LSBRCK_0_RSBRCK_) (* 2 a_LSBRCK_1_RSBRCK_)) (* 4 cj)) (* 8
   a_LSBRCK_3_RSBRCK_))) (not v)) u) (or (or af v) (not u)) (or (not
   z) (not h)) (or (or x (not h)) (not m)) (or (not ak) z af) (or (not
   ak) (or y (not z)) (not af)) (or (not y) z) (or (not y) af) (or (or
   (not ag) y) x) (or (or (not ag) (not y)) (or ag (not y)) x) (or (or
   ag y) (not x)) (or (not ac) i) (not n) (or ac (not i)) (or (not al)
   ac ag) (or (not al) (not ac) (not ag)) (or (or ab (not ac)) (not
   ag)) aq (not aa) (>= d 0) (<= d 31) (>= ap 0) (<= ap 1) (or am (=
   an 0)) (or (not ao) (>= (+ (+ a b) an) 32)) (or ao (not (>= (+ (+ a
   b) an) 32))) (or ao (= (- (- (- d a) b) an) 0)) (or (not (= (- (-
   (- d a) b) an) (- 32))) (not (= (- (- (- d a) b) an) 0))) (not am)
   (not (= d c))))
(check-sat)
[558] %