Sun Sep 16 10:05:15 EDT 2018

PRUs and instruction counting

So I got something to work, but what I miss is a good way to specify
it.  I think this is getting closer to SAT solver territory.

The problem there is how to encode the problem.

SMT seems more convenient then SAT.