examples/smtbmc/demo4.smtc


1
2
3
4
5
6
7
8
9
10
11

initial
assume [rst]

always -1
assume (not [rst])
assume (=> [-1:inv2] [inv2])

final -2
assume [-1:inv2]
assume (not [-2:inv2])
assert (= [r1] [r2])