SWAP
----

This example is described in: 
"Automatic Abstraction without Counterexamples"
by K. L. McMillan and Nina Amla. 
Cadence Technical Report

They claim this is a difficult example for BMC-like
techniques.

- prove property diff for 4 registers

  % sal-smc -v 10 --assertion='swap{4}!diff'

- prove property all_diff using 1-induction for 4 registers

  % sal-bmc -v 10 -i -d 1 --assertion='swap{4}!all_diff'

- prove property diff using 1-induction and all_diff as a lemma

  % sal-bmc -v 10 -i -d 1 -l all_diff --assertion='swap{4}!diff'

- prove property all_diff using sal-smc and backward reachability

  % sal-smc -v 10 --backward --assertion='swap{4}!all_diff'

- Same example for 8 registers

  % sal-smc -v 10 --assertion='swap{8}!diff'
  % sal-bmc -v 10 -i -d 1 --assertion='swap{8}!all_diff'
  % sal-bmc -v 10 -i -d 1 -l all_diff --assertion='swap{8}!diff'
  % sal-smc -v 10 --backward --assertion='swap{8}!all_diff'

