DOING LOCALIZATION...

Starting conversion of file: /home/bekkouche/eclipse-workspace/Benchmarks_LocFaults/TriPerimetre/TriPerimetrev4/Progs_with_spec/TriPerimetrev4_TestCase_92.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 := 8 --> line -1
triperimetre_0_j_0 := 8 --> line -1
triperimetre_0_k_0 := 6 --> 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 --> line 0
triperimetre_0_res_2 := triperimetre_0_res_1 --> line 0
triperimetre_0_trityp_4 := ( triperimetre_0_trityp_3 + 3 ) --> line 31
triperimetre_0_res_3 := ( 2 * triperimetre_0_j_0 ) --> line 32
triperimetre_0_res_4 := ( triperimetre_0_res_3 + triperimetre_0_i_0 ) --> line 46
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 32}
{line 46}

Runtime of the method that compute MCS: 0.032
MIVcard(ctrs,line 32)=1.0
MIVcard(ctrs,line 46)=1.0
MIVcard(ctrs,line 68)=1.0

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

Runtime of the method that compute IIS using Deletion Filter: 0.011
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 12
{CE,line 68,line 46,line 32,POST}

Runtime of the method that compute IIS using QuickExplain: 0.026
   IIS in CSP_a using the conflict refiner implementation of CPLEX:
{CE,line 32,line 46,line 68,POST}

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

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


Solver: CPLEX
1. CSP_d:
line 30(If) : ( triperimetre_0_j_0 == triperimetre_0_i_0 )
------------------------
2. CSP_a:
triperimetre_0_i_0 := 8 --> line -1
triperimetre_0_j_0 := 8 --> line -1
triperimetre_0_k_0 := 6 --> 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 --> line 0
triperimetre_0_res_2 := triperimetre_0_res_1 --> line 0
!( ( triperimetre_0_j_0 == triperimetre_0_i_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.004
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 7
{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.002

Solver: CPLEX
1. CSP_d:
line 34(Else) : ( triperimetre_0_trityp_4 == 0 )
------------------------
2. CSP_a:
triperimetre_0_i_0 := 8 --> line -1
triperimetre_0_j_0 := 8 --> line -1
triperimetre_0_k_0 := 6 --> 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 --> line 0
triperimetre_0_res_2 := triperimetre_0_res_1 --> line 0
triperimetre_0_trityp_4 := ( triperimetre_0_trityp_3 + 3 ) --> line 31
triperimetre_0_res_3 := ( 2 * triperimetre_0_j_0 ) --> line 32
( triperimetre_0_trityp_4 == 0 ) --> line -2

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

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

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

Runtime of the method that compute IIS using Deletion Filter: 0.006
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 9
{CE,line 31,line 0,line 23,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 23,line 0,line 31,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.006
2. Elapsed time during MCS calculation: 0.051
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.004
/***************************************************************/
By deviating '2' condition(s), we obtain:


Solver: CPLEX
1. CSP_d:
line 22(If) : ( triperimetre_0_i_0 == triperimetre_0_j_0 )
line 49(Else) : ( ( triperimetre_0_trityp_4 == 1 ) && ( ( triperimetre_0_i_0 + triperimetre_0_j_0 ) > triperimetre_0_k_0 ) )
------------------------
2. CSP_a:
triperimetre_0_i_0 := 8 --> line -1
triperimetre_0_j_0 := 8 --> line -1
triperimetre_0_k_0 := 6 --> 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 --> line 0
triperimetre_0_res_2 := triperimetre_0_res_1 --> line 0
triperimetre_0_trityp_4 := ( triperimetre_0_trityp_3 + 3 ) --> line 31
triperimetre_0_res_3 := ( 2 * triperimetre_0_j_0 ) --> line 32
!( ( triperimetre_0_i_0 == triperimetre_0_j_0 ) ) --> line -2
( ( triperimetre_0_trityp_4 == 1 ) && ( ( triperimetre_0_i_0 + triperimetre_0_j_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.006
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 9
{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

The resulats:
1. Elapsed time during DFS exploration: 0.006
2. Elapsed time during MCS calculation: 0.002
3. Elapsed time during IIS isolation using Deletion Filter: 0.006
4. Elapsed time during IIS isolation using QuickExplain: 0.001
5. Elapsed time during IIS isolation using Conflict Refiner: 0.001
/***************************************************************/
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.384
2. Total elapsed time during DFS exploration: 0.032

3. The time required to calculate the MCSs:0.085
4. The time required for Deletion Filter:0.027
5. The time required for QuickExplain:0.039
6. The time required for the conflict refiner implementation:0.01
7. Total elapsed time during DFS exploration and MCS calculation: 0.117
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.071
10. Total elapsed time during DFS exploration and IIS calculation using conflict refiner: 0.042
11. The number of paths that resulted in an IIS with at least one soft constraint: 2
12. Suspicious instructions (using MCSs):[32, 46, 68, 30, 34, 21, 23, 31, 22, 49]
13. Suspicious instructions (using Deletion Filter):[32, 49, 34, 68, 21, 22, 23, 46, 30, 31]
14. Suspicious instructions (using QuickExplain):[32, 49, 34, 68, 21, 22, 23, 46, 30, 31]
15. Suspicious instructions (using Conflict Refiner):[32, 49, 34, 68, 21, 22, 23, 46, 30, 31]

Total elapsed time: 0.625 s.