DOING LOCALIZATION...

Starting conversion of file: /home/bekkouche/eclipse-workspace/Benchmarks_LocFaults/Tcas/Tcasv34/Progs_with_spec/Tcasv34_t415.java
Loops are unwound 10 times.
The size of the constructed CFG: 66

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:
tcas_0_Cur_Vertical_Sep_0 := 994 --> line -1
tcas_0_Own_Tracked_Alt_0 := 3194 --> line -1
tcas_0_Own_Tracked_Alt_Rate_0 := 242 --> line -1
tcas_0_Other_Tracked_Alt_0 := 687 --> line -1
tcas_0_Alt_Layer_Value_0 := 1 --> line -1
tcas_0_Up_Separation_0 := 501 --> line -1
tcas_0_Down_Separation_0 := 741 --> line -1
tcas_0_Other_RAC_0 := 0 --> line -1
tcas_0_Other_Capability_0 := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[0] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[1] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[2] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[3] := 0 --> line -1
tcas_0_OLEV_0 := 0 --> line 28
tcas_0_MAXALTDIFF_0 := 0 --> line 29
tcas_0_MINSEP_0 := 0 --> line 30
tcas_0_NOZCROSS_0 := 0 --> line 31
tcas_0_NO_INTENT_0 := 0 --> line 32
tcas_0_TCAS_TA_0 := 0 --> line 33
tcas_0_UNRESOLVED_0 := 0 --> line 34
tcas_0_UPWARD_RA_0 := 0 --> line 35
tcas_0_DOWNWARD_RA_0 := 0 --> line 36
tcas_0_alt_sep_0 := 0 --> line 42
tcas_0_upward_crossing_situation_0 := 0 --> line 44
tcas_0_Inhibit_Biased_Climb_0 := 0 --> line 46
tcas_0_OLEV_1 := 600 --> line 47
tcas_0_MAXALTDIFF_1 := 600 --> line 48
tcas_0_MINSEP_1 := 300 --> line 49
tcas_0_NOZCROSS_1 := 100 --> line 50
tcas_0_NO_INTENT_1 := 0 --> line 51
tcas_0_TCAS_TA_1 := 1 --> line 52
tcas_0_UNRESOLVED_1 := 0 --> line 53
tcas_0_UPWARD_RA_1 := 1 --> line 54
tcas_0_DOWNWARD_RA_1 := 2 --> line 55
tcas_0_alt_sep_1 := tcas_0_UNRESOLVED_1 --> line 63
tcas_0_Inhibit_Biased_Climb_1 := ( tcas_0_Up_Separation_0 + tcas_0_NOZCROSS_1 ) --> line 67
tcas_0_Inhibit_Biased_Climb_2 := ( tcas_0_Up_Separation_0 + tcas_0_NOZCROSS_1 ) --> line 83
tcas_0_alt_sep_2 := tcas_0_DOWNWARD_RA_1 --> line 109
tcas_0_Result_0 := tcas_0_alt_sep_2 --> line 114
( ( tcas_0_alt_sep_2 == 0 ) ) --> line -2
tcas_0_High_Confidence_0 := true --> line -1
tcas_0_Two_of_Three_Reports_Valid_0 := true --> line -1
tcas_0_Climb_Inhibit_0 := true --> line -1
tcas_0_enabled_0 := false --> line 37
tcas_0_tcas_equipped_0 := false --> line 38
tcas_0_intent_not_known_0 := false --> line 39
tcas_0_need_upward_RA_0 := false --> line 40
tcas_0_need_downward_RA_0 := false --> line 41
tcas_0_upward_preferred_0 := false --> line 43
tcas_0_resultat_0 := false --> line 45
tcas_0_Positive_RA_Alt_Thresh_1[0] := 400 --> line 56
tcas_0_Positive_RA_Alt_Thresh_2[1] := 500 --> line 57
tcas_0_Positive_RA_Alt_Thresh_3[2] := 640 --> line 58
tcas_0_Positive_RA_Alt_Thresh_4[3] := 740 --> line 59
tcas_0_enabled_1 := ( ( tcas_0_High_Confidence_0 && ( tcas_0_Own_Tracked_Alt_Rate_0 <= tcas_0_OLEV_1 ) ) && ( tcas_0_Cur_Vertical_Sep_0 > tcas_0_MAXALTDIFF_1 ) ) --> line 60
tcas_0_tcas_equipped_1 := ( tcas_0_Other_Capability_0 == tcas_0_TCAS_TA_1 ) --> line 61
tcas_0_intent_not_known_1 := ( tcas_0_Two_of_Three_Reports_Valid_0 && ( tcas_0_Other_RAC_0 == tcas_0_NO_INTENT_1 ) ) --> line 62
tcas_0_resultat_1 := ( ( ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) && ( tcas_0_Cur_Vertical_Sep_0 >= tcas_0_MINSEP_1 ) ) && ( tcas_0_Up_Separation_0 >= tcas_0_Positive_RA_Alt_Thresh_4[tcas_0_Alt_Layer_Value_0] ) ) --> line 78
tcas_0_need_upward_RA_1 := ( tcas_0_resultat_1 && ( tcas_0_Own_Tracked_Alt_0 < tcas_0_Other_Tracked_Alt_0 ) ) --> line 81
tcas_0_resultat_2 := ( !( ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) ) || ( ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) && ( tcas_0_Up_Separation_0 >= tcas_0_Positive_RA_Alt_Thresh_4[tcas_0_Alt_Layer_Value_0] ) ) ) --> line 95
tcas_0_need_downward_RA_1 := ( tcas_0_resultat_2 && ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) ) --> line 98

