Refactor how we handle bitwidths of input variables. Instead of trying to determine possible query widths by looking at free variables, specify per LHS term the range of widths considered.
Also:
Use the solver to resolve the essentially-dependently-typed widths.
Provide an option to run with only dynamic widths.
This is still failing some rotate tests with solver crashes, and, more interestingly, some iadd tests with counterexamples. Investigating.
Refactor how we handle bitwidths of input variables. Instead of trying to determine possible query widths by looking at free variables, specify per LHS term the range of widths considered.
Also: