# Automatic Repair of Buggy If Conditions and Missing Preconditions with SMT

arXiv: https://arxiv.org/abs/1404.3186 · HTML: https://mlsanity.com/paper/1404.3186/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Apr 2014.

## Built on by (most cited first, 7 of 7)

- [Keep the Conversation Going: Fixing 162 out of 337 bugs for 0.42 each using ChatGPT](https://mlsanity.com/paper/2304.00385/) (2023)
- [Copiloting the Copilots: Fusing Large Language Models with Completion Engines for Automated Program Repair](https://mlsanity.com/paper/2309.00608/) (2023)
- [FixEval: Execution-based Evaluation of Program Fixes for Programming Problems](https://mlsanity.com/paper/2206.07796/) (2022)
- [COAST: Enhancing the Code Debugging Ability of LLMs through Communicative Agent Based Data Synthesis](https://mlsanity.com/paper/2408.05006/) (2024)
- [Enhancing Automated Program Repair through Fine-tuning and Prompt Engineering](https://mlsanity.com/paper/2304.07840/) (2023)
- [Revisiting the Plastic Surgery Hypothesis via Large Language Models](https://mlsanity.com/paper/2303.10494/) (2023)
- [Exploring the Limits of ChatGPT in Software Security Applications](https://mlsanity.com/paper/2312.05275/) (2023)

## Abstract (arXiv)

We present Nopol, an approach for automatically repairing buggy if conditions and missing preconditions. As input, it takes a program and a test suite which contains passing test cases modeling the expected behavior of the program and at least one failing test case embodying the bug to be repaired. It consists of collecting data from multiple instrumented test suite executions, transforming this data into a Satisfiability Modulo Theory (SMT) problem, and translating the SMT result -- if there exists one -- into a source code patch. Nopol repairs object oriented code and allows the patches to contain nullness checks as well as specific method calls.