mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity

relations with no columns are not always non-empty.

Browse source 
fix that in the udoc datalog backend

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2014-09-25 16:27:20 +01:00
parent aaa931e0d5
commit b7397b6967
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/udoc_relation.cpp
View file

@ -63,7 +63,7 @@ namespace datalog {
m_elems.push_back(fact2doc(f));
}
bool udoc_relation::empty() const {
if (get_signature().empty()) return false;
if (m_elems.is_empty()) return true;
// TBD: make this a complete check
for (unsigned i = 0; i < m_elems.size(); ++i) {
if (!dm.is_empty(m_elems[i])) return false;