Vibe-Coded and Tuned: A State-of-the-Art SMT Solver for QF-LRA

Mikoláš Janota, Jan Jakubův

This paper presents the SMT solver primo, which is fully vibe-coded and then parameter-tuned, achieving state-of-the-art results on linear real arithmetic (QF-LRA). The performance…