From 4b2e5ecca0b63a9ab3cfc12fb49f1e93cc83deea Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Apr 2020 17:34:18 -0700
Subject: [PATCH] fix #3797

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/rel/dl_mk_explanations.cpp | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index f4ab9d521..d1567c89b 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -456,11 +456,15 @@ namespace datalog {
               m_col_idx(col_idx), 
               m_new_rule(std::move(new_rule)) {}
 
+        void not_handled() {
+            throw default_exception("explanations are not supported with undefined predicates");
+        }
+
         void operator()(relation_base & r0) override {
             explanation_relation & r = static_cast<explanation_relation &>(r0);
 
             if (!r.is_undefined(m_col_idx)) {
-                throw default_exception("explanations are not supported with undefined predicates");
+                not_handled();
             }
 
             unsigned sz = r.get_signature().size();
@@ -468,7 +472,8 @@ namespace datalog {
             subst_arg.resize(sz);
             unsigned ofs = sz-1;
             for (unsigned i=0; i<sz; i++) {
-                SASSERT(!r.is_undefined(i) || !contains_var(m_new_rule, i));
+                if (r.is_undefined(i) && contains_var(m_new_rule, i))
+                    not_handled();
                 subst_arg[ofs-i] = r.m_data.get(i);
             }
             expr_ref res = m_subst(m_new_rule, subst_arg.size(), subst_arg.c_ptr());