The system is infeasible
------------------------
3. MCS in CSP_a:
{line 55}
{line 109}

Runtime of the method that compute MCS: 0.025
MIVcard(ctrs,line 55)=1.0
MIVcard(ctrs,line 109)=1.0

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

Runtime of the method that compute IIS using Deletion Filter: 0.04
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 44
{CE,line 109,line 55,POST}

Runtime of the method that compute IIS using QuickExplain: 0.034
   IIS in CSP_a using the conflict refiner implementation of CPLEX:
{CE,line 55,line 109,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.028
2. Elapsed time during MCS calculation: 0.025
3. Elapsed time during IIS isolation using Deletion Filter: 0.04
4. Elapsed time during IIS isolation using QuickExplain: 0.034
5. Elapsed time during IIS isolation using Conflict Refiner: 0.008
/***************************************************************/
By deviating '1' condition(s), we obtain:


Solver: CPLEX
1. CSP_d:
line 64(If) : ( ( ( tcas_0_enabled_1 && tcas_0_tcas_equipped_1 ) && tcas_0_intent_not_known_1 ) || !( tcas_0_tcas_equipped_1 ) )
------------------------
2. CSP_a:
tcas_0_Cur_Vertical_Sep_0 := 994 --> line -1
tcas_0_Own_Tracked_Alt_0 := 3194 --> line -1
tcas_0_Own_Tracked_Alt_Rate_0 := 242 --> line -1
tcas_0_Other_Tracked_Alt_0 := 687 --> line -1
tcas_0_Alt_Layer_Value_0 := 1 --> line -1
tcas_0_Up_Separation_0 := 501 --> line -1
tcas_0_Down_Separation_0 := 741 --> line -1
tcas_0_Other_RAC_0 := 0 --> line -1
tcas_0_Other_Capability_0 := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[0] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[1] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[2] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[3] := 0 --> line -1
tcas_0_OLEV_0 := 0 --> line 28
tcas_0_MAXALTDIFF_0 := 0 --> line 29
tcas_0_MINSEP_0 := 0 --> line 30
tcas_0_NOZCROSS_0 := 0 --> line 31
tcas_0_NO_INTENT_0 := 0 --> line 32
tcas_0_TCAS_TA_0 := 0 --> line 33
tcas_0_UNRESOLVED_0 := 0 --> line 34
tcas_0_UPWARD_RA_0 := 0 --> line 35
tcas_0_DOWNWARD_RA_0 := 0 --> line 36
tcas_0_alt_sep_0 := 0 --> line 42
tcas_0_upward_crossing_situation_0 := 0 --> line 44
tcas_0_Inhibit_Biased_Climb_0 := 0 --> line 46
tcas_0_OLEV_1 := 600 --> line 47
tcas_0_MAXALTDIFF_1 := 600 --> line 48
tcas_0_MINSEP_1 := 300 --> line 49
tcas_0_NOZCROSS_1 := 100 --> line 50
tcas_0_NO_INTENT_1 := 0 --> line 51
tcas_0_TCAS_TA_1 := 1 --> line 52
tcas_0_UNRESOLVED_1 := 0 --> line 53
tcas_0_UPWARD_RA_1 := 1 --> line 54
tcas_0_DOWNWARD_RA_1 := 2 --> line 55
tcas_0_alt_sep_1 := tcas_0_UNRESOLVED_1 --> line 63
tcas_0_High_Confidence_0 := true --> line -1
tcas_0_Two_of_Three_Reports_Valid_0 := true --> line -1
tcas_0_Climb_Inhibit_0 := true --> line -1
tcas_0_enabled_0 := false --> line 37
tcas_0_tcas_equipped_0 := false --> line 38
tcas_0_intent_not_known_0 := false --> line 39
tcas_0_need_upward_RA_0 := false --> line 40
tcas_0_need_downward_RA_0 := false --> line 41
tcas_0_upward_preferred_0 := false --> line 43
tcas_0_resultat_0 := false --> line 45
tcas_0_Positive_RA_Alt_Thresh_1[0] := 400 --> line 56
tcas_0_Positive_RA_Alt_Thresh_2[1] := 500 --> line 57
tcas_0_Positive_RA_Alt_Thresh_3[2] := 640 --> line 58
tcas_0_Positive_RA_Alt_Thresh_4[3] := 740 --> line 59
tcas_0_enabled_1 := ( ( tcas_0_High_Confidence_0 && ( tcas_0_Own_Tracked_Alt_Rate_0 <= tcas_0_OLEV_1 ) ) && ( tcas_0_Cur_Vertical_Sep_0 > tcas_0_MAXALTDIFF_1 ) ) --> line 60
tcas_0_tcas_equipped_1 := ( tcas_0_Other_Capability_0 == tcas_0_TCAS_TA_1 ) --> line 61
tcas_0_intent_not_known_1 := ( tcas_0_Two_of_Three_Reports_Valid_0 && ( tcas_0_Other_RAC_0 == tcas_0_NO_INTENT_1 ) ) --> line 62
!( ( ( ( tcas_0_enabled_1 && tcas_0_tcas_equipped_1 ) && tcas_0_intent_not_known_1 ) || !( tcas_0_tcas_equipped_1 ) ) ) --> line -2

The system is infeasible
------------------------
3. MCS in CSP_a:
{line 47,line 61}
{line 60,line 61}
{line 51,line 61}
{line 48,line 61}
{line 52,line 60}
{line 48,line 52}
{line 52,line 62}
{line 51,line 52}
{line 61,line 62}
{line 47,line 52}

Runtime of the method that compute MCS: 0.085
MIVcard(ctrs,line 47)=1.0
MIVcard(ctrs,line 48)=1.0
MIVcard(ctrs,line 51)=1.0
MIVcard(ctrs,line 52)=2.5
MIVcard(ctrs,line 60)=1.0
MIVcard(ctrs,line 61)=2.5
MIVcard(ctrs,line 62)=1.0

The number of instructions suspected: 7
   IIS in CSP_a using Deletion Filter:
{CE,line 52,line 61,POST}

Runtime of the method that compute IIS using Deletion Filter: 0.029
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 36
{CE,line 61,line 52,POST}

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

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

Solver: CPLEX
1. CSP_d:
line 89(Else) : ( tcas_0_Inhibit_Biased_Climb_2 > tcas_0_Down_Separation_0 )
------------------------
2. CSP_a:
tcas_0_Cur_Vertical_Sep_0 := 994 --> line -1
tcas_0_Own_Tracked_Alt_0 := 3194 --> line -1
tcas_0_Own_Tracked_Alt_Rate_0 := 242 --> line -1
tcas_0_Other_Tracked_Alt_0 := 687 --> line -1
tcas_0_Alt_Layer_Value_0 := 1 --> line -1
tcas_0_Up_Separation_0 := 501 --> line -1
tcas_0_Down_Separation_0 := 741 --> line -1
tcas_0_Other_RAC_0 := 0 --> line -1
tcas_0_Other_Capability_0 := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[0] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[1] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[2] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[3] := 0 --> line -1
tcas_0_OLEV_0 := 0 --> line 28
tcas_0_MAXALTDIFF_0 := 0 --> line 29
tcas_0_MINSEP_0 := 0 --> line 30
tcas_0_NOZCROSS_0 := 0 --> line 31
tcas_0_NO_INTENT_0 := 0 --> line 32
tcas_0_TCAS_TA_0 := 0 --> line 33
tcas_0_UNRESOLVED_0 := 0 --> line 34
tcas_0_UPWARD_RA_0 := 0 --> line 35
tcas_0_DOWNWARD_RA_0 := 0 --> line 36
tcas_0_alt_sep_0 := 0 --> line 42
tcas_0_upward_crossing_situation_0 := 0 --> line 44
tcas_0_Inhibit_Biased_Climb_0 := 0 --> line 46
tcas_0_OLEV_1 := 600 --> line 47
tcas_0_MAXALTDIFF_1 := 600 --> line 48
tcas_0_MINSEP_1 := 300 --> line 49
tcas_0_NOZCROSS_1 := 100 --> line 50
tcas_0_NO_INTENT_1 := 0 --> line 51
tcas_0_TCAS_TA_1 := 1 --> line 52
tcas_0_UNRESOLVED_1 := 0 --> line 53
tcas_0_UPWARD_RA_1 := 1 --> line 54
tcas_0_DOWNWARD_RA_1 := 2 --> line 55
tcas_0_alt_sep_1 := tcas_0_UNRESOLVED_1 --> line 63
tcas_0_Inhibit_Biased_Climb_1 := ( tcas_0_Up_Separation_0 + tcas_0_NOZCROSS_1 ) --> line 67
tcas_0_Inhibit_Biased_Climb_2 := ( tcas_0_Up_Separation_0 + tcas_0_NOZCROSS_1 ) --> line 83
( tcas_0_Inhibit_Biased_Climb_2 > tcas_0_Down_Separation_0 ) --> line -2
tcas_0_High_Confidence_0 := true --> line -1
tcas_0_Two_of_Three_Reports_Valid_0 := true --> line -1
tcas_0_Climb_Inhibit_0 := true --> line -1
tcas_0_enabled_0 := false --> line 37
tcas_0_tcas_equipped_0 := false --> line 38
tcas_0_intent_not_known_0 := false --> line 39
tcas_0_need_upward_RA_0 := false --> line 40
tcas_0_need_downward_RA_0 := false --> line 41
tcas_0_upward_preferred_0 := false --> line 43
tcas_0_resultat_0 := false --> line 45
tcas_0_Positive_RA_Alt_Thresh_1[0] := 400 --> line 56
tcas_0_Positive_RA_Alt_Thresh_2[1] := 500 --> line 57
tcas_0_Positive_RA_Alt_Thresh_3[2] := 640 --> line 58
tcas_0_Positive_RA_Alt_Thresh_4[3] := 740 --> line 59
tcas_0_enabled_1 := ( ( tcas_0_High_Confidence_0 && ( tcas_0_Own_Tracked_Alt_Rate_0 <= tcas_0_OLEV_1 ) ) && ( tcas_0_Cur_Vertical_Sep_0 > tcas_0_MAXALTDIFF_1 ) ) --> line 60
tcas_0_tcas_equipped_1 := ( tcas_0_Other_Capability_0 == tcas_0_TCAS_TA_1 ) --> line 61
tcas_0_intent_not_known_1 := ( tcas_0_Two_of_Three_Reports_Valid_0 && ( tcas_0_Other_RAC_0 == tcas_0_NO_INTENT_1 ) ) --> line 62
tcas_0_resultat_1 := ( ( ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) && ( tcas_0_Cur_Vertical_Sep_0 >= tcas_0_MINSEP_1 ) ) && ( tcas_0_Up_Separation_0 >= tcas_0_Positive_RA_Alt_Thresh_4[tcas_0_Alt_Layer_Value_0] ) ) --> line 78
tcas_0_need_upward_RA_1 := ( tcas_0_resultat_1 && ( tcas_0_Own_Tracked_Alt_0 < tcas_0_Other_Tracked_Alt_0 ) ) --> line 81

