BTOR2

word-level model checking format for capturing models of hardware and potentially software in a bit-precise manner; a non-backward-compatible extension of BTOR, which was tailored towards bit-vectors and one-dimensional bit-vector arrays, BTOR2 has explicit sort declarations and register/memory initialisations; inpired by a new AIGER format

<num>     ::= positive unsigned integer (greater than zero)
<uint>    ::= unsigned integer (including zero)
<string>  ::= sequence of whitespace and printable characters without '\n'
<symbol>  ::= sequence of printable characters without '\n'
<comment> ::= ';' <string>
<nid>     ::= <num>
<sid>     ::= <num>
<const>   ::= 'const' <sid> [0-1]+
<constd>  ::= 'constd' <sid> ['-']<uint>
<consth>  ::= 'consth' <sid> [0-9a-fA-F]+
<input>   ::= ( 'input' | 'one' | 'ones' | 'zero' ) <sid> | <const> | <constd> | <consth>
<state>   ::= 'state' <sid>
<bitvec>  ::= 'bitvec' <num>
<array>   ::= 'array' <sid> <sid>
<node>    ::= <sid> 'sort' ( <array> | <bitvec> )
            | <nid> ( <input> | <state> )
            | <nid> <opidx> <sid> <nid> <uint> [<uint>]
            | <nid> <op> <sid> <nid> [<nid> [<nid>]]
            | <nid> ( 'init' | 'next' ) <sid> <nid> <nid>
            | <nid> ( 'bad' | 'constraint' | 'fair' | 'output' ) <nid>
            | <nid> 'justice' <num> ( <nid> )+
<line>    ::= <comment> | <node> [<symbol>] [<comment>]
<btor>    ::= ( <line> '\n' )+