Program verification is a fundamental aspect of software engineering, aimed at ensuring the correctness and compliance of software systems with their specified requirements. A key methodology in this domain is the application of Constrained Horn Clauses (CHCs), a tool for automating reasoning tasks such as the verification of smart contracts and the assurance of functional and memory safety in programs. This project focuses on Eldarica [1], a CHC solver that functions as the backend for TriCera [2], both open-source tools developed at Uppsala University. The main objective of this project is to investigate and optimize various encoding strategies within Eldarica. The process of encoding problems into CHCs is crucial for the efficiency and efficacy of program verification. This project aims to experiment with novel encoding techniques in Eldarica, contributing to the fields of automated reasoning and software verification. References: [1] Eldarica Project, Uppsala University, available at https://github.com/uuverifiers/eldarica [2] TriCera Project, Uppsala University, available at https://github.com/uuverifiers/tricera