diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp index 927eed283..4f950973c 100644 --- a/src/muz/rel/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -480,7 +480,7 @@ bool doc_manager::contains(doc const& a, doc const& b) const { for (unsigned i = 0; i < a.neg().size(); ++i) { bool found = false; for (unsigned j = 0; !found && j < b.neg().size(); ++j) { - found = m.contains(b.neg()[i],a.neg()[j]); + found = m.contains(b.neg()[j],a.neg()[i]); } if (!found) return false; } diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 205d52416..2f4cd2801 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -887,6 +887,7 @@ namespace datalog { u.intersect(dm, m_udoc); SASSERT(u.well_formed(dm)); if (m_condition && !u.is_empty()) { + std::cout << "Apply: " << m_condition << "\n"; t.apply_guard(m_condition, u, m_equalities, m_empty_bv); SASSERT(u.well_formed(dm)); }