Incorrect model when quantifying over polymorphic type #7102
Description
Running the following smt2 file
(declare-type-var T)
(declare-fun f (T) Bool)
(declare-var b Bool)
(assert (forall ((x T)) (f x)))
(assert (= b (f 0)))
(check-sat)
(get-model)
(assert (not b))
(check-sat)produces the output:
sat
(
;; universe for T:
;; T!val!0
;; -----------
;; definitions for universe elements:
(declare-fun T!val!0 () T)
;; cardinality constraint:
(forall ((x T)) (= x T!val!0))
;; -----------
(define-fun b () Bool
false)
(define-fun f ((x!0 T)) Bool
true)
(define-fun f ((x!0 Int)) Bool
false)
)
unsatIn particular the model produced for b is false even though after the first check-sat, b must be true. Interestingly after asserting (not b) (which agrees with the previous model) z3 correctly reports unsat.
z3 also gives the expected model when the quatifier is (forall ((x Int)) (f x)) instead of (forall ((x T)) (f x))
This is with Z3 version 4.12.5 - 64 bit