Skip to content

Commit b165bf9

Browse files
committed
simplifier now simplifies !(exists/forall) with multiple bindings
The simplifier can now simplify !exists and !forall with multiple bindings.
1 parent a1edc82 commit b165bf9

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/util/simplify_expr_boolean.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -204,13 +204,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
204204
else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
205205
{
206206
auto const &op_as_exists = to_exists_expr(op);
207-
return forall_exprt{op_as_exists.symbol(),
207+
return forall_exprt{op_as_exists.variables(),
208208
simplify_not(not_exprt(op_as_exists.where()))};
209209
}
210210
else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
211211
{
212212
auto const &op_as_forall = to_forall_expr(op);
213-
return exists_exprt{op_as_forall.symbol(),
213+
return exists_exprt{op_as_forall.variables(),
214214
simplify_not(not_exprt(op_as_forall.where()))};
215215
}
216216

0 commit comments

Comments
 (0)