path: root/test/regress/regress1/nl/nl_uf_lalt.smt2

; COMMAND-LINE: --decision=justification
(set-logic QF_UFNIA)
(set-info :status unsat)
(declare-fun c (Int) Int)
(declare-fun a (Int) Int)
(declare-fun b (Int) Int)
(assert (> (a 0) 0))
(assert (= (c 0) (* (a 0) (b 0))))
(assert (not (= (b 0) (div (c 0) (a 0)))))
(check-sat)