(set-option :produce-models true)
  (set-logic QF_UFLIA)
  (declare-fun f (Int) Bool)
  (define-fun nf ((i Int)) Bool (not (f i)))
  (assert (f 0))
  (check-sat)
  (get-value ((f 0) (nf 0) (f 0) (not (f 0))))