test/regress/regress0/nl/nta/tan-rewrite2.smt2

   1 ; COMMAND-LINE: --nl-ext
   2 ; EXPECT: unsat
   3 (set-logic QF_UFNRA)
   4 (set-info :status unsat)
   5 (declare-fun x () Real)
   6
   7
   8 (assert (= (tan x) (sin x)))
   9 (assert (> (cos x) 0))
  10 (assert (not (= (cos x) 1)))
  11 (assert (not (= (sin x) 0)))
  12
  13 (check-sat)