diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index f516b2948..8584741f3 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -912,7 +912,7 @@ namespace sls { m_string_updates.reset(); u[i][j] = d[i - 1][j]; } - if (d[i][j - 1] < u[i][j] && b.can_add(i - 1)) { + if (d[i][j - 1] < u[i][j] && b.can_add(j - 1)) { m_string_updates.reset(); u[i][j] = d[i][j - 1]; } diff --git a/src/test/sls_seq_plugin.cpp b/src/test/sls_seq_plugin.cpp index b7a23a596..4c8c5340c 100644 --- a/src/test/sls_seq_plugin.cpp +++ b/src/test/sls_seq_plugin.cpp @@ -351,4 +351,28 @@ void tst_sls_seq_plugin() { app_ref eq(m.mk_eq(l, r), m); verbose_stream() << eq << "\n"; ts.repair_down_str_eq_edit_distance_incremental(eq); + + test_seq::string_instance lhs, rhs; + lhs.s = zstring("a"); + lhs.is_value.push_back(false); + lhs.prev_is_var.push_back(false); + lhs.next_is_var.push_back(false); + rhs.s = zstring("ab"); + rhs.is_value.push_back(true); + rhs.prev_is_var.push_back(false); + rhs.next_is_var.push_back(false); + rhs.is_value.push_back(false); + rhs.prev_is_var.push_back(false); + rhs.next_is_var.push_back(false); + + ENSURE(ts.edit_distance_with_updates(lhs, rhs) == 0); + ENSURE(ts.m_string_updates.size() == 2); + ENSURE(ts.m_string_updates[0].side == test_seq::side_t::right); + ENSURE(ts.m_string_updates[0].op == test_seq::op_t::add); + ENSURE(ts.m_string_updates[0].i == 0); + ENSURE(ts.m_string_updates[0].j == 1); + ENSURE(ts.m_string_updates[1].side == test_seq::side_t::right); + ENSURE(ts.m_string_updates[1].op == test_seq::op_t::del); + ENSURE(ts.m_string_updates[1].i == 1); + ENSURE(ts.m_string_updates[1].j == 0); } \ No newline at end of file