The system is infeasible
------------------------
3. MCS in CSP_a:
{line 50}
{line 83}

Runtime of the method that compute MCS: 0.025
MIVcard(ctrs,line 50)=1.0
MIVcard(ctrs,line 83)=1.0

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

Runtime of the method that compute IIS using Deletion Filter: 0.032
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 40
{CE,line 83,line 50,POST}

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

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

Solver: CPLEX
1. CSP_d:
line 99(Else) : ( tcas_0_need_upward_RA_1 && tcas_0_need_downward_RA_1 )
------------------------
2. CSP_a:
tcas_0_Cur_Vertical_Sep_0 := 994 --> line -1
tcas_0_Own_Tracked_Alt_0 := 3194 --> line -1
tcas_0_Own_Tracked_Alt_Rate_0 := 242 --> line -1
tcas_0_Other_Tracked_Alt_0 := 687 --> line -1
tcas_0_Alt_Layer_Value_0 := 1 --> line -1
tcas_0_Up_Separation_0 := 501 --> line -1
tcas_0_Down_Separation_0 := 741 --> line -1
tcas_0_Other_RAC_0 := 0 --> line -1
tcas_0_Other_Capability_0 := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[0] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[1] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[2] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[3] := 0 --> line -1
tcas_0_OLEV_0 := 0 --> line 28
tcas_0_MAXALTDIFF_0 := 0 --> line 29
tcas_0_MINSEP_0 := 0 --> line 30
tcas_0_NOZCROSS_0 := 0 --> line 31
tcas_0_NO_INTENT_0 := 0 --> line 32
tcas_0_TCAS_TA_0 := 0 --> line 33
tcas_0_UNRESOLVED_0 := 0 --> line 34
tcas_0_UPWARD_RA_0 := 0 --> line 35
tcas_0_DOWNWARD_RA_0 := 0 --> line 36
tcas_0_alt_sep_0 := 0 --> line 42
tcas_0_upward_crossing_situation_0 := 0 --> line 44
tcas_0_Inhibit_Biased_Climb_0 := 0 --> line 46
tcas_0_OLEV_1 := 600 --> line 47
tcas_0_MAXALTDIFF_1 := 600 --> line 48
tcas_0_MINSEP_1 := 300 --> line 49
tcas_0_NOZCROSS_1 := 100 --> line 50
tcas_0_NO_INTENT_1 := 0 --> line 51
tcas_0_TCAS_TA_1 := 1 --> line 52
tcas_0_UNRESOLVED_1 := 0 --> line 53
tcas_0_UPWARD_RA_1 := 1 --> line 54
tcas_0_DOWNWARD_RA_1 := 2 --> line 55
tcas_0_alt_sep_1 := tcas_0_UNRESOLVED_1 --> line 63
tcas_0_Inhibit_Biased_Climb_1 := ( tcas_0_Up_Separation_0 + tcas_0_NOZCROSS_1 ) --> line 67
tcas_0_Inhibit_Biased_Climb_2 := ( tcas_0_Up_Separation_0 + tcas_0_NOZCROSS_1 ) --> line 83
tcas_0_High_Confidence_0 := true --> line -1
tcas_0_Two_of_Three_Reports_Valid_0 := true --> line -1
tcas_0_Climb_Inhibit_0 := true --> line -1
tcas_0_enabled_0 := false --> line 37
tcas_0_tcas_equipped_0 := false --> line 38
tcas_0_intent_not_known_0 := false --> line 39
tcas_0_need_upward_RA_0 := false --> line 40
tcas_0_need_downward_RA_0 := false --> line 41
tcas_0_upward_preferred_0 := false --> line 43
tcas_0_resultat_0 := false --> line 45
tcas_0_Positive_RA_Alt_Thresh_1[0] := 400 --> line 56
tcas_0_Positive_RA_Alt_Thresh_2[1] := 500 --> line 57
tcas_0_Positive_RA_Alt_Thresh_3[2] := 640 --> line 58
tcas_0_Positive_RA_Alt_Thresh_4[3] := 740 --> line 59
tcas_0_enabled_1 := ( ( tcas_0_High_Confidence_0 && ( tcas_0_Own_Tracked_Alt_Rate_0 <= tcas_0_OLEV_1 ) ) && ( tcas_0_Cur_Vertical_Sep_0 > tcas_0_MAXALTDIFF_1 ) ) --> line 60
tcas_0_tcas_equipped_1 := ( tcas_0_Other_Capability_0 == tcas_0_TCAS_TA_1 ) --> line 61
tcas_0_intent_not_known_1 := ( tcas_0_Two_of_Three_Reports_Valid_0 && ( tcas_0_Other_RAC_0 == tcas_0_NO_INTENT_1 ) ) --> line 62
tcas_0_resultat_1 := ( ( ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) && ( tcas_0_Cur_Vertical_Sep_0 >= tcas_0_MINSEP_1 ) ) && ( tcas_0_Up_Separation_0 >= tcas_0_Positive_RA_Alt_Thresh_4[tcas_0_Alt_Layer_Value_0] ) ) --> line 78
tcas_0_need_upward_RA_1 := ( tcas_0_resultat_1 && ( tcas_0_Own_Tracked_Alt_0 < tcas_0_Other_Tracked_Alt_0 ) ) --> line 81
tcas_0_resultat_2 := ( !( ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) ) || ( ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) && ( tcas_0_Up_Separation_0 >= tcas_0_Positive_RA_Alt_Thresh_4[tcas_0_Alt_Layer_Value_0] ) ) ) --> line 95
tcas_0_need_downward_RA_1 := ( tcas_0_resultat_2 && ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) ) --> line 98
( tcas_0_need_upward_RA_1 && tcas_0_need_downward_RA_1 ) --> line -2

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

