Handle contradictory relations combination as dead paths

[karoliineh]

This fixes one cause of the IntDomain0.ArithmeticOnIntegerBot crashes at SV-COMP, found by inspecting the analysis of recursive/recHanoi02-2.c.

The crash was caused by propagating a bottom from relationAnalysis.combine_env.
In the failing recursive Hanoi case, context-insensitive summary reuse can legitimately pair a caller state with a callee summary whose constraints contradict the actual call arguments. The resulting bottom value is semantically correct and represents an infeasible path. However, combine_env continued with unify_rel becoming bottom, propagating the bottom value further, eventually leading to the ArithmeticOnIntegerBot crash.

The fix is to detect if RD.is_bot_env unify_rel and raise Deadcode immediately, treating it as an unreachable path instead of propagating bottom. Why this is the right fix:

• context coarsening for recursive functions is intentional and acceptable
• contradictory caller/callee combinations can therefore arise during summary reuse
• the correct semantics for such a contradiction is path infeasibility, not analyzer failure

During debugging, removing setting relation.no-context for recursive functions from autotuning made the crash disappear, which helped isolate the issue, showing that the contradiction came from coarse summary reuse. But the real bug was the missing dead-path handling in combine_env, not the autotuning itself.

With this fix, we should be now able to solve this task.

[sim642]

It's interesting that this kind of contradiction only became apparent now. But that may be because most of our analyses don't have abstract states which would allow this to be determined, i.e. they can happily combine pretty much anything.
In this case the contradictions only arise because the relational analysis has the x#arg variables in the return state, which indirectly describe the context which has been made insensitive.

The C2PO analysis seems to have something similar, but doesn't raise Deadcode:

analyzer/src/analyses/c2poAnalysis.ml

Lines 292 to 293 in 3bd3da1

	match D.meet (`Lifted local) f_d with
	| `Bot -> `Bot

@michael-schwarz, is it true that the C2PO analysis also infers relations between arguments and return value? If so, maybe it should also raise instead of just continuing with Bot.

[michael-schwarz]

@sim642: Yes, I think it does. The technique is called anchoring from some paper "Access-Based Localization for Octagons" by Beckschulze et al., and it was key to being able to not import a lot of imprecision from callees.