§ Modular Arithmetic Decision Procedure

• Modular Arithmetic Decision Procedure by Domagoj and Madanlal
• For bounded integers, actually just perform the hensel lifting. Can handle polynomial fragment.
• I am not sure why this is supposed to be better than just performing a bit-encoding followed by bitblasting, by deriving the width bounds.
• I suppose the idea is that if the system is linear, then linear algebra can help us find the seed solution, and lifts should also be faster?