Runtime of the method that compute MCS: 0.013
MIVcard(ctrs,line 81)=1.0

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

Runtime of the method that compute IIS using Deletion Filter: 0.033
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 42
{CE,line 81,POST}

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

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

Solver: CPLEX
1. CSP_d:
line 108(If) : tcas_0_need_downward_RA_1
------------------------
2. CSP_a:
tcas_0_Cur_Vertical_Sep_0 := 994 --> line -1
tcas_0_Own_Tracked_Alt_0 := 3194 --> line -1
tcas_0_Own_Tracked_Alt_Rate_0 := 242 --> line -1
tcas_0_Other_Tracked_Alt_0 := 687 --> line -1
tcas_0_Alt_Layer_Value_0 := 1 --> line -1
tcas_0_Up_Separation_0 := 501 --> line -1
tcas_0_Down_Separation_0 := 741 --> line -1
tcas_0_Other_RAC_0 := 0 --> line -1
tcas_0_Other_Capability_0 := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[0] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[1] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[2] := 0 --> line -1
tcas_0_Positive_RA_Alt_Thresh_0[3] := 0 --> line -1
tcas_0_OLEV_0 := 0 --> line 28
tcas_0_MAXALTDIFF_0 := 0 --> line 29
tcas_0_MINSEP_0 := 0 --> line 30
tcas_0_NOZCROSS_0 := 0 --> line 31
tcas_0_NO_INTENT_0 := 0 --> line 32
tcas_0_TCAS_TA_0 := 0 --> line 33
tcas_0_UNRESOLVED_0 := 0 --> line 34
tcas_0_UPWARD_RA_0 := 0 --> line 35
tcas_0_DOWNWARD_RA_0 := 0 --> line 36
tcas_0_alt_sep_0 := 0 --> line 42
tcas_0_upward_crossing_situation_0 := 0 --> line 44
tcas_0_Inhibit_Biased_Climb_0 := 0 --> line 46
tcas_0_OLEV_1 := 600 --> line 47
tcas_0_MAXALTDIFF_1 := 600 --> line 48
tcas_0_MINSEP_1 := 300 --> line 49
tcas_0_NOZCROSS_1 := 100 --> line 50
tcas_0_NO_INTENT_1 := 0 --> line 51
tcas_0_TCAS_TA_1 := 1 --> line 52
tcas_0_UNRESOLVED_1 := 0 --> line 53
tcas_0_UPWARD_RA_1 := 1 --> line 54
tcas_0_DOWNWARD_RA_1 := 2 --> line 55
tcas_0_alt_sep_1 := tcas_0_UNRESOLVED_1 --> line 63
tcas_0_Inhibit_Biased_Climb_1 := ( tcas_0_Up_Separation_0 + tcas_0_NOZCROSS_1 ) --> line 67
tcas_0_Inhibit_Biased_Climb_2 := ( tcas_0_Up_Separation_0 + tcas_0_NOZCROSS_1 ) --> line 83
tcas_0_High_Confidence_0 := true --> line -1
tcas_0_Two_of_Three_Reports_Valid_0 := true --> line -1
tcas_0_Climb_Inhibit_0 := true --> line -1
tcas_0_enabled_0 := false --> line 37
tcas_0_tcas_equipped_0 := false --> line 38
tcas_0_intent_not_known_0 := false --> line 39
tcas_0_need_upward_RA_0 := false --> line 40
tcas_0_need_downward_RA_0 := false --> line 41
tcas_0_upward_preferred_0 := false --> line 43
tcas_0_resultat_0 := false --> line 45
tcas_0_Positive_RA_Alt_Thresh_1[0] := 400 --> line 56
tcas_0_Positive_RA_Alt_Thresh_2[1] := 500 --> line 57
tcas_0_Positive_RA_Alt_Thresh_3[2] := 640 --> line 58
tcas_0_Positive_RA_Alt_Thresh_4[3] := 740 --> line 59
tcas_0_enabled_1 := ( ( tcas_0_High_Confidence_0 && ( tcas_0_Own_Tracked_Alt_Rate_0 <= tcas_0_OLEV_1 ) ) && ( tcas_0_Cur_Vertical_Sep_0 > tcas_0_MAXALTDIFF_1 ) ) --> line 60
tcas_0_tcas_equipped_1 := ( tcas_0_Other_Capability_0 == tcas_0_TCAS_TA_1 ) --> line 61
tcas_0_intent_not_known_1 := ( tcas_0_Two_of_Three_Reports_Valid_0 && ( tcas_0_Other_RAC_0 == tcas_0_NO_INTENT_1 ) ) --> line 62
tcas_0_resultat_1 := ( ( ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) && ( tcas_0_Cur_Vertical_Sep_0 >= tcas_0_MINSEP_1 ) ) && ( tcas_0_Up_Separation_0 >= tcas_0_Positive_RA_Alt_Thresh_4[tcas_0_Alt_Layer_Value_0] ) ) --> line 78
tcas_0_need_upward_RA_1 := ( tcas_0_resultat_1 && ( tcas_0_Own_Tracked_Alt_0 < tcas_0_Other_Tracked_Alt_0 ) ) --> line 81
tcas_0_resultat_2 := ( !( ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) ) || ( ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) && ( tcas_0_Up_Separation_0 >= tcas_0_Positive_RA_Alt_Thresh_4[tcas_0_Alt_Layer_Value_0] ) ) ) --> line 95
tcas_0_need_downward_RA_1 := ( tcas_0_resultat_2 && ( tcas_0_Other_Tracked_Alt_0 < tcas_0_Own_Tracked_Alt_0 ) ) --> line 98
!( tcas_0_need_downward_RA_1 ) --> line -2

