From 9116d386284a99ebbcfceb0e902b43c1298a8556 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 18 Sep 2014 06:07:03 -0700
Subject: [PATCH] doc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/ddnf/tbv.cpp | 10 +++++-----
 src/test/doc.cpp     | 12 ++++++++++--
 2 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/src/muz/ddnf/tbv.cpp b/src/muz/ddnf/tbv.cpp
index b1e5d5344..371233590 100644
--- a/src/muz/ddnf/tbv.cpp
+++ b/src/muz/ddnf/tbv.cpp
@@ -130,15 +130,15 @@ void tbv_manager::copy(tbv& dst, tbv const& src) const {
     m.copy(dst, src);
 }    
 tbv& tbv_manager::fill0(tbv& bv) const { 
-    // 01010101 = 1 + 4 + 16 + 64
-    memset(bv.m_data, 1 + 4 + 16 + 64, m.num_bytes());
-    return bv; 
-}
-tbv& tbv_manager::fill1(tbv& bv) const { 
     // 10101010 = 2 + 8 + 32 + 128
     memset(bv.m_data, 2 + 8 + 32 + 128, m.num_bytes());
     return bv; 
 }
+tbv& tbv_manager::fill1(tbv& bv) const {  
+    // 01010101 = 1 + 4 + 16 + 64
+    memset(bv.m_data, 1 + 4 + 16 + 64, m.num_bytes());
+    return bv; 
+}
 tbv& tbv_manager::fillX(tbv& bv) const { 
     m.fill1(bv); 
     return bv; 
diff --git a/src/test/doc.cpp b/src/test/doc.cpp
index 9d37654af..ea5202efe 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -13,6 +13,11 @@ static void tst_doc1(unsigned n) {
     doc_ref dXc(m, m.allocate(*dX));
     doc_ref d10(m, m.allocate(10));
     doc_ref d20(m, m.allocate(rational(20)));
+    m.display(std::cout, *d1) << "\n";
+    m.display(std::cout, *d0) << "\n";
+    m.display(std::cout, *dX) << "\n";
+    m.display(std::cout, *d10) << "\n";
+    m.display(std::cout, *d20) << "\n";
     unsigned hi = 3, lo = 1;
     SASSERT(hi <= n);
     doc_ref d111X(m, m.allocate(0xFF, hi, lo));
@@ -39,8 +44,11 @@ static void tst_doc1(unsigned n) {
     VERIFY(m.fold_neg(*dX));
     ptr_vector<doc> result;
     //    VERIFY(!m.intersect(*d1,*d0, result));    
-    m.subtract(*d1,*d0, result);
+    //    m.subtract(*d1,*d0, result);
     SASSERT(result.empty());
+    dX = m.allocateX();
+    m.display(std::cout, *d0) << "\n";
+    m.display(std::cout, *dX) << "\n";
     SASSERT(m.contains(*dX,*d1));
     SASSERT(m.contains(*dX,*d0));
     SASSERT(!m.contains(*d0,*d1));
@@ -53,7 +61,7 @@ static void tst_doc1(unsigned n) {
     m.display(std::cout, *d1) << "\n";
 
 
-    svector<bool> to_delete(n);
+    svector<bool> to_delete(n, false);
     to_delete[1] = true;
     to_delete[3] = true;
     doc_manager m1(n-2);