mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix #3797

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-06 17:34:18 -07:00
parent 4792ee8110
commit 4b2e5ecca0
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -456,11 +456,15 @@ namespace datalog {
m_col_idx(col_idx), m_col_idx(col_idx),
m_new_rule(std::move(new_rule)) {} 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 { void operator()(relation_base & r0) override {
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)) {
throw default_exception("explanations are not supported with undefined predicates"); not_handled();
} }
unsigned sz = r.get_signature().size(); unsigned sz = r.get_signature().size();
@ -468,7 +472,8 @@ namespace datalog {
subst_arg.resize(sz); subst_arg.resize(sz);
unsigned ofs = sz-1; unsigned ofs = sz-1;
for (unsigned i=0; i<sz; i++) { 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); subst_arg[ofs-i] = r.m_data.get(i);
} }
expr_ref res = m_subst(m_new_rule, subst_arg.size(), subst_arg.c_ptr()); expr_ref res = m_subst(m_new_rule, subst_arg.size(), subst_arg.c_ptr());