Consolidate invalid model bugs

[wintered]

[601] % z3release model_validate=true small.smt2
sat
(error "line 5 column 29: an invalid model was generated")
(model 
 (define-fun b () Real
  0.0)
 (define-fun a () Real
  0.0)
 (define-fun c ((x!0 Real)) Real
  5.0)
)
[602] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c (Real) Real)
(assert (= (- a b) 1))
(check-sat (distinct 0 (c 2)))
(get-model)
[603] %

OS: Ubuntu 18.04
Commit: 44679d8

[wintered]

possibly related instance

[551] % z3release model_validate=true small.smt2
sat
(error "line 4 column 25: an invalid model was generated")
(model 
 (define-fun b () Bool
  true)
 (define-fun a () Int
  0)
)
[552] % 
[552] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Bool)
(assert (> a 1))
(check-sat (or b (= a 2)))
(get-model)
[553] %

OS: Ubuntu 18.04
Commit: 44679d8

[muchang]

invalid model from z3's arith.solver=2 (feeding the generated model to the formula leads to unsat)

[510] % z3release smt.arith.solver=6 model_validate=true small.smt2
sat
(error "line 13 column 10: an invalid model was generated")
(model
 (define-fun f () Int
  1)
 (define-fun c () Int
  2)
 (define-fun k () Int
  3)
 (define-fun i () Bool
  false)
 (define-fun n ((x!0 Int)) Bool
  true)
 (define-fun /0 ((x!0 Real) (x!1 Real)) Real
  0.0)
 (define-fun m ((x!0 Int) (x!1 Int) (x!2 Int)) Int
  0)
 (define-fun h ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
  (= 0 x!0))
 (define-fun g ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
  true)
 (define-fun j ((x!0 Int) (x!1 Int) (x!2 Int) (x!3 Int)) Bool
  (not (= 0 x!0)))
 (define-fun d ((x!0 Int) (x!1 Int) (x!2 Int)) Int
  0)
)
[511] % z3release smt.arith.solver=2 model_validate=true small.smt2
sat
(error "line 13 column 10: an invalid model was generated")
(model
 (define-fun f () Int
  (- 1))
 (define-fun c () Int
  1)
 (define-fun k () Int
  2)
 (define-fun i () Bool
  false)
 (define-fun n ((x!0 Int)) Bool
  true)
 (define-fun /0 ((x!0 Real) (x!1 Real)) Real
  0.0)
 (define-fun m ((x!0 Int) (x!1 Int) (x!2 Int)) Int
  0)
 (define-fun h ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
  (= 0 x!0))
 (define-fun g ((x!0 Int) (x!1 Int) (x!2 Int)) Bool
  true)
 (define-fun j ((x!0 Int) (x!1 Int) (x!2 Int) (x!3 Int)) Bool
  (not (= 0 x!0)))
 (define-fun d ((x!0 Int) (x!1 Int) (x!2 Int)) Int
  0)
)
[512] %
[512] % cat small.smt2
(define-fun m ((c Int) (a Int) (b Int)) Int 0)
(define-fun d ((c Int) (a Int) (b Int)) Int (m c (/ a b) 0))
(define-fun j ((c Int) (e Int) (f Int) (k Int)) Bool (distinct (d c e f) k))
(define-fun g ((c Int) (f Int) (k Int)) Bool true)
(declare-fun n (Int) Bool)
(declare-fun c () Int)
(declare-fun f () Int)
(declare-fun k () Int)
(define-fun h ((c Int) (f Int) (k Int)) Bool (xor (g c f k) (j c 0 f k)))
(define-fun i () Bool (h c f k ))
(assert i)
(assert (n k))
(check-sat)
(get-model)
[513] %

Commit: 2f756da