From 2b929cb31e175a8e1df4680973dcb2c01eab826f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Apr 2020 17:36:26 -0700 Subject: [PATCH] fix #3797 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 d1567c89b..1c8250a75 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -800,9 +800,9 @@ namespace datalog { SASSERT(prod_rel.size()==2); if (!prod_rel[0].get_plugin().is_sieve_relation()) - throw default_exception("explanations are not supported for this query"); + throw default_exception("explanations are not supported with undefined predicates"); if (!prod_rel[1].get_plugin().is_sieve_relation()) - throw default_exception("explanations are not supported for this query"); + throw default_exception("explanations are not supported with undefined predicates"); sieve_relation * srels[] = { static_cast(&prod_rel[0]), static_cast(&prod_rel[1]) };