Add documentation for --disable-fmf-inst-gen, which removes a warning
Fix erroneous results when the logic was incorrectly specified (by throwing LogicException).  Also correct a case where sharing was doing some work during pure theory solving.