if ( ( x != 7 || y!=0 ) && (x < 6 || x > 7) )
{
...
};

Both Mathematica and Z3 (using "simplify" command) can't make it shorter, but I've got gut feeling, that it's somewhat redundant.

Let's take a look at the right part of the expression. If $x$ must be less than 6 OR greater than 7, that it can hold any value except 6 AND 7, right?
So I can rewrite this manually:

if ( ( x != 7 || y!=0 ) && x != 6 && x != 7) )
{
...
};

This is what Mathematica can simplify:

In[]:= BooleanMinimize[(x != 7 || y != 0) && (x != 6 && x != 7)]
Out[]:= x != 6 && x != 7

$y$ gets reduced.

But am I really right?
And why Mathematica and Z3 didn't simplify this at first place?

I can use Z3 to prove that these expressions are equal to each other:

Z3 can't find counterexample, so it says "unsat", meaning, these expressions are equal to each other.
So I've rewritten this expression in my code, tests has been passed, etc.

Yes, using both Mathematica and Z3 is overkill, and this is basic boolean algebra, but after ~10 hours of sitting at a computer you can make really dumb mistakes,
and additional proof your piece of code is correct is never unwanted.