contract

Variant1 is not terrific. It offers poor maintainability, and likely wouldn't get past Code Review unchanged.

int? checkLoginDay(int lastDay) {

We started with a verb, good. But what's the contract? How would I know if it "checked" the login day, when I inspect the null-or-int that comes back? What semantics do we place on lastDay? As caller, how would I know if I'm passing in a sensible argument? For example, maybe -1 is prohibited, but that's hard to tell.

The review context helpfully mentioned

determine the day of a login reward. If there are no more rewards, return null.

But we see no javadoc or comments here, so the poor checkLoginDay identifier is left shouldering the burden of explaining the pre- and post-conditions. It turns out it isn't up to the task.

The signature doesn't mention the _rewardStore and _progressStore global input params.

What are the units on days? Maybe they are Julian days? Is it some integer K × 86400, representing seconds since 1970 epoch? Doesn't dart offer a type to describe the concept? Or perhaps we're stuck with just int.

consistent language in comments

I have to assume that "check" is drawn from the business vocabulary. Reading a little farther on we see:

  //don't show if user is not at least level 5
  if (_progressStore.level < 5) return null;

So we started out "checking", but now we're maybe "showing", which sounds like a presentation layer responsibility.

Rather than these comments, I would prefer to see the part of a requirements document that talks about eligibility for a reward. With those English rules available, reading the Variant2 code would be straightforward.

post-condition

  return lastLoginDay + 1;

The contract seemed to be that we would "check" a "login day". This seems more like we will "get" a "foo day", where it's not yet clear to me how to describe "foo". It doesn't appear to be a day the user is known to have logged in. Maybe it's a "earliest eligibility" day?

Variant 3

  if (_progressStore.level < 5 || lastLoginDay == lastDay || !now.isDayAfter(lastLoginTimeStamp))

I agree with you that, as written, this is unpleasant to read.

But start a pair of lines with || so each disjunct is on its own line, and then it reads at least as nicely as Variant2. Possible downside is that during debugging it's harder to set breakpoint where you want it, or to insert statements for "print debugging".

long ternary

I agree with you that Variant4 is a non-starter.

We're examining "expressive" vs. "concise".

The code in Variant2 is not as expressive as it could be. Consider breaking out as many as three helper functions, with descriptive (expressive!) names, such as isEligibleCustomer. Good names obviate the need for verbose comments.

Does that lead to more concise code, in SLOC? Probably not. But it's easier to read, and easier to believe that what you're reading is true. It also gives you the opportunity to unit test individual helpers, for added confidence that the code really does what it claims.