Skip to content

Commit 37ebba5

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 95b2da6 commit 37ebba5

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
@@ -971,7 +971,7 @@ void symex_target_equationt::SSA_stept::validate(
971971
validate_full_expr(ssa_rhs, ns, vm);
972972
DATA_CHECK(
973973
vm,
974-
base_type_eq(ssa_lhs.get_original_expr(), ssa_rhs, ns),
974+
base_type_eq(ssa_lhs.get_original_expr().type(), ssa_rhs.type(), ns),
975975
"Type inequality in SSA assignment\nlhs-type: " +
976976
ssa_lhs.get_original_expr().type().id_string() +
977977
"\nrhs-type: " + ssa_rhs.type().id_string());

0 commit comments

Comments
 (0)