Function check 

pub(crate) fn check<'tcx>(
    _checker: &SmtChecker<'tcx>,
    checkpoint: &Checkpoint<'tcx>,
    _property: &Property<'tcx>,
    _forward: &ForwardVisitResult<'tcx>,
) -> SmtCheckResult