Figure out how many inputs satisfy a given branch condition

I am trying to do the following task. Suppose I have the following program:

int foo(char a){
  if (a > 3 && a < 7) {
     if (a >= 4 && a < 6) { <--- how many solutions can satisfy this point?
        printf("win!\n");
     }
  }
}

Given input a as a char variable, we want to figure out how many possible values of a can be used to reach the nested conditions.

Obviously since a is a char variable, then only if a is within {4, 5}, the nested condition can be satisfied. But in general, how I can figure this out? Is there any solution for that?

I am aware to use certain symbolic execution technique, together with model counting technique to formally infer the satisfiable solutions for such nested conditions. But that is, although quite general in principle, too slow...