(logic AUFLIRA

 :smt-lib-version 2.0
 :written_by "Cesare Tinelli and Clark Barrett"
 :date "2010-05-05"
 :updated "2011-06-03"
 :update_log 
 "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.
 "
)