The system is infeasible
------------------------
3. MCS in CSP_a:
{line 98}
{line 95}
{line 59}
{line 58}
{line 57}

Runtime of the method that compute MCS: 0.161
MIVcard(ctrs,line 57)=1.0
MIVcard(ctrs,line 58)=1.0
MIVcard(ctrs,line 59)=1.0
MIVcard(ctrs,line 95)=1.0
MIVcard(ctrs,line 98)=1.0

The number of instructions suspected: 5
   IIS in CSP_a using Deletion Filter:
{CE,line 57,line 58,line 59,line 95,line 98,POST}

Runtime of the method that compute IIS using Deletion Filter: 0.07
   IIS in CSP_a using QuickExplain:
Length of the set of soft constraints : 42
{CE,line 98,line 95,line 59,line 58,line 57,POST}

Runtime of the method that compute IIS using QuickExplain: 0.068
   IIS in CSP_a using the conflict refiner implementation of CPLEX:
{CE,line 57,line 58,line 59,line 95,line 98,POST}

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

The resulats:
1. Elapsed time during DFS exploration: 0.024
2. Elapsed time during MCS calculation: 0.284
3. Elapsed time during IIS isolation using Deletion Filter: 0.164
4. Elapsed time during IIS isolation using QuickExplain: 0.173
5. Elapsed time during IIS isolation using Conflict Refiner: 0.085
/***************************************************************/
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.376
2. Total elapsed time during DFS exploration: 0.059

