test/regress/regress1/nl/sin1-sat.smt2

   1 ; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models
   2 ; EXPECT: sat
   3 (set-logic QF_NRAT)
   4 (set-info :status sat)
   5 (declare-fun x () Real)
   6
   7 (assert (> (sin 1) 0.84))
   8 (assert (< (sin 1) 0.85))
   9 (assert (< (- x (sin 1)) 0.000001))
  10 (assert (< (- (sin 1) x) 0.000001))
  11
  12 (check-sat)