MAYBE
Errors:

Unhandled Exception:
System.Exception: Internal T2 error (, method investigate_cex_for_fixed_cp, line 0, col 0): UNSAT path invariant (this is probably due to the incompleteness of the interpolation procedure on integers). Please contact mabrocks@microsoft.com or h.khlaaf@ucl.ac.uk
  at Microsoft.Research.T2.Lasso.investigate_cex_for_fixed_cp (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p, Microsoft.Research.T2.SafetyInterface+SafetyProver reachGraph, Microsoft.FSharp.Collections.FSharpList`1[T] pi, System.Int32 cp, Microsoft.Research.T2.Instrumentation+LexicographicInfo lex_info) [0x00332] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Lasso.investigate_cex$cont@637 (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p, Microsoft.Research.T2.SafetyInterface+SafetyProver reachGraph, Microsoft.FSharp.Collections.FSharpList`1[T] pi, Microsoft.FSharp.Collections.FSharpMap`2[TKey,TValue] found_disj_rfs, Microsoft.FSharp.Collections.FSharpMap`2[TKey,TValue] found_lex_rfs, Microsoft.Research.T2.Instrumentation+LexicographicInfo lex_info, Microsoft.FSharp.Core.FSharpOption`1[T] failing_cutpoint, Microsoft.FSharp.Core.Unit unitVar) [0x000a3] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Lasso.investigate_cex (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p, Microsoft.Research.T2.SafetyInterface+SafetyProver reachGraph, Microsoft.FSharp.Collections.FSharpList`1[T] pi, Microsoft.FSharp.Collections.FSharpMap`2[TKey,TValue] found_disj_rfs, Microsoft.FSharp.Collections.FSharpMap`2[TKey,TValue] found_lex_rfs, Microsoft.Research.T2.Instrumentation+LexicographicInfo lex_info) [0x0000b] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Termination.prover[a] (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p_orig, Microsoft.Research.T2.CTL+CTL_Formula f, System.Boolean termination_only, Microsoft.Research.T2.Utils+SetDictionary`2[Key,Value] precondMap, Microsoft.FSharp.Core.FSharpOption`1[T] fairness_constraint, System.Boolean existential, System.Boolean findPreconds, System.Boolean next) [0x003e1] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Termination.bottomUp[a] (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p, Microsoft.Research.T2.CTL+CTL_Formula f, System.Boolean termination_only, System.Int32 nest_level, Microsoft.FSharp.Core.FSharpOption`1[T] fairness_constraint, Microsoft.Research.T2.Utils+SetDictionary`2[Key,Value] propertyMap) [0x0029e] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Termination.bottomUpProver (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p, Microsoft.Research.T2.CTL+CTL_Formula f, System.Boolean termination_only, Microsoft.FSharp.Core.FSharpOption`1[T] fairness_constraint) [0x00116] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Main.main$cont@113-1 (Microsoft.Research.T2.Arguments+runMode runMode, Microsoft.Research.T2.Parameters+parameters parameters, System.String fairness_constraint_string, Microsoft.Research.T2.Programs+Program p, Microsoft.FSharp.Core.Unit unitVar) [0x00071] in <597f4945c11a1123a745038345497f59>:0 
  at Microsoft.Research.T2.Main.main (System.String[] arguments) [0x00261] in <597f4945c11a1123a745038345497f59>:0 
[ERROR] FATAL UNHANDLED EXCEPTION: System.Exception: Internal T2 error (, method investigate_cex_for_fixed_cp, line 0, col 0): UNSAT path invariant (this is probably due to the incompleteness of the interpolation procedure on integers). Please contact mabrocks@microsoft.com or h.khlaaf@ucl.ac.uk
  at Microsoft.Research.T2.Lasso.investigate_cex_for_fixed_cp (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p, Microsoft.Research.T2.SafetyInterface+SafetyProver reachGraph, Microsoft.FSharp.Collections.FSharpList`1[T] pi, System.Int32 cp, Microsoft.Research.T2.Instrumentation+LexicographicInfo lex_info) [0x00332] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Lasso.investigate_cex$cont@637 (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p, Microsoft.Research.T2.SafetyInterface+SafetyProver reachGraph, Microsoft.FSharp.Collections.FSharpList`1[T] pi, Microsoft.FSharp.Collections.FSharpMap`2[TKey,TValue] found_disj_rfs, Microsoft.FSharp.Collections.FSharpMap`2[TKey,TValue] found_lex_rfs, Microsoft.Research.T2.Instrumentation+LexicographicInfo lex_info, Microsoft.FSharp.Core.FSharpOption`1[T] failing_cutpoint, Microsoft.FSharp.Core.Unit unitVar) [0x000a3] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Lasso.investigate_cex (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p, Microsoft.Research.T2.SafetyInterface+SafetyProver reachGraph, Microsoft.FSharp.Collections.FSharpList`1[T] pi, Microsoft.FSharp.Collections.FSharpMap`2[TKey,TValue] found_disj_rfs, Microsoft.FSharp.Collections.FSharpMap`2[TKey,TValue] found_lex_rfs, Microsoft.Research.T2.Instrumentation+LexicographicInfo lex_info) [0x0000b] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Termination.prover[a] (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p_orig, Microsoft.Research.T2.CTL+CTL_Formula f, System.Boolean termination_only, Microsoft.Research.T2.Utils+SetDictionary`2[Key,Value] precondMap, Microsoft.FSharp.Core.FSharpOption`1[T] fairness_constraint, System.Boolean existential, System.Boolean findPreconds, System.Boolean next) [0x003e1] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Termination.bottomUp[a] (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p, Microsoft.Research.T2.CTL+CTL_Formula f, System.Boolean termination_only, System.Int32 nest_level, Microsoft.FSharp.Core.FSharpOption`1[T] fairness_constraint, Microsoft.Research.T2.Utils+SetDictionary`2[Key,Value] propertyMap) [0x0029e] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Termination.bottomUpProver (Microsoft.Research.T2.Parameters+parameters pars, Microsoft.Research.T2.Programs+Program p, Microsoft.Research.T2.CTL+CTL_Formula f, System.Boolean termination_only, Microsoft.FSharp.Core.FSharpOption`1[T] fairness_constraint) [0x00116] in <597f493e96b5f0a0a74503833e497f59>:0 
  at Microsoft.Research.T2.Main.main$cont@113-1 (Microsoft.Research.T2.Arguments+runMode runMode, Microsoft.Research.T2.Parameters+parameters parameters, System.String fairness_constraint_string, Microsoft.Research.T2.Programs+Program p, Microsoft.FSharp.Core.Unit unitVar) [0x00071] in <597f4945c11a1123a745038345497f59>:0 
  at Microsoft.Research.T2.Main.main (System.String[] arguments) [0x00261] in <597f4945c11a1123a745038345497f59>:0