Question about abstractLevel()

[PIXEL]

Hello everyone:
I have a question about the funtion of abstractLevel() in
Solver.h of Minisat2.2.0:

Here is the source code:
inline uint32_t Solver::abstractLevel (Var x) const
{ return 1 << (level[x] & 31); }

My qusetion is:the MAX number of levels in abstractLevel()
is 32, if level is greater than 32, will it be a bug?

For example, Var x(at level 2) and Var y(at level 34) will
have the same return value of abstractLevel (),will this cause a
mistake in Clause Elimition later? or just I understand wrong?

I hope your answers, thank you!

[svadimr]

The abstract level of 2 and 34 is the same (as result of & 31), but
clause elimination will work correct. It explicitly checks if those
are the same variables.
The abstraction level is used to reduce number of those explicit
checks in case where the clauses don't share similar variables
(abstract representation).

Vadim.

[PIXEL]

Thank you for your answer.

Can I interpret your answer in this way:
In function litRedundant(), abstract level will
help us to select the Lit in learnt clause that can
not be removed by clause elimination in a quicker
way directly.
But for Lits in abstract level of 2 and 34,abstraction
level can not give us answer directly, but later the
function litRedundant() will still make the right decision.