test/regress/regress2/nl/ufnia-factor-open-proof.smt2

   1 (set-logic QF_UFNIA)
   2 (set-info :status unsat)
   3 (declare-fun pow2 (Int) Int)
   4 (define-fun intmax ((k Int)) Int (- (pow2 k) 1))
   5 (define-fun intmodtotal ((pow2 Int) (a Int) (b Int)) Int (mod a b))
   6 (define-fun intneg ((k Int) (a Int)) Int 1)
   7 (define-fun intmul ((k Int) (a Int) (b Int)) Int (mod (* a b) (pow2 k)))
   8 (declare-fun k () Int)
   9 (assert (> k 0))
  10 (assert (= 1 (pow2 1)))
  11 (declare-fun %x () Int)
  12 (assert (> %x 0))
  13 (assert (not (= (intmul k %x (intmax k)) (mod (- (pow2 k) %x) (pow2 k)))))
  14 (check-sat)