Skip to content

Commit 4c40cd0

Browse files
committed
Add a PRECONDITION for the types of expressions that check_rec_logical_op can handle.
It should only handle `and`, `or` or `==>`.
1 parent 394497d commit 4c40cd0

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/analyses/goto_check.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1606,6 +1606,8 @@ void goto_checkt::check_rec_address(const exprt &expr, guardt &guard)
16061606

16071607
void goto_checkt::check_rec_logical_op(const exprt &expr, guardt &guard)
16081608
{
1609+
PRECONDITION(
1610+
expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies);
16091611
INVARIANT(
16101612
expr.is_boolean(),
16111613
"'" + expr.id_string() + "' must be Boolean, but got " + expr.pretty());

0 commit comments

Comments
 (0)