(logic QF_LIA :smt-lib-version 2.6 :smt-lib-release "2017-11-24" :written-by "Cesare Tinelli" :date "2010-04-30" :last-updated "2015-04-25" :update-history "Note: history only accounts for content changes, not release changes. 2021-01-21 Clarified wording around what terms are included in extensions. 2015-04-25 Updated to Version 2.5. " :theories (Ints) :language "Closed quantifier-free formulas built over an arbitrary expansion of the Ints signature with free constant symbols, but whose terms of sort Int are all linear, that is, have no occurrences of the function symbols /, div, mod, and abs, and no occurrences of the function symbol *, except as specified in the :extensions attribute. " :extensions "Terms containing * with _concrete_ coefficients are also allowed, that is, terms of the form c, (* c x), or (* x c) where x is a free constant and c is a term of the form n or (- n) for some numeral n. " )