mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 09:20:22 +00:00
Code Activity

datalog: fix compilation for rules like a(X) :- not b(X).

Browse source 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-01-29 20:41:22 +00:00
parent 4be2f608f1
commit 6017dcace3
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/rel/dl_compiler.cpp
View file

@ -857,7 +857,7 @@ namespace datalog {
ast_manager& m = m_context.get_manager(); ast_manager& m = m_context.get_manager();
unsigned pt_len = r->get_positive_tail_size(); unsigned pt_len = r->get_positive_tail_size();
unsigned ut_len = r->get_uninterpreted_tail_size(); unsigned ut_len = r->get_uninterpreted_tail_size();
if (pt_len == ut_len || pt_len == 0) { if (pt_len == ut_len) {
return; return;
} }
// populate negative variables: // populate negative variables: