prefer explicit error message to unspecific Options exception: Z3 proof traces may lack information necessary for replay when dealing with quantified formulas
session Spec_Check in Spec_Check = Pure + theories Spec_Check Examplessession SML in SML = Pure + theories Examples