test/regress/regress0/nl/pow2-native-3.smt2

   1 ; EXPECT: unsat
   2 (set-logic QF_NIA)
   3 (set-info :status unsat)
   4 (declare-fun x () Int)
   5 (declare-fun y () Int)
   6
   7 (assert (<= 0 x))
   8 (assert (<= 0 y))
   9 (assert (< x y))
  10 (assert (> (pow2 x) (pow2 y)))
  11
  12 (check-sat)