[630] % z3 small.smt2
unsat
sat
[631] % cat small.smt2
(set-option :fp.xform.scale true)
(set-option :fp.xform.bit_blast true)
(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Int)
(declare-fun d () Bool)
(declare-fun e () Bool)
(declare-fun f () Bool)
(assert (= (not (= a (not (= b f)))) d (not (= c 0)) a (= d e) b (not (= f e))))
(check-sat)
(check-sat-using (then add-bounds qfnra horn-simplify))
[632] %