From 6010d751eda9a03dccf85a4490377f91a99b0ed8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 18 Mar 2022 16:21:47 -0700
Subject: [PATCH] fix #5903

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

diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp
index d3ad54bd9..8535bf1e9 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.cpp
+++ b/src/muz/transforms/dl_mk_rule_inliner.cpp
@@ -437,6 +437,8 @@ namespace datalog {
                 tgt.add_rule(r);
                 continue;
             }
+
+            TRACE("dl", tout << pt_len
             modified = true;
 
             func_decl * pred = r->get_decl(i);
@@ -449,7 +451,7 @@ namespace datalog {
             }
         }
         if (modified) {
-            datalog::del_rule(m_mc, *r0, l_true);
+            datalog::del_rule(m_mc, *r0, l_undef);
         }
 
         return modified;