mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +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:36:26 -07:00
parent 4b2e5ecca0
commit 2b929cb31e
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

@ -800,9 +800,9 @@ namespace datalog {
SASSERT(prod_rel.size()==2); SASSERT(prod_rel.size()==2);
if (!prod_rel[0].get_plugin().is_sieve_relation()) 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()) 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[] = { sieve_relation * srels[] = {
static_cast<sieve_relation *>(&prod_rel[0]), static_cast<sieve_relation *>(&prod_rel[0]),
static_cast<sieve_relation *>(&prod_rel[1]) }; static_cast<sieve_relation *>(&prod_rel[1]) };