(logic QF_NIA

 :written_by {Cesare Tinelli}
 :date {26/06/09}
 
 :theory Ints

 :language 
 "Closed quantifier-free formulas built over an arbitrary expansion of 
  the Ints signature with free constant symbols, containing one or more
  non-linear atoms, that is, atoms with terms of the form (* x y) where
  neither x nor y is a numeral.

  Formulas in ite terms must satisfy the same restriction as well,
  with the exception that they need not be closed.
 "
 :extensions
 "In addition to 0 and 1, numerals n > 1 are allowed also as arguments of
  predicate or function symbols. In that case, they abbreviate the term
  (+ 1 ... 1) with n occurrences of 1.
 "
)