DOING LOCALIZATION...

Starting conversion of file: /home/bekkouche/eclipse-workspace/Benchmarks_LocFaults/Heron/Heronv2/Progs_with_spec/Heronv2_TestCase_9.java
Loops are unwound 10 times.
The size of the constructed CFG: 40

From the counterexample, LocFaults calculates MCS and IIS by exploring the graph in DFS from top to bottom and by deviating at most '3' conditional statements.
By deviating '0' condition(s), we obtain:


Solver: CP OPTIMIZER
1. CSP_d: empty set
------------------------
2. CSP_a:
heron_0_i_0 := 5 --> line -1
heron_0_j_0 := 8 --> line -1
heron_0_k_0 := 7 --> line -1
heron_0_trityp_0 := 0 --> line 14
heron_0_res_0 := 0 --> line 15
heron_0_s_0 := ( ( ( heron_0_i_0 + heron_0_j_0 ) + heron_0_k_0 ) / 2 ) --> line 16
heron_0_trityp_1 := 0 --> line 22
heron_0_trityp_2 := heron_0_trityp_1 --> line 0
heron_0_trityp_3 := heron_0_trityp_2 --> line 0
heron_0_trityp_4 := heron_0_trityp_3 --> line 0
heron_0_trityp_5 := 1 --> line 38
heron_0_res_1 := ( ( ( heron_0_s_0 * ( heron_0_s_0 - heron_0_i_0 ) ) * ( heron_0_s_0 - heron_0_k_0 ) ) * ( heron_0_s_0 - heron_0_k_0 ) ) --> line 39
heron_0_Result_0 := heron_0_res_1 --> line 76
( ( ( ( ( ( ( ( ( ( ( heron_0_i_0 + heron_0_j_0 ) ) <= heron_0_k_0 ) || ( ( ( heron_0_j_0 + heron_0_k_0 ) ) <= heron_0_i_0 ) ) || ( ( ( heron_0_i_0 + heron_0_k_0 ) ) <= heron_0_j_0 ) ) ) || ( ( ( ( heron_0_i_0 == 0 ) || ( heron_0_j_0 == 0 ) ) || ( heron_0_k_0 == 0 ) ) ) ) ) ==> ( ( heron_0_Result_0 == -1 ) ) ) ) && ( ( ( !( ( ( ( ( ( ( ( ( heron_0_i_0 + heron_0_j_0 ) ) <= heron_0_k_0 ) || ( ( ( heron_0_j_0 + heron_0_k_0 ) ) <= heron_0_i_0 ) ) || ( ( ( heron_0_i_0 + heron_0_k_0 ) ) <= heron_0_j_0 ) ) ) || ( ( ( ( heron_0_i_0 == 0 ) || ( heron_0_j_0 == 0 ) ) || ( heron_0_k_0 == 0 ) ) ) ) ) ) ) ==> ( ( heron_0_Result_0 == ( ( ( ( ( ( ( heron_0_i_0 + heron_0_j_0 ) + heron_0_k_0 ) ) / 2 ) * ( ( ( ( ( ( ( heron_0_i_0 + heron_0_j_0 ) + heron_0_k_0 ) ) / 2 ) ) - heron_0_i_0 ) ) ) * ( ( ( ( ( ( ( heron_0_i_0 + heron_0_j_0 ) + heron_0_k_0 ) ) / 2 ) ) - heron_0_j_0 ) ) ) * ( ( ( ( ( ( ( heron_0_i_0 + heron_0_j_0 ) + heron_0_k_0 ) ) / 2 ) ) - heron_0_k_0 ) ) ) ) ) ) ) ) --> line -2

The system is infeasible
------------------------
3. MCS in CSP_a:
{line 76}
{line 39}

Runtime of the method that compute MCS: 0.087
MIVcard(ctrs,line 39)=1.0
MIVcard(ctrs,line 76)=1.0

The number of instructions suspected: 2
   IIS in CSP_a using Deletion Filter:
{CE,line 39,line 76,POST}

Runtime of the method that compute IIS using Deletion Filter: 0.203
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 10
{CE,line 76,line 39,POST}

Runtime of the method that compute IIS using QuickExplain: 0.028
   IIS in CSP_a using the conflict refiner implementation of CP Optimizer:
{CE,line 39,line 76,POST}

Runtime of the method that compute IIS using the conflict refiner implementation of CP Optimizer: 0.02

The resulats:
1. Elapsed time during DFS exploration: 0.032
2. Elapsed time during MCS calculation: 0.087
3. Elapsed time during IIS isolation using Deletion Filter: 0.203
4. Elapsed time during IIS isolation using QuickExplain: 0.028
5. Elapsed time during IIS isolation using Conflict Refiner: 0.02
By deviating '1' condition(s), we obtain:


The resulats:
1. Elapsed time during DFS exploration: 0.002
2. Elapsed time during MCS calculation: 0.0
3. Elapsed time during IIS isolation using Deletion Filter: 0.0
4. Elapsed time during IIS isolation using QuickExplain: 0.0
5. Elapsed time during IIS isolation using Conflict Refiner: 0.0
By deviating '2' condition(s), we obtain:


The resulats:
1. Elapsed time during DFS exploration: 0.004
2. Elapsed time during MCS calculation: 0.0
3. Elapsed time during IIS isolation using Deletion Filter: 0.0
4. Elapsed time during IIS isolation using QuickExplain: 0.0
5. Elapsed time during IIS isolation using Conflict Refiner: 0.0
By deviating '3' condition(s), we obtain:


The resulats:
1. Elapsed time during DFS exploration: 0.009
2. Elapsed time during MCS calculation: 0.0
3. Elapsed time during IIS isolation using Deletion Filter: 0.0
4. Elapsed time during IIS isolation using QuickExplain: 0.0
5. Elapsed time during IIS isolation using Conflict Refiner: 0.0
/***************************************************************/
The final resulats:
1. The pretreatment(CFG building) time: 0.434
2. Total elapsed time during DFS exploration: 0.047

3. The time required to calculate the MCSs:0.087
4. The time required for Deletion Filter:0.203
5. The time required for QuickExplain:0.028
6. The time required for the conflict refiner implementation:0.02
7. Total elapsed time during DFS exploration and MCS calculation: 0.134
8. Total elapsed time during DFS exploration and IIS calculation using Deletion Filter: 0.25
9. Total elapsed time during DFS exploration and IIS calculation using QuickExplain: 0.075
10. Total elapsed time during DFS exploration and IIS calculation using conflict refiner: 0.067
11. The number of paths that resulted in an IIS with at least one soft constraint: 1
12. Suspicious instructions (using MCSs):[39, 76]
13. Suspicious instructions (using Deletion Filter):[39, 76]
14. Suspicious instructions (using QuickExplain):[39, 76]
15. Suspicious instructions (using Conflict Refiner):[39, 76]

Total elapsed time: 0.873 s.