diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 59ba260a4..76b7f7c36 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -597,7 +597,8 @@ namespace datalog { unsigned ft_len = r->get_tail_size(); // full tail ptr_vector tail; for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { - tail.push_back(r->get_tail(tail_index)); + if (!r->is_min_tail(tail_index)) + tail.push_back(r->get_tail(tail_index)); } expr_ref_vector binding(m);