Skip to content

Commit 987d384

Browse files
martinMatthias Güdemann
martin
authored and
Matthias Güdemann
committed
Switch (!a | b) for (a => b) to clarrify the intent of the code.
1 parent 40ff71b commit 987d384

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/solvers/flattening/arrays.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -348,7 +348,7 @@ void arrayst::add_array_Ackermann_constraints()
348348

349349
// add constraint
350350
lazy_constraintt lazy(lazy_typet::ARRAY_ACKERMANN,
351-
or_exprt(literal_exprt(!indices_equal_lit), values_equal));
351+
implies_exprt(literal_exprt(indices_equal_lit), values_equal));
352352
add_array_constraint(lazy, true); // added lazily
353353

354354
#if 0 // old code for adding, not significantly faster

0 commit comments

Comments
 (0)