(smt.arith.solver=2/6, rewriter.flat=false) invalid model on QF_NIA formula #5328
Description
Commit: 7c86134
OS: Ubuntu 18.04
Note: (1) regression from z3-4.8.8 (also affects z3-4.8.10); (2)smt.arith.solver=2 or smt.arith.solver=6 is needed to reproduce the issue
[619] % z3release smt.arith.solver=6 rewriter.flat=false model_validate=true small.smt2
sat
(error "line 11 column 10: an invalid model was generated")
(
(define-fun aa () Int
1)
(define-fun a () Int
(- 637))
(define-fun c () Int
1)
(define-fun b () Int
1)
)
[620] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun aa () Int)
(assert (= (> (- (- (ite (< (- (+ b a)) 632) (- (* 6 b)) 0) aa)) 6) (>= c 1)))
(assert (<= c aa 2))
(assert (<= 0 aa))
(assert (> 6 (* (- (- (ite (< (- (+ b a)) 632) (- b) 0))) a)))
(assert (< b 16))
(assert (>= b 0))
(check-sat)
(get-model)
[621] %