(logic QF_UFIDL :written_by {Cesare Tinelli} :date {07/04/05} :theory Ints :language "Closed quantifier-free formulas built over an arbitrary expansion with free function and predicate symbols of the following subsignature of Ints: :sorts (Int) :funs ((1 Int) (- Int Int Int) (+ Int Int Int) ) :preds ((<= Int Int) (< Int Int) (>= Int Int) (> Int Int) ) and such that every term headed by + or - is, modulo commutativity, a term of the form (op t 1) where op is + or -, and t is an SMT-LIB term. " :extensions "Modulo commutativity of +, nested increments of the form (+ 1 ... (+ 1 t)) with n occurrences of 1 can be abbreviated as (+ n t). Similarly for -. " )