(logic AUFLIRA :smt-lib-version 2.6 :smt-lib-release "2017-11-24" :written-by "Cesare Tinelli and Clark Barrett" :date "2010-05-05" :last-updated "2015-04-25" :update-history "Note: history only accounts for content changes, not release changes. 2015-04-25 Updated to Version 2.5. 2011-06-03 Replaced "(* c x), or (* x c)" with "c, (* c x), or (* x c)" in :extensions. (The missing case was had been left out unintentionally.) " :theories (Reals_Ints ArraysEx) :language "Closed formulas built over arbitrary expansions of the Reals_Ints and ArraysEx signatures with free sort and function symbols, but with the following restrictions: - all terms of sort Int are linear, that is, have no occurrences of the function symbols *, /, div, mod, and abs, except as specified in the :extensions attributes; - all terms of sort Real are linear, that is, have no occurrences of the function symbols * and /, except as specified in the :extensions attribute; - all array terms have sort (Array Int Real) or (Array Int (Array Int Real)). " :extensions "For every operator op with declaration (op Real Real s) for some sort s, and every term t1, t2 of sort Int and t of sort Real, the expression - (op t1 t) is syntactic sugar for (op (to_real t1) t) - (op t t1) is syntactic sugar for (op t (to_real t1)) - (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2)) " :extensions "Real or Int terms with _concrete_ coefficients are also allowed, that is, terms of the form c, (* c x), or (* x c) where x is a free constant of sort Int or Real and c is an integer or rational coefficient, respectively. - An integer coefficient is a term of the form m or (- m) for some numeral m. - A rational coefficient is a term of the form d, (- d) or (/ c n) for some decimal d, integer coefficient c and numeral n other than 0. " )