From 6017dcace39749888644862c9f7fccd2e8e0279e Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Thu, 29 Jan 2015 20:41:22 +0000
Subject: [PATCH] datalog: fix compilation for rules like a(X) :- not b(X).

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/dl_compiler.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index fa88a3316..42805d1a4 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -857,7 +857,7 @@ namespace datalog {
         ast_manager& m = m_context.get_manager();
         unsigned pt_len = r->get_positive_tail_size();
         unsigned ut_len = r->get_uninterpreted_tail_size();
-        if (pt_len == ut_len || pt_len == 0) {
+        if (pt_len == ut_len) {
             return;
         }
         // populate negative variables: