From 9b7c5658c8f9b7e42607d3e56cb339821b1f12eb Mon Sep 17 00:00:00 2001 From: Alex Horn Date: Wed, 10 Jun 2015 20:06:09 +0100 Subject: [PATCH] Ignore min aggregation functions in compiler for now Signed-off-by: Alex Horn --- src/muz/rel/dl_compiler.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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);