From 9bb579c5c8bc9f16a5519527cfb524c5316ec125 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Apr 2020 19:43:32 -0700
Subject: [PATCH] fix #3814

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/rel/dl_base.cpp  |  4 +++-
 src/muz/rel/dl_table.cpp | 14 +++++++++-----
 2 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp
index 5dd21a9f0..572b689d5 100644
--- a/src/muz/rel/dl_base.cpp
+++ b/src/muz/rel/dl_base.cpp
@@ -366,7 +366,7 @@ namespace datalog {
      */
     table_base * table_base::complement(func_decl* p, const table_element * func_columns) const {
         const table_signature & sig = get_signature();
-        SASSERT(sig.functional_columns()==0 || func_columns!=0);
+        SASSERT(sig.functional_columns() == 0 || func_columns != 0);
         SASSERT(sig.first_functional() <= 1);
 
         table_base * res = get_plugin().mk_empty(sig);
@@ -377,6 +377,8 @@ namespace datalog {
 
         if (sig.first_functional() == 0) {
             if (empty()) {
+                if (fact.empty())
+                    throw default_exception("empty relations cannot be complemented");
                 res->add_fact(fact);
             }
             return res;
diff --git a/src/muz/rel/dl_table.cpp b/src/muz/rel/dl_table.cpp
index 71ffd88f3..054ac9360 100644
--- a/src/muz/rel/dl_table.cpp
+++ b/src/muz/rel/dl_table.cpp
@@ -260,7 +260,7 @@ namespace datalog {
     unsigned bitvector_table::fact2offset(const table_element* f) const {
         unsigned result = 0;
         for (unsigned i = 0; i < m_num_cols; ++i) {
-            SASSERT(f[i]<get_signature()[i]);
+            SASSERT(f[i] < get_signature()[i]);
             result +=  ((unsigned)f[i]) << m_shift[i];
         }
         return result;
@@ -274,15 +274,19 @@ namespace datalog {
     }
     
     void bitvector_table::add_fact(const table_fact & f) {
-        m_bv.set(fact2offset(f.c_ptr()));
+        if (m_num_cols > 0) {
+            m_bv.set(fact2offset(f.c_ptr()));
+        }
     }
 
-    void bitvector_table::remove_fact(const table_element* fact) {
-        m_bv.unset(fact2offset(fact));
+    void bitvector_table::remove_fact(const table_element* fact) {    
+        if (m_num_cols > 0) {
+            m_bv.unset(fact2offset(fact));
+        }
     }
 
     bool bitvector_table::contains_fact(const table_fact & f) const {
-        return m_bv.get(fact2offset(f.c_ptr()));
+        return !f.empty() && m_bv.get(fact2offset(f.c_ptr()));
     }
 
     table_base::iterator bitvector_table::begin() const {