kind2 v2.0.0-7-gdcc7f6f



====================================================================================================================
Analyzing until_3v
  with First top: 'until_3v'
             subsystems
               | concrete: until_true, until_false, timeab_tmp, timeab_exp, timeab, min, forall_a, exist

<Success> Property until_false[l287c24].timeab[l213c39].assume[l117c2] is valid by property directed reachability (IA) after 0.502s.

<Success> Property until_true[l286c23].timeab[l157c26].timeab_tmp[l122c17].assume[l102c3] is valid by inductive step after 0.665s.

<Success> Property until_true[l286c23].timeab[l157c26].timeab_exp[l118c19].assume[l89c5] is valid by inductive step after 0.665s.

<Success> Property until_true[l286c23].timeab[l157c26].assume[l117c2] is valid by inductive step after 0.665s.

<Success> Property until_true[l286c23].timeab[l155c12].timeab_tmp[l122c17].assume[l102c3] is valid by inductive step after 0.665s.

<Success> Property until_true[l286c23].timeab[l155c12].timeab_exp[l118c19].assume[l89c5] is valid by inductive step after 0.665s.

<Success> Property until_true[l286c23].timeab[l155c12].assume[l117c2] is valid by inductive step after 0.665s.

<Success> Property until_false[l287c24].timeab[l215c26].timeab_tmp[l122c17].assume[l102c3] is valid by inductive step after 0.665s.

<Success> Property until_false[l287c24].timeab[l215c26].timeab_exp[l118c19].assume[l89c5] is valid by inductive step after 0.665s.

<Success> Property until_false[l287c24].timeab[l215c26].assume[l117c2] is valid by inductive step after 0.665s.

<Success> Property until_false[l287c24].timeab[l213c39].timeab_tmp[l122c17].assume[l102c3] is valid by inductive step after 0.665s.

<Success> Property until_false[l287c24].timeab[l213c39].timeab_exp[l118c19].assume[l89c5] is valid by inductive step after 0.665s.

<Success> Property until_false[l287c24].timeab[l213c39].timeab_tmp[l122c17].guarantee[l104c2] is valid by 2-induction after 0.710s.

<Success> Property until_false[l287c24].timeab[l215c26].timeab_tmp[l122c17].guarantee[l104c2] is valid by 2-induction after 0.710s.

<Success> Property until_true[l286c23].timeab[l155c12].timeab_tmp[l122c17].guarantee[l104c2] is valid by 2-induction after 0.710s.

<Success> Property until_true[l286c23].timeab[l157c26].timeab_tmp[l122c17].guarantee[l104c2] is valid by 2-induction after 0.710s.

<Success> Property until_false[l287c24].timeab[l215c26].guarantee[l118c2] is valid by 2-induction after 7.740s.

<Success> Property until_true[l286c23].timeab[l157c26].guarantee[l118c2] is valid by 2-induction after 7.740s.

<Success> Property until_true[l286c23].timeab[l155c12].guarantee[l118c2] is valid by 2-induction after 11.692s.

<Success> Property until_false[l287c24].timeab[l213c39].guarantee[l118c2] is valid by 2-induction after 13.799s.

<Error> Caught exception in invariant generator: Invalid_argument("mk_const_state_var")

<Success> Property guarantee[l283c3] is valid by property directed reachability (QE) after 26.191s.

--------------------------------------------------------------------------------------------------------------------
Summary of properties:
--------------------------------------------------------------------------------------------------------------------
guarantee[l283c3]: valid (k=1)
until_true[l286c23].timeab[l157c26].guarantee[l118c2]: valid (k=1)
until_true[l286c23].timeab[l157c26].timeab_tmp[l122c17].assume[l102c3]: valid (k=1)
until_true[l286c23].timeab[l157c26].timeab_tmp[l122c17].guarantee[l104c2]: valid (k=1)
until_true[l286c23].timeab[l157c26].timeab_exp[l118c19].assume[l89c5]: valid (k=1)
until_true[l286c23].timeab[l157c26].assume[l117c2]: valid (k=1)
until_true[l286c23].timeab[l155c12].guarantee[l118c2]: valid (k=1)
until_true[l286c23].timeab[l155c12].timeab_tmp[l122c17].assume[l102c3]: valid (k=1)
until_true[l286c23].timeab[l155c12].timeab_tmp[l122c17].guarantee[l104c2]: valid (k=1)
until_true[l286c23].timeab[l155c12].timeab_exp[l118c19].assume[l89c5]: valid (k=1)
until_true[l286c23].timeab[l155c12].assume[l117c2]: valid (k=1)
until_false[l287c24].timeab[l215c26].guarantee[l118c2]: valid (k=1)
until_false[l287c24].timeab[l215c26].timeab_tmp[l122c17].assume[l102c3]: valid (k=1)
until_false[l287c24].timeab[l215c26].timeab_tmp[l122c17].guarantee[l104c2]: valid (k=1)
until_false[l287c24].timeab[l215c26].timeab_exp[l118c19].assume[l89c5]: valid (k=1)
until_false[l287c24].timeab[l215c26].assume[l117c2]: valid (k=1)
until_false[l287c24].timeab[l213c39].guarantee[l118c2]: valid (k=1)
until_false[l287c24].timeab[l213c39].timeab_tmp[l122c17].assume[l102c3]: valid (k=1)
until_false[l287c24].timeab[l213c39].timeab_tmp[l122c17].guarantee[l104c2]: valid (k=1)
until_false[l287c24].timeab[l213c39].timeab_exp[l118c19].assume[l89c5]: valid (k=1)
until_false[l287c24].timeab[l213c39].assume[l117c2]: valid (k=1)
====================================================================================================================