[543] % z3release model_validate=true small.smt2
sat
(
 (define-fun p () (_ FloatingPoint 8 24)
  (_ +zero 8 24))
 (define-fun bb () (_ FloatingPoint 8 24)
  (_ -zero 8 24))
 (define-fun d () (_ FloatingPoint 8 24)
  (fp #b0 #x74 #b00000010010000010001010))
 (define-fun n () (_ FloatingPoint 8 24)
  (_ -zero 8 24))
 (define-fun k () (_ FloatingPoint 8 24)
  (fp #b0 #x00 #b00000010000000000000000))
 (define-fun h () (_ FloatingPoint 8 24)
  (fp #b0 #x00 #b11111111111111111111111))
 (define-fun j () (_ FloatingPoint 8 24)
  (_ -zero 8 24))
 (define-fun o () (_ FloatingPoint 8 24)
  (_ +zero 8 24))
 (define-fun i () (_ FloatingPoint 8 24)
  (fp #b0 #x14 #b01000100001001010110000))
 (define-fun f () (_ FloatingPoint 8 24)
  (fp #b0 #x74 #b00000010010000010001010))
 (define-fun g () (_ FloatingPoint 8 24)
  (_ +zero 8 24))
 (define-fun q () (_ FloatingPoint 8 24)
  (_ +zero 8 24))
 (define-fun l () (_ FloatingPoint 8 24)
  (fp #b1 #x7f #b00000000000000000000000))
 (define-fun aa () (_ FloatingPoint 8 24)
  (fp #b0 #x00 #b11111111111111111111111))
 (define-fun cc () (_ FloatingPoint 8 24)
  (_ +zero 8 24))
 (define-fun c () RoundingMode
  roundNearestTiesToAway)
 (define-fun b () RoundingMode
  roundNearestTiesToEven)
 (define-fun a () RoundingMode
  roundNearestTiesToEven)
 (define-fun e () RoundingMode
  roundTowardPositive)
)
[544] % z3-4.8.8 rewriter.flat=false model_validate=true small.smt2
sat
(model 
 (define-fun p () (_ FloatingPoint 8 24)
  (fp #b1 #x7f #b01100110011000000100000))
 (define-fun bb () (_ FloatingPoint 8 24)
  (fp #b0 #x6f #b00000000000000000000000))
 (define-fun d () (_ FloatingPoint 8 24)
  (fp #b1 #x7f #b01010110001010000110100))
 (define-fun n () (_ FloatingPoint 8 24)
  (fp #b0 #x7f #b01010110001010010110100))
 (define-fun k () (_ FloatingPoint 8 24)
  (_ NaN 8 24))
 (define-fun h () (_ FloatingPoint 8 24)
  (_ -zero 8 24))
 (define-fun j () (_ FloatingPoint 8 24)
  (fp #b0 #x6f #b00000000000000000000000))
 (define-fun o () (_ FloatingPoint 8 24)
  (_ +zero 8 24))
 (define-fun i () (_ FloatingPoint 8 24)
  (fp #b1 #x18 #b01010110001010000100000))
 (define-fun f () (_ FloatingPoint 8 24)
  (fp #b1 #x7f #b01010110001010000110100))
 (define-fun g () (_ FloatingPoint 8 24)
  (_ +zero 8 24))
 (define-fun q () (_ FloatingPoint 8 24)
  (fp #b1 #x7f #b01100110011000000100000))
 (define-fun l () (_ FloatingPoint 8 24)
  (_ NaN 8 24))
 (define-fun aa () (_ FloatingPoint 8 24)
  (_ -zero 8 24))
 (define-fun cc () (_ FloatingPoint 8 24)
  (_ -oo 8 24))
 (define-fun c () RoundingMode
  roundTowardZero)
 (define-fun b () RoundingMode
  roundNearestTiesToEven)
 (define-fun a () RoundingMode
  roundNearestTiesToEven)
 (define-fun e () RoundingMode
  roundTowardZero)
)
[545] % z3release rewriter.flat=false model_validate=true small.smt2
sat
(error "line 34 column 10: an invalid model was generated")
(
 (define-fun p () (_ FloatingPoint 8 24)
  (fp #b1 #x24 #b00000000000000000000000))
 (define-fun bb () (_ FloatingPoint 8 24)
  (fp #b0 #xd7 #b00100000010000010110100))
 (define-fun d () (_ FloatingPoint 8 24)
  (fp #b1 #x7f #b01100110011001100110100))
 (define-fun n () (_ FloatingPoint 8 24)
  (fp #b0 #x24 #b00000000000000000110100))
 (define-fun k () (_ FloatingPoint 8 24)
  (_ NaN 8 24))
 (define-fun h () (_ FloatingPoint 8 24)
  (_ +zero 8 24))
 (define-fun j () (_ FloatingPoint 8 24)
  (fp #b0 #xd7 #b00100000010000010110100))
 (define-fun o () (_ FloatingPoint 8 24)
  (_ +zero 8 24))
 (define-fun i () (_ FloatingPoint 8 24)
  (fp #b1 #x7f #b11100110011001100110111))
 (define-fun f () (_ FloatingPoint 8 24)
  (fp #b1 #x7f #b01100110011001100110100))
 (define-fun g () (_ FloatingPoint 8 24)
  (_ +zero 8 24))
 (define-fun q () (_ FloatingPoint 8 24)
  (fp #b1 #x24 #b00000000000000000000000))
 (define-fun l () (_ FloatingPoint 8 24)
  (fp #b0 #x80 #b00000000000000000000000))
 (define-fun aa () (_ FloatingPoint 8 24)
  (_ +zero 8 24))
 (define-fun cc () (_ FloatingPoint 8 24)
  (_ -oo 8 24))
 (define-fun c () RoundingMode
  roundNearestTiesToAway)
 (define-fun b () RoundingMode
  roundNearestTiesToEven)
 (define-fun a () RoundingMode
  roundNearestTiesToEven)
 (define-fun e () RoundingMode
  roundTowardZero)
)
[546] % 
[546] % cat small.smt2
(declare-fun a () RoundingMode)
(declare-fun b () RoundingMode)
(declare-fun c () RoundingMode)
(declare-fun e () RoundingMode)
(declare-fun d () (_ FloatingPoint 8 24))
(declare-fun f () (_ FloatingPoint 8 24))
(declare-fun o () (_ FloatingPoint 8 24))
(declare-fun g () (_ FloatingPoint 8 24))
(declare-fun h () (_ FloatingPoint 8 24))
(declare-fun aa () (_ FloatingPoint 8 24))
(declare-fun i () (_ FloatingPoint 8 24))
(declare-fun j () (_ FloatingPoint 8 24))
(declare-fun bb () (_ FloatingPoint 8 24))
(declare-fun n () (_ FloatingPoint 8 24))
(declare-fun p () (_ FloatingPoint 8 24))
(declare-fun q () (_ FloatingPoint 8 24))
(declare-fun k () (_ FloatingPoint 8 24))
(declare-fun cc () (_ FloatingPoint 8 24))
(declare-fun l () (_ FloatingPoint 8 24))
(assert (distinct c b))
(assert (distinct c a))
(assert (distinct e roundNearestTiesToEven))
(assert (not (= (ite (let ((m ((_ to_fp 8 24) e (/ 7.0 5.0)))) (and (fp.lt f m) (fp.geq f (fp.neg m)))) (_ bv1 32) (_ bv0 32)) (_ bv0 32))))
(assert (= f d f))
(assert (= g o))
(assert (= aa h))
(assert (distinct i f))
(assert (= bb j))
(assert (distinct n (fp.sub e f (fp.add e aa bb))))
(assert (distinct p n))
(assert (= q p))
(assert (distinct cc k))
(assert (not (fp.eq ((_ to_fp 11 53) e l) ((_ to_fp 11 53) e (/ 1.0 10.0)))))
(check-sat)
(get-model)
[547] %