Bit-Blasting for Termination Analysis Johannes Waldmann, HTWK Leipzig, Germany I will report on the constraints that come from the application area of proving termination of term and string rewriting by interpretations, and how we solve them. These constraints are inequalities between polynomials over unknowns in the standard (plus,times), arctic (max,plus), tropical (min,plus) or fuzzy (min,max) semi-ring. In the SMT-LIB family of languages, this is QF_NIA and QF_LIA (polynomial and linear integer arithmetics, respectively). Experience from Termination Competitions shows that encoding in QF_BV (bitvectors) gives better results, that can still be improved by hand-made bit-blasting for arithmetical constraints of small bit widths. For the fuzzy semiring, a totally different approach works. Dr. Waldmann ( http://www.imn.htwk-leipzig.de/~waldmann/ ) is a participant, organizer, and steering committee member of Termination Competitions ( http://termination-portal.org/wiki/Termination_Competition ) and co-invented the termination proof methods of match-bounds and matrix interpretations that are now widely used. He maintains a SAT encoding library for Haskell http://hackage.haskell.org/package/satchmo-2.9.7.3