[586] % z3-4.8.7 small.smt2
sat
[587] % z3 small.smt2
sat
(error "line 6 column 46: an invalid model was generated")
[588] %
[588] % cat small.smt2
(set-option :fp.engine spacer)
(set-option :model_validate true)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (= a b))
(check-sat-using (then reduce-invertible horn))
[589] %