Skip to content

Commit d53bf4b

Browse files
committed
Equation validation: use base_type_eq on types, not exprs
The expr version expects two like-structured expressions and validates subexpressions pairwise, which is not the expected situation for VCCs.
1 parent 0f1abe1 commit d53bf4b

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/goto-symex/symex_target_equation.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -973,7 +973,7 @@ void symex_target_equationt::SSA_stept::validate(
973973
validate_full_expr(ssa_rhs, ns, vm);
974974
DATA_CHECK(
975975
vm,
976-
base_type_eq(ssa_lhs.get_original_expr(), ssa_rhs, ns),
976+
base_type_eq(ssa_lhs.get_original_expr().type(), ssa_rhs.type(), ns),
977977
"Type inequality in SSA assignment\nlhs-type: " +
978978
ssa_lhs.get_original_expr().type().id_string() +
979979
"\nrhs-type: " + ssa_rhs.type().id_string());

0 commit comments

Comments
 (0)