importing context "Alarms12"... parsing SAL file "Alarms12.sal"... creating abstract syntax tree for context "Alarms12"... ast generation time: 0.01 secs type checking context "Alarms12"... type-checker time: 0.02 secs flattening modules in the assertion located at [Context: scratch, line(1), column(1)] calculating implicit assignments of base module at [Context: Alarms12, line(20), column(2)]... calculating implicit assignments of base module at [Context: Alarms12, line(35), column(4)]... calculating implicit assignments of base module at [Context: Alarms12, line(77), column(4)]... calculating implicit assignments of base module at [Context: Alarms12, line(120), column(2)]... assertion flattening time: 0.0 secs simplifying abstract syntax tree... simplification time: 0.01 secs expanding function applications... expansion time: 0.03 secs eliminating common subexpressions in an assertion... eliminating common subexpressions in a flat module... eliminating common subexpressions... starting a new iteration of the common subexpression elimination procedure... simplifying result of the common subexpression elimination procedure... eliminating common subexpressions... expression doesn't contain common (shared) subexpressions... eliminating common subexpressions... starting a new iteration of the common subexpression elimination procedure... starting a new iteration of the common subexpression elimination procedure... simplifying result of the common subexpression elimination procedure... eliminating common subexpressions... expression doesn't contain common (shared) subexpressions... eliminating common subexpressions... expression doesn't contain common (shared) subexpressions... eliminating common subexpressions... expression doesn't contain common (shared) subexpressions... flat module -- common subexpression elimination time: 0.16 secs assertion -- common subexpression elimination time: 0.16 secs creating monitor (buchi-automata) for LTL property... LTL -> VWAA (very weak alternating automata)... VWAA -> GBA (generalized buchi automata)... simplifying GBA... GBA -> BA (buchi automata)... simplifying BA... number of states in the BA: 4 eliminating common subexpressions... starting a new iteration of the common subexpression elimination procedure... simplifying result of the common subexpression elimination procedure... monitor generation time: 0.0 secs flattening data structure in flat module... flattening time: 0.02 secs flattening data structures in the property... flattening time: 0.0 secs simplifying abstract syntax tree... simplification time: 0.03 secs substituting simple definitions... substitution time: 0.0 secs simplifying abstract syntax tree... simplification time: 0.0 secs number of system variables: 19, number of auxiliary variables: 0 executing BMC from depth 0 to 12... BMC depth: 12... building BMC formula... build time: 0.07 secs simplifying formula... including type constraints... converting (remaining) scalars to integers... preprocessing type predicates... simplification time: 0.14 secs formula size: 137584 nodes executing Yices... YICES command: yices --evidence "/tmp/sal-mbolton-17752-input.yices" > "/tmp/sal-mbolton-17752-output.yices" YICES execution time: 63.19 secs parsing output produced by YICES... BMC time: 63.47 secs total execution time: 63.76 secs