mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 04:31:24 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-04-28 12:51:58 -07:00
commit 160a448823
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/dl_rule.cpp
View file

@ -202,7 +202,7 @@ namespace datalog {
unsigned index = extract_horn(fml, m_body, m_head); unsigned index = extract_horn(fml, m_body, m_head);
hoist_compound_predicates(index, m_head, m_body); hoist_compound_predicates(index, m_head, m_body);
TRACE("dl_rule", TRACE("dl_rule",
tout << mk_pp(head, m) << " :- "; tout << mk_pp(m_head, m) << " :- ";
for (unsigned i = 0; i < m_body.size(); ++i) { for (unsigned i = 0; i < m_body.size(); ++i) {
tout << mk_pp(m_body[i].get(), m) << " "; tout << mk_pp(m_body[i].get(), m) << " ";
} }