TcTerm: only warn about missing variables in SMTPats in phase1

The pattern could have an implicit that is to be solved by unification
or typeclass resolution, so warning in phase1 could just give false
positives.

Fixes #3081

src/typechecker/FStar.TypeChecker.TcTerm.fst

@@ -1754,7 +1754,8 @@ and tc_value env (e:term) : term
     let c, uc, f = tc_comp env c in
     let e = {U.arrow bs c with pos=top.pos} in
     (* checks the SMT pattern associated with this function is properly defined with regard to context *)
-    check_smt_pat env e bs c;
+    if not env.phase1 then
+      check_smt_pat env e bs c;
     (* taking the maximum of the universes of the computation and of all binders *)
     let u = S.U_max (uc::us) in
     (* create a universe of level u *)