From b2ba45448a7a2417e6ef1b06abed20d7538201e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Apr 2020 17:06:17 -0700 Subject: [PATCH] fix #3798 Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_mk_explanations.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index 73abd850d..f4ab9d521 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -389,7 +389,7 @@ namespace datalog { explanation_relation_plugin & plugin = tgt.get_plugin(); if (!src.no_undefined() || !tgt.no_undefined() || (delta && !delta->no_undefined())) { - UNREACHABLE(); + throw default_exception("explanations are not supported with undefined predicates"); } if (src.empty()) { return; @@ -460,7 +460,7 @@ namespace datalog { explanation_relation & r = static_cast(r0); if (!r.is_undefined(m_col_idx)) { - UNREACHABLE(); + throw default_exception("explanations are not supported with undefined predicates"); } unsigned sz = r.get_signature().size();