3. The time required to calculate the MCSs:0.309
4. The time required for Deletion Filter:0.204
5. The time required for QuickExplain:0.207
6. The time required for the conflict refiner implementation:0.093
7. Total elapsed time during DFS exploration and MCS calculation: 0.368
8. Total elapsed time during DFS exploration and IIS calculation using Deletion Filter: 0.263
9. Total elapsed time during DFS exploration and IIS calculation using QuickExplain: 0.266
10. Total elapsed time during DFS exploration and IIS calculation using conflict refiner: 0.152
11. The number of paths that resulted in an IIS with at least one soft constraint: 5
12. Suspicious instructions (using MCSs):[55, 109, 64, 47, 48, 51, 52, 60, 61, 62, 89, 50, 83, 99, 81, 108, 57, 58, 59, 95, 98]
13. Suspicious instructions (using Deletion Filter):[64, 98, 99, 108, 109, 81, 50, 83, 52, 55, 89, 57, 58, 59, 61, 95]
14. Suspicious instructions (using QuickExplain):[64, 98, 99, 108, 109, 81, 50, 83, 52, 55, 89, 57, 58, 59, 61, 95]
15. Suspicious instructions (using Conflict Refiner):[64, 98, 99, 108, 109, 81, 50, 83, 52, 55, 89, 57, 58, 59, 61, 95]

Total elapsed time: 1.298 s.