Update bv proof signature and example, after discussions with Liana.
Fix --inst-max-level for strategies that use arbitrary representative terms.
Avoid doing work in quantifiers engine when no quantifiers are asserted.