Obviously incorrect model

[nafur]

I minimized an input to this:

(set-option :print-success false)
(set-option :produce-models true)
(set-logic QF_UFNIA)
(declare-fun Y () Bool)
(declare-fun X () Bool)
(declare-fun Z () Bool)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun f (Int) Int)
(assert
    (= X
        (=>
            (> (f a) 0)
            (=>
                (= c (mod b 10))
                (=> Y Z)
            )
        )
    )
)
(assert (not X))
(check-sat)
(get-model)

On my machine:

$ yices-smt2 --version ; yices-smt2 foo_small.smt2 
Yices 2.6.4
Copyright SRI International.
Linked with GMP 6.2.1
Copyright Free Software Foundation, Inc.
Build date: 2021-10-22
Platform: x86_64-pc-linux-gnu (release)
Revision: unknown
sat
(= Y true)
(= X true)
(= Z false)
(= a 0)
(= b 5)
(= c 5)
(= f @fun_8)
(function @fun_8
 (type (Array Int Int))
 (default 0))

Note that the model sets (= X true) whereas I assert (assert (not X))...