This paper explores the use of Optimisation Modulo Theories (OMT) to address classic Constraint Satisfaction (and Optimisation) Problems. By leveraging the Z3 solver, we investigate the impact of different SMT logics—Linear Integer Arithmetic (LIA), Linear Real Arithmetic (LRA), Quantifier-Free Bit-Vectors (QF_BV), and Quantifier-Free Arrays with Integer Arithmetic (QF_ALIA)—on problem-solving efficiency and solution quality. A set of automatic encoding rules is proposed to transform problems initially modelled in LIA into other logics, simplifying the process for users without specialised expertise. We demonstrate how logic selection can significantly influence solver performance. For example, QF_BV excels in scheduling and sequential problems like the Nurse Scheduling Problem and the Travelling Salesman Problem. In contrast, LRA and QF_ALIA stand out in problems with broad numerical ranges, such as the Unbounded Knapsack Problem. These findings underscore the importance of an automatic logic encoder capable of dynamically selecting and transforming models into the most appropriate SMT logic for a given problem. This performance-driven logic selection approach enhances the solving process. It extends the accessibility and practicality of OMT frameworks across diverse problem domains.