message: Undef refinement check: consider fresh variables that were produced
  for a specific expression. Since we are rewriting some of these expressions, we may need
  to refresh those variables.
  This is in alternative to redo vcgen from scratch (which is slow).
diff: @@ -384,6 +384,16 @@ static expr encode_undef_refinement(const Type &type, const State::ValTy &a,
  for (auto &v : val.undef_vars) {
  repls.emplace_back(v, expr::some(v));
  }
  +
  + // We need to consider fresh variables that are produced for specific
  + // expressions. Since we are now rewriting those expressions, those
  + // variables *may* need to be refreshed. For now consider just NaNs.
  + if (!repls.empty()) {
  + for (auto &v : val.val.vars()) {
  + if (v.fn_name().starts_with("#NaN!"))
  + repls.emplace_back(v, expr::some(v));
  + }
  + }
  return val.val.value.subst(repls);
  };
  