test/regress/regress0/nl/nta/shifting2.smt2

   1 ; COMMAND-LINE: --nl-ext
   2 ; EXPECT: unsat
   3 (set-logic QF_NIRA)
   4 (set-info :status unsat)
   5 (declare-fun pi () Real)
   6
   7 (assert (and (< 3.0 pi) (< pi 3.5)))
   8
   9 (declare-fun y () Real)
  10 (assert (and (< (- pi) y) (< y pi)))
  11
  12 (declare-fun s () Int)
  13
  14 (declare-fun z () Real)
  15
  16 (assert (= z (+ y (* 2 pi s))))
  17
  18 (assert (and (< (- pi) z) (< z pi)))
  19
  20 (assert (not (= z y)))
  21
  22 (check-sat)