From 084a6f35eb2f1ad7db7b6c89bf580e36f4052a75 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 2 Jan 2014 17:37:35 -0800
Subject: [PATCH] fix bug reported by Nuno Lopes: inlining is unsound for
 negated predicates

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/transforms/dl_mk_rule_inliner.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index 3e933b099..d9dad5c56 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -527,6 +527,9 @@ namespace datalog {
 
 
     bool mk_rule_inliner::do_eager_inlining(rule * r, rule_set const& rules, rule_ref& res) {
+        if (r->has_negation()) {
+            return false;
+        }
 
         SASSERT(rules.is_closed());
         const rule_stratifier& strat = rules.get_stratifier();