examples/smtbmc/demo4.smtc

   1 initial
   2 assume [rst]
   3
   4 always -1
   5 assume (not [rst])
   6 assume (=> [-1:inv2] [inv2])
   7
   8 final -2
   9 assume [-1:inv2]
  10 assume (not [-2:inv2])
  11 assert (= [r1] [r2])