DOING LOCALIZATION...

Starting conversion of file: /home/bekkouche/eclipse-workspace/Benchmarks_LocFaults/TriPerimetre/TriPerimetrev2/Progs_with_spec/TriPerimetrev2_TestCase_6.java
Loops are unwound 10 times.
The size of the constructed CFG: 42

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: CPLEX
1. CSP_d: empty set
------------------------
2. CSP_a:
triperimetre_0_i_0 := 5 --> line -1
triperimetre_0_j_0 := 6 --> line -1
triperimetre_0_k_0 := 5 --> line -1
triperimetre_0_trityp_0 := 0 --> line 14
triperimetre_0_res_0 := 0 --> line 15
triperimetre_0_trityp_1 := 0 --> line 21
triperimetre_0_trityp_2 := triperimetre_0_trityp_1 --> line 0
triperimetre_0_res_1 := triperimetre_0_res_0 --> line 0
triperimetre_0_trityp_3 := ( triperimetre_0_trityp_2 + 2 ) --> line 27
triperimetre_0_res_2 := ( 2 * triperimetre_0_j_0 ) --> line 28
triperimetre_0_trityp_4 := triperimetre_0_trityp_3 --> line 0
triperimetre_0_res_3 := triperimetre_0_res_2 --> line 0
triperimetre_0_res_4 := ( triperimetre_0_res_3 + triperimetre_0_j_0 ) --> line 54
triperimetre_0_trityp_5 := triperimetre_0_trityp_4 --> line 0
triperimetre_0_Result_0 := triperimetre_0_res_4 --> line 68
( ( ( ( ( ( ( ( ( ( ( triperimetre_0_i_0 + triperimetre_0_j_0 ) ) <= triperimetre_0_k_0 ) || ( ( ( triperimetre_0_j_0 + triperimetre_0_k_0 ) ) <= triperimetre_0_i_0 ) ) || ( ( ( triperimetre_0_i_0 + triperimetre_0_k_0 ) ) <= triperimetre_0_j_0 ) ) ) ==> ( ( triperimetre_0_Result_0 == -1 ) ) ) ) && ( ( ( ( !( ( ( ( ( ( ( triperimetre_0_i_0 + triperimetre_0_j_0 ) ) <= triperimetre_0_k_0 ) || ( ( ( triperimetre_0_j_0 + triperimetre_0_k_0 ) ) <= triperimetre_0_i_0 ) ) || ( ( ( triperimetre_0_i_0 + triperimetre_0_k_0 ) ) <= triperimetre_0_j_0 ) ) ) ) && ( ( ( triperimetre_0_i_0 == triperimetre_0_j_0 ) && ( triperimetre_0_j_0 == triperimetre_0_k_0 ) ) ) ) ) ==> ( ( triperimetre_0_Result_0 == ( ( triperimetre_0_i_0 + triperimetre_0_j_0 ) + triperimetre_0_k_0 ) ) ) ) ) ) && ( ( ( ( ( !( ( ( ( ( ( ( triperimetre_0_i_0 + triperimetre_0_j_0 ) ) <= triperimetre_0_k_0 ) || ( ( ( triperimetre_0_j_0 + triperimetre_0_k_0 ) ) <= triperimetre_0_i_0 ) ) || ( ( ( triperimetre_0_i_0 + triperimetre_0_k_0 ) ) <= triperimetre_0_j_0 ) ) ) ) && !( ( ( ( triperimetre_0_i_0 == triperimetre_0_j_0 ) && ( triperimetre_0_j_0 == triperimetre_0_k_0 ) ) ) ) ) && ( ( ( ( triperimetre_0_i_0 == triperimetre_0_j_0 ) || ( triperimetre_0_j_0 == triperimetre_0_k_0 ) ) || ( triperimetre_0_i_0 == triperimetre_0_k_0 ) ) ) ) ) ==> ( ( triperimetre_0_Result_0 == ( ( triperimetre_0_i_0 + triperimetre_0_j_0 ) + triperimetre_0_k_0 ) ) ) ) ) ) && ( ( ( ( ( !( ( ( ( ( ( ( triperimetre_0_i_0 + triperimetre_0_j_0 ) ) <= triperimetre_0_k_0 ) || ( ( ( triperimetre_0_j_0 + triperimetre_0_k_0 ) ) <= triperimetre_0_i_0 ) ) || ( ( ( triperimetre_0_i_0 + triperimetre_0_k_0 ) ) <= triperimetre_0_j_0 ) ) ) ) && !( ( ( ( triperimetre_0_i_0 == triperimetre_0_j_0 ) && ( triperimetre_0_j_0 == triperimetre_0_k_0 ) ) ) ) ) && !( ( ( ( ( triperimetre_0_i_0 == triperimetre_0_j_0 ) || ( triperimetre_0_j_0 == triperimetre_0_k_0 ) ) || ( triperimetre_0_i_0 == triperimetre_0_k_0 ) ) ) ) ) ) ==> ( ( triperimetre_0_Result_0 == ( ( triperimetre_0_i_0 + triperimetre_0_j_0 ) + triperimetre_0_k_0 ) ) ) ) ) ) --> line -2

The system is infeasible
------------------------
3. MCS in CSP_a:
{line 28}
{line 0}
{line 54}
{line 68}

Runtime of the method that compute MCS: 0.042
MIVcard(ctrs,line 28)=1.0
MIVcard(ctrs,line 0)=1.0
MIVcard(ctrs,line 54)=1.0
MIVcard(ctrs,line 68)=1.0

The number of instructions suspected: 3
   IIS in CSP_a using Deletion Filter:
{CE,line 28,line 0,line 54,line 68,POST}

Runtime of the method that compute IIS using Deletion Filter: 0.014
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 12
{CE,line 68,line 54,line 0,line 28,POST}

Runtime of the method that compute IIS using QuickExplain: 0.032
   IIS in CSP_a using the conflict refiner implementation of CPLEX:
{CE,line 28,line 0,line 54,line 68,POST}

Runtime of the method that compute IIS using the conflict refiner implementation of CPLEX: 0.006

The resulats:
1. Elapsed time during DFS exploration: 0.018
2. Elapsed time during MCS calculation: 0.042
3. Elapsed time during IIS isolation using Deletion Filter: 0.014
4. Elapsed time during IIS isolation using QuickExplain: 0.032
5. Elapsed time during IIS isolation using Conflict Refiner: 0.006
/***************************************************************/
By deviating '1' condition(s), we obtain:


Solver: CPLEX
1. CSP_d:
line 26(If) : ( triperimetre_0_i_0 == triperimetre_0_k_0 )
------------------------
2. CSP_a:
triperimetre_0_i_0 := 5 --> line -1
triperimetre_0_j_0 := 6 --> line -1
triperimetre_0_k_0 := 5 --> line -1
triperimetre_0_trityp_0 := 0 --> line 14
triperimetre_0_res_0 := 0 --> line 15
triperimetre_0_trityp_1 := 0 --> line 21
triperimetre_0_trityp_2 := triperimetre_0_trityp_1 --> line 0
triperimetre_0_res_1 := triperimetre_0_res_0 --> line 0
!( ( triperimetre_0_i_0 == triperimetre_0_k_0 ) ) --> line -2

The system is infeasible
------------------------
3. MCS in CSP_a:

Runtime of the method that compute MCS: 0.002

The number of instructions suspected: 0
   IIS in CSP_a using Deletion Filter:
{CE,POST}

Runtime of the method that compute IIS using Deletion Filter: 0.003
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 5
{CE,POST}

Runtime of the method that compute IIS using QuickExplain: 0.001
   IIS in CSP_a using the conflict refiner implementation of CPLEX:
{CE,POST}

Runtime of the method that compute IIS using the conflict refiner implementation of CPLEX: 0.001

Solver: CPLEX
1. CSP_d:
line 34(Else) : ( triperimetre_0_trityp_4 == 0 )
------------------------
2. CSP_a:
triperimetre_0_i_0 := 5 --> line -1
triperimetre_0_j_0 := 6 --> line -1
triperimetre_0_k_0 := 5 --> line -1
triperimetre_0_trityp_0 := 0 --> line 14
triperimetre_0_res_0 := 0 --> line 15
triperimetre_0_trityp_1 := 0 --> line 21
triperimetre_0_trityp_2 := triperimetre_0_trityp_1 --> line 0
triperimetre_0_res_1 := triperimetre_0_res_0 --> line 0
triperimetre_0_trityp_3 := ( triperimetre_0_trityp_2 + 2 ) --> line 27
triperimetre_0_res_2 := ( 2 * triperimetre_0_j_0 ) --> line 28
triperimetre_0_trityp_4 := triperimetre_0_trityp_3 --> line 0
triperimetre_0_res_3 := triperimetre_0_res_2 --> line 0
( triperimetre_0_trityp_4 == 0 ) --> line -2

The system is infeasible
------------------------
3. MCS in CSP_a:
{line 27}
{line 0}
{line 0}
{line 21}

Runtime of the method that compute MCS: 0.03
MIVcard(ctrs,line 21)=1.0
MIVcard(ctrs,line 0)=1.0
MIVcard(ctrs,line 27)=1.0
MIVcard(ctrs,line 0)=1.0

The number of instructions suspected: 2
   IIS in CSP_a using Deletion Filter:
{CE,line 21,line 0,line 27,line 0,POST}

Runtime of the method that compute IIS using Deletion Filter: 0.007
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 9
{CE,line 0,line 27,line 0,line 21,POST}

Runtime of the method that compute IIS using QuickExplain: 0.011
   IIS in CSP_a using the conflict refiner implementation of CPLEX:
{CE,line 21,line 0,line 27,line 0,POST}

Runtime of the method that compute IIS using the conflict refiner implementation of CPLEX: 0.001

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


The resulats:
1. Elapsed time during DFS exploration: 0.003
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.003
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.368
2. Total elapsed time during DFS exploration: 0.035

3. The time required to calculate the MCSs:0.074
4. The time required for Deletion Filter:0.024
5. The time required for QuickExplain:0.044
6. The time required for the conflict refiner implementation:0.008
7. Total elapsed time during DFS exploration and MCS calculation: 0.109
8. Total elapsed time during DFS exploration and IIS calculation using Deletion Filter: 0.059
9. Total elapsed time during DFS exploration and IIS calculation using QuickExplain: 0.079
10. Total elapsed time during DFS exploration and IIS calculation using conflict refiner: 0.043
11. The number of paths that resulted in an IIS with at least one soft constraint: 2
12. Suspicious instructions (using MCSs):[28, 54, 68, 26, 34, 21, 27]
13. Suspicious instructions (using Deletion Filter):[34, 68, 21, 54, 26, 27, 28]
14. Suspicious instructions (using QuickExplain):[34, 68, 21, 54, 26, 27, 28]
15. Suspicious instructions (using Conflict Refiner):[34, 68, 21, 54, 26, 27, 28]

Total elapsed time: 0.601 s.