(logic QF_ABV :smt-lib-version 2.6 :smt-lib-release "2017-11-24" :written-by "Cesare Tinelli and Clark Barrett" :date "2010-07-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. 2013-06-24 Changed references to Fixed_Size_Bitvectors to FixedSizeBitVectors. " :theories (FixedSizeBitVectors ArraysEx) :language "Closed quantifier-free formulas built over the FixedSizeBitVectors and ArraysEx signatures, with the restriction that all array terms have sort of the form (Array (_ BitVec i) (_ BitVec j)) for some i, j > 0. " :extensions "As in the logic QF_BV." )