We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 438ba8d commit 7c545c8Copy full SHA for 7c545c8
src/solvers/flattening/arrays.cpp
@@ -348,7 +348,7 @@ void arrayst::add_array_Ackermann_constraints()
348
349
// add constraint
350
lazy_constraintt lazy(lazy_typet::ARRAY_ACKERMANN,
351
- or_exprt(literal_exprt(!indices_equal_lit), values_equal));
+ implies_exprt(literal_exprt(indices_equal_lit), values_equal));
352
add_array_constraint(lazy, true); // added lazily
353
354
#if 0 // old code for adding, not significantly faster
0 commit comments