Skip to content

Commit 9a33565

Browse files
committed
apply_condition: notequal need not have constant operand
Just as is done for equality, the not-equal case needs to test that the LHS is a symbol and the RHS is a constant before attempting to constant propagate. The problem became apparent while trying to enable abort-after-failing-C assert, but only on Visual Studio builds (owing to the code that the assert macro expands to in Visual Studio).
1 parent cee5acf commit 9a33565

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

src/goto-symex/goto_state.cpp

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,9 @@ void goto_statet::apply_condition(
141141
if(is_ssa_expr(rhs))
142142
std::swap(lhs, rhs);
143143

144+
if(!is_ssa_expr(lhs) || !goto_symex_is_constantt()(rhs))
145+
return;
146+
144147
if(rhs.is_true())
145148
apply_condition(equal_exprt{lhs, false_exprt{}}, previous_state, ns);
146149
else if(rhs.is_false())

0 commit comments

Comments
 (0)