anchor.diff:                               (Print.term_to_string t0)
                                (Print.term_to_string t))
   
  -      | Tm_lazy i -> encode_term (U.unfold_lazy i) env
  +      | Tm_lazy i ->
  +        let e = U.unfold_lazy i in
  +        if Env.debug env.tcenv <| Options.Other "SMTEncoding" then
  +            BU.print2 ">> Unfolded (%s) ~> (%s)\n" (Print.term_to_string t0)
  +                                                   (Print.term_to_string e);
  +        encode_term e env
   
         | Tm_bvar x ->
           failwith (BU.format1 "Impossible: locally nameless; got %s" (Print.bv_to_string x))
  
positive.code:         //
          // Actual encoding: `q ~> pack qv where qv is the view of q
          let tv = EMB.embed RE.e_term_view t.pos (R.inspect_ln qt) in
          let t = U.mk_app (RD.refl_constant_term RD.fstar_refl_pack_ln) [S.as_arg tv] in
          encode_term t env
  
  
negative.code: and encode_term (t:typ) (env:env_t) : (term         (* encoding of t, expects t to be in normal form already *)
                                       * decls_t)     (* top-level declarations to be emitted (for shared representations of existentially bound terms *) =
  
      (* GM: Why keep `t`? *)
      let t0 = SS.compress t in
      if Env.debug env.tcenv <| Options.Other "SMTEncoding"
      then BU.print3 "(%s) (%s)   %s\n" (Print.tag_of_term t) (Print.tag_of_term t0) (Print.term_to_string t0);
  