From 5122437fc2f5564365994313ef3b0c42364dcfa2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 18 Jun 2026 20:59:37 +0000 Subject: [PATCH] cprover: only equate same-address-type pairs in axiom field-condition eval In axiomst::evaluate_fc, two evaluate expressions can only alias when their object addresses have the same type; skip incompatible-address-type pairs rather than conditionally typecasting one address to the other's type. Co-authored-by: Kiro --- src/cprover/axioms.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/cprover/axioms.cpp b/src/cprover/axioms.cpp index e381f17abbb..e38b930fca3 100644 --- a/src/cprover/axioms.cpp +++ b/src/cprover/axioms.cpp @@ -65,9 +65,13 @@ void axiomst::evaluate_fc() if(a_it->state() != b_it->state()) continue; + // Skip pairs with incompatible address types — they can never + // point to the same location. + if(a_it->address().type() != b_it->address().type()) + continue; + auto a_op = a_it->address(); - auto b_op = typecast_exprt::conditional_cast( - b_it->address(), a_it->address().type()); + auto b_op = b_it->address(); auto operands_equal = equal_exprt(a_op, b_op); auto implication = implies_exprt( operands_equal,