pub fn run_solver_with_static_widths( rulectx: &RuleCtx<'_>, tyctx: &TypeContext, concrete: &Option<ConcreteTest>, ) -> VerificationResult