# Incremental Formula-Based Fix Localization
## 3 Proposed Method
### Illustrative Example  
We illustrate how our proposed method work using the running example in Figure 1. Figure 5 shows the progress of AgxFaults in the firsts 4 iterations. In the figure, the green nodes represents program parts that are assumed to be correct; thus, they are encoded into the formula as hard constraints.  
After the initialization steps, the angelic program \(P_{agx}\) contains only an entry point and a normally exit point (i.e., successful terminated). The solver, \(solver\), is initialized when the soft-constraints set is empty, and the set of hard-constraints encode the entry point and the normal exit points which represent the successful terminator. In the first iteration of the loop, the algorithm do nothing important but invoke the _AgelicRefinement_ method (line 8) with input an empty angelic fix location set and an empty angelic path. Thus, the AngelicRefinement method just runs a given test case and encodes the executed statements into the formula. Figure 5 shows the state of algorithm after the first iteration. Specifically, the angelic program precisely presents only executed statements in the original error trace, while all other parts are abstracted. Figure 6 shows the set of encoded constraints in the first iteration (We eliminated the fault predicate variables \(ab\) from the clauses for simplification).  
In the second iteration, first, the solver solves the current angelic formula and returns an MCS \(\phi_{mcs}=\{foo=b_{3}\}\), which corresponds to the return statement at line 8. Then, the MCSAnalyzer component analyzes the mcs and corresponding model to identify fix location set and corresponding angelic path, (line 6 in Algorithm 1). The constructed angelic path \(\Pi_{agx}\) is the path (s,1,2,6,8,9,OK) in the CFG of the angelic program. This path is feasible because all edges in the path are deterministic. Thus, the algorithm goes to line 12 to output the newly found minimal fix candidate, and then it adds a constraint to block this solution that will occur in the next iterations. In other words, from this time, the solver considers the statement at line 8 as correct.  
In the third iteration, the solver returns an MCS \(mcs=\{b_{1}=x_{0}+y_{0}\}\), which correspond to assignment \([b=x+y]\) at line 1. The constructed angelic path for this mcs is the path (s,1,2,6,8,9,OK), which is a feasible path in the angelic program. Thus, similar to the second iteration, the algorithm outputs the newly found MFC, adds blocking constraint for line 1, and goes to the next iteration.  
Figure 5c shows the current state of the angelic program and the angelic formula in the solver. Because the blocking constraint that are added in previous iterations, the statements at line 1 and line 8 will not be considered as possible faults. Thus, the solve only needs to search in a smaller search space for the next MCSs.  
In the fourth iteration, the solver found an MCS \(mcs=\{g_{2}=(a_{1}>=y_{0})\}\), and the angelic value is \(\{^{*}g_{2}\"=True\}\). This mcs indicates the branch condition at line 6 is the fix location. The constructed angelic path for this mcs is the path (S,1,2,3,6,7,8,9,OK). Because the angelic path contain an non-deterministic branch, thus, the AngelicRefinement method is invoked with input \(mcs=\{line~{}6\}\), and its corresponding angelic value is \(True\) to  
Figure 5: Angelic program encoded during the process of AgxFaults.  
Figure 6: Constraints added in the first iteration.  
explore the true-branch of the if-statement at line 6. After the refinement, the assignment \([b=x-y]\) is presented in the angelic program, and additional constraints in Figure 7 are added into the solver.  
After the refinement, the process continues until timeout or all minimal fix candidates have been found (i.e., the solver.Check() return UNSAT).  
\[soft:b_{2}=x_{0}-y_{0}\] \[hard:\ \wedge\left(g_{2}\implies(b_{3}=b_{2})\right)\]