DOING LOCALIZATION...

Starting conversion of file: /home/bekkouche/eclipse-workspace/Benchmarks_LocFaults/TriPerimetre/TriPerimetrev3/Progs_with_spec/TriPerimetrev3_TestCase_16.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 := 8 --> 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 + 1 ) --> line 23
triperimetre_0_res_1 := ( 2 * triperimetre_0_i_0 ) --> line 24
triperimetre_0_trityp_3 := ( triperimetre_0_trityp_2 + 2 ) --> line 27
triperimetre_0_res_2 := ( 2 * triperimetre_0_i_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_i_0 ) --> line 58
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 68}
{line 58}
{line 0}
{line 28}

Runtime of the method that compute MCS: 0.086
MIVcard(ctrs,line 28)=1.0
MIVcard(ctrs,line 0)=1.0
MIVcard(ctrs,line 58)=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 58,line 68,POST}

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

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

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

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


Solver: CPLEX
1. CSP_d:
line 22(If) : ( triperimetre_0_i_0 == triperimetre_0_k_0 )
------------------------
2. CSP_a:
triperimetre_0_i_0 := 5 --> line -1
triperimetre_0_j_0 := 8 --> 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_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 : 3
{CE,POST}

Runtime of the method that compute IIS using QuickExplain: 0.002
   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.002

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 := 8 --> 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 + 1 ) --> line 23
triperimetre_0_res_1 := ( 2 * triperimetre_0_i_0 ) --> line 24
triperimetre_0_trityp_3 := ( triperimetre_0_trityp_2 + 2 ) --> line 27
triperimetre_0_res_2 := ( 2 * triperimetre_0_i_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 21}
{line 23}

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

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

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

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

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

Solver: CPLEX
1. CSP_d:
line 53(Else) : ( ( triperimetre_0_trityp_4 == 2 ) && ( ( triperimetre_0_i_0 + triperimetre_0_k_0 ) > triperimetre_0_j_0 ) )
------------------------
2. CSP_a:
triperimetre_0_i_0 := 5 --> line -1
triperimetre_0_j_0 := 8 --> 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 + 1 ) --> line 23
triperimetre_0_res_1 := ( 2 * triperimetre_0_i_0 ) --> line 24
triperimetre_0_trityp_3 := ( triperimetre_0_trityp_2 + 2 ) --> line 27
triperimetre_0_res_2 := ( 2 * triperimetre_0_i_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 == 2 ) && ( ( triperimetre_0_i_0 + triperimetre_0_k_0 ) > triperimetre_0_j_0 ) ) --> line -2

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

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

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

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

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

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

The resulats:
1. Elapsed time during DFS exploration: 0.013
2. Elapsed time during MCS calculation: 0.207
3. Elapsed time during IIS isolation using Deletion Filter: 0.019
4. Elapsed time during IIS isolation using QuickExplain: 0.034
5. Elapsed time during IIS isolation using Conflict Refiner: 0.005
/***************************************************************/
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.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
/***************************************************************/
The final resulats:
1. The pretreatment(CFG building) time: 0.385
2. Total elapsed time during DFS exploration: 0.039

3. The time required to calculate the MCSs:0.293
4. The time required for Deletion Filter:0.029
5. The time required for QuickExplain:0.064
6. The time required for the conflict refiner implementation:0.013
7. Total elapsed time during DFS exploration and MCS calculation: 0.332
8. Total elapsed time during DFS exploration and IIS calculation using Deletion Filter: 0.068
9. Total elapsed time during DFS exploration and IIS calculation using QuickExplain: 0.103
10. Total elapsed time during DFS exploration and IIS calculation using conflict refiner: 0.052
11. The number of paths that resulted in an IIS with at least one soft constraint: 3
12. Suspicious instructions (using MCSs):[28, 58, 68, 22, 34, 21, 23, 27, 53]
13. Suspicious instructions (using Deletion Filter):[34, 68, 21, 53, 22, 23, 58, 27, 28]
14. Suspicious instructions (using QuickExplain):[34, 68, 21, 53, 22, 23, 58, 27, 28]
15. Suspicious instructions (using Conflict Refiner):[34, 68, 21, 53, 22, 23, 58, 27, 28]

Total elapsed time: 0.871 s.