mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 11:20:26 +00:00
Code Activity

fix #3798

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-06 17:06:17 -07:00
parent bfb26ecc6d
commit b2ba45448a
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz/rel/dl_mk_explanations.cpp
View file

@ -389,7 +389,7 @@ namespace datalog {
explanation_relation_plugin & plugin = tgt.get_plugin(); explanation_relation_plugin & plugin = tgt.get_plugin();
if (!src.no_undefined() || !tgt.no_undefined() || (delta && !delta->no_undefined())) { 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()) { if (src.empty()) {
return; return;
@ -460,7 +460,7 @@ namespace datalog {
explanation_relation & r = static_cast<explanation_relation &>(r0); explanation_relation & r = static_cast<explanation_relation &>(r0);
if (!r.is_undefined(m_col_idx)) { if (!r.is_undefined(m_col_idx)) {
UNREACHABLE(); throw default_exception("explanations are not supported with undefined predicates");
} }
unsigned sz = r.get_signature().size(); unsigned sz = r.get_signature().size();