*** This is nuXmv 1.1.1 (compiled on Wed Jun  1 10:18:42 2016)
*** Copyright (c) 2014-2016, Fondazione Bruno Kessler

*** For more information on nuXmv see https://nuxmv.fbk.eu
*** or email to <nuxmv@list.fbk.eu>.
*** Please report bugs at https://nuxmv.fbk.eu/bugs
*** (click on "Login Anonymously" to access)
*** Alternatively write to <nuxmv@list.fbk.eu>.

*** This version of nuXmv is linked to NuSMV 2.6.0.
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@list.fbk.eu>.
*** Copyright (C) 2010-2014, Fondazione Bruno Kessler

*** This version of nuXmv is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado

*** This version of nuXmv is linked to the MiniSat SAT solver. 
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson

*** This version of nuXmv is linked to MathSAT
*** Copyright (C) 2009-2016 by Fondazione Bruno Kessler
*** Copyright (C) 2009-2016 by University of Trento
*** See http://mathsat.fbk.eu

Number of Input Variables: 5
    2: boolean
    1: unsigned word[14]
    1: {Op, Teach}
    1: signed word[14]
Number of State Variables: 19
    3: boolean
    1: {Ok, NoTeachPoints, Teaching, InvalidTeachPoints, InvalidInputValue}
    3: unsigned word[14]
    1: {Op, Teach}
    1: {l0, l1, l2, l3, l4, l5, l6, l7, SUCCESS, FAIL}
   10: signed word[14]
Number of Frozen Variables: 4
    4: signed word[14]
  mode : {Op, Teach}
  
  TPy : signed word[14]
  
  TPSet : boolean
  
  SensorInput : unsigned word[14]
  
  system.SensorOutput : signed word[14]
  
  system.Status : {Ok, NoTeachPoints, Teaching, (other 2 values)}
  
  system.initial : boolean
  
  system.lastmode : {Op, Teach}
  
  system.m : signed word[14]
  
  system.t : signed word[14]
  
  system.teachstep : signed word[14]
  
  system.timeout$ET : unsigned word[14]
  
  system.timeout$IN : boolean
  
  system.timeout$PT : unsigned word[14]
  
  system.timeout$Q : boolean
  
  system.x1 : signed word[14]
  
  system.x2 : signed word[14]
  
  system.x_temp : signed word[14]
  
  system.y1 : signed word[14]
  
  system.y2 : signed word[14]
  
  system.y_temp : signed word[14]
  
  spec.dice : boolean
  
  spec.x1 : signed word[14]
  
  spec.x2 : signed word[14]
  
  spec.y1 : signed word[14]
  
  spec.y2 : signed word[14]
  
  spec.counter : unsigned word[14]
  
  spec.state : {l0, l1, l2, l3, l4, l5, l6, l7, SUCCESS, FAIL}
  
Number of bits: 280 (56 frozen, 31 input, 193 state)
-- no proof or counterexample found with bound 4
-- no proof or counterexample found with bound 5
-- invariant !(state = FAIL) IN spec is false
-- as demonstrated by the following execution sequence
Trace Description: IC3 counterexample 
Trace Type: Counterexample 
