# MC: formula failed --- AG(o2=0)
# MC: Calling debugger for trace 1
--State
machine_concret1.m_state:S0
o1:0
o2:0
r_i1:0
fails AG(o2=0)

--Counter example is a path to a state where o2=0 is false
 --Counter example begins
--State 0:
machine_concret1.m_state:S0
o1:0
o2:0
r_i1:0

--Goes to state 1:
machine_concret1.m_state:S1
o1:1
r_i1:1
--On input:
i1:1

--Goes to state 2:
machine_concret1.m_state:S2
o1:0
o2:1
--On input:
<Unchanged>

 --Counter example ends

--State
machine_concret1.m_state:S2
o1:0
o2:1
r_i1:1
fails o2=0.