  Debugging is one of the most time-consuming and expensive tasks in software
development. Several formula-based fault localization (FBFL) methods have been
proposed, but they fail to guarantee a set of diagnoses across all failing
tests or may produce redundant diagnoses that are not subset-minimal,
particularly for programs with multiple faults.
  This paper introduces a novel fault localization approach for C programs with
multiple faults. CFaults leverages Model-Based Diagnosis (MBD) with multiple
observations and aggregates all failing test cases into a unified MaxSAT
formula. Consequently, our method guarantees consistency across observations
and simplifies the fault localization procedure. Experimental results on two
benchmark sets of C programs, TCAS and C-Pack-IPAs, show that CFaults is faster
than other FBFL approaches like BugAssist and SNIPER. Moreover, CFaults only
generates subset-minimal diagnoses of faulty statements, whereas the other
approaches tend to enumerate redundant diagnoses.
