diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h
index 901f4ee61..79b6361b5 100644
--- a/src/math/polysat/viable.h
+++ b/src/math/polysat/viable.h
@@ -16,12 +16,18 @@ Author:
 
 #include <limits>
 #include "math/dd/dd_bdd.h"
+#include "math/interval/mod_interval.h"
 #include "math/polysat/types.h"
 
 namespace polysat {
 
     class solver;
 
+    class viable_values : public mod_interval<rational> {
+
+
+    };
+
     class viable {
         typedef dd::bdd bdd;
         solver& s;
diff --git a/src/muz/rel/CMakeLists.txt b/src/muz/rel/CMakeLists.txt
index f03a90406..1129b6dd9 100644
--- a/src/muz/rel/CMakeLists.txt
+++ b/src/muz/rel/CMakeLists.txt
@@ -23,7 +23,6 @@ z3_add_component(rel
     doc.cpp
     karr_relation.cpp
     rel_context.cpp
-    tbv.cpp
     udoc_relation.cpp
   COMPONENT_DEPENDENCIES
     muz
diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 0b7800905..fbe6b1f61 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -695,12 +695,36 @@ void doc_manager::check_equiv(ast_manager& m, expr* fml1, expr* fml2) {
     SASSERT(res == l_false);
 }
 
+
+expr_ref doc_manager::to_formula(ast_manager & m, tbv const& src) {
+    expr_ref result(m);
+    expr_ref_vector conj(m);
+    for (unsigned i = 0; i < num_tbits(); ++i) {
+        switch (src[i]) {
+        case BIT_0:
+            conj.push_back(m.mk_not(m.mk_const(symbol(i), m.mk_bool_sort())));
+            break;
+        case BIT_1:
+            conj.push_back(m.mk_const(symbol(i), m.mk_bool_sort()));
+            break;
+        default:
+            break;            
+        }        
+    }
+    result = mk_and(m, conj.size(), conj.data());
+    return result;    
+}
+
+expr_ref doc_manager::mk_var(ast_manager & m, unsigned i) {
+    return expr_ref(m.mk_const(symbol(i), m.mk_bool_sort()), m);    
+}
+
 expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) {
     expr_ref result(m);
     expr_ref_vector conj(m);
-    conj.push_back(tbvm().to_formula(m, src.pos()));
+    conj.push_back(to_formula(m, src.pos()));
     for (unsigned i = 0; i < src.neg().size(); ++i) {
-        conj.push_back(m.mk_not(tbvm().to_formula(m, src.neg()[i])));
+        conj.push_back(m.mk_not(to_formula(m, src.neg()[i])));
     }
     result = mk_and(m, conj.size(), conj.data());
     return result;
@@ -712,9 +736,9 @@ void doc_manager::project_expand(expr_ref& fml, bit_vector const& to_delete) {
     for (unsigned i = 0; i < num_tbits(); ++i) {
         if (to_delete.get(i)) {
             expr_safe_replace rep1(m), rep2(m);
-            rep1.insert(tbvm().mk_var(m, i), m.mk_true());
+            rep1.insert(mk_var(m, i), m.mk_true());
             rep1(fml, tmp1);
-            rep2.insert(tbvm().mk_var(m, i), m.mk_false());
+            rep2.insert(mk_var(m, i), m.mk_false());
             rep2(fml, tmp2);
             if (tmp1 == tmp2) {
                 fml = tmp1;
@@ -731,7 +755,7 @@ void doc_manager::project_rename(expr_ref& fml, bit_vector const& to_delete) {
     expr_safe_replace rep(m);
     for (unsigned i = 0, j = 0; i < num_tbits(); ++i) {
         if (!to_delete.get(i)) {
-            rep.insert(tbvm().mk_var(m, j), tbvm().mk_var(m, i));
+            rep.insert(mk_var(m, j), mk_var(m, i));
             ++j;
         }
     }
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index 10120ce8b..b56947e2e 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -22,7 +22,7 @@ Revision History:
 
 #pragma once
 
-#include "muz/rel/tbv.h"
+#include "util/tbv.h"
 #include "util/union_find.h"
 #include "util/buffer.h"
 
@@ -101,6 +101,8 @@ private:
     void project_rename(expr_ref& fml, bit_vector const& to_delete);
     void project_expand(expr_ref& fml, bit_vector const& to_delete);
     expr_ref to_formula(ast_manager& m, doc const& src);
+    expr_ref to_formula(ast_manager& m, tbv const& src);
+    expr_ref mk_var(ast_manager& m, unsigned i);
     void check_equiv(ast_manager& m, expr* fml1, expr* fml2);
 };
 
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 35727bce2..c2a7e8296 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -54,6 +54,7 @@ z3_add_component(util
     state_graph.cpp
     statistics.cpp
     symbol.cpp
+    tbv.cpp
     timeit.cpp
     timeout.cpp
     trace.cpp
diff --git a/src/muz/rel/tbv.cpp b/src/util/tbv.cpp
similarity index 91%
rename from src/muz/rel/tbv.cpp
rename to src/util/tbv.cpp
index 289e43b4e..13615b549 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/util/tbv.cpp
@@ -18,7 +18,7 @@ Revision History:
 
 --*/
 
-#include "muz/rel/tbv.h"
+#include "util/tbv.h"
 #include "util/hashtable.h"
 #include "ast/ast_util.h"
 
@@ -301,26 +301,3 @@ std::ostream& tbv_manager::display(std::ostream& out, tbv const& b) const {
     if (num_tbits() == 0) return out << "[]";
     return display(out, b, num_tbits()-1, 0);
 }
-
-expr_ref tbv_manager::to_formula(ast_manager& m, tbv const& src) {
-    expr_ref result(m);
-    expr_ref_vector conj(m);
-    for (unsigned i = 0; i < num_tbits(); ++i) {
-        switch (src[i]) {
-        case BIT_0:
-            conj.push_back(m.mk_not(m.mk_const(symbol(i), m.mk_bool_sort())));
-            break;
-        case BIT_1:
-            conj.push_back(m.mk_const(symbol(i), m.mk_bool_sort()));
-            break;
-        default:
-            break;
-        }
-    }
-    result = mk_and(m, conj.size(), conj.data());
-    return result;
-}
-
-expr_ref tbv_manager::mk_var(ast_manager& m, unsigned i) {
-    return expr_ref(m.mk_const(symbol(i), m.mk_bool_sort()), m);
-}
diff --git a/src/muz/rel/tbv.h b/src/util/tbv.h
similarity index 97%
rename from src/muz/rel/tbv.h
rename to src/util/tbv.h
index a8aaea234..2fe00c2a1 100644
--- a/src/muz/rel/tbv.h
+++ b/src/util/tbv.h
@@ -21,6 +21,7 @@ Revision History:
 #pragma once
 
 #include "util/fixed_bit_vector.h"
+#include "util/bit_vector.h"
 #include "util/rational.h"
 #include "ast/ast.h"
 
@@ -84,10 +85,7 @@ public:
     void set(tbv& dst, tbv const& other, unsigned hi, unsigned lo);
     void set(tbv& dst, unsigned index, tbit value);
 
-
     static void debug_alloc();
-    expr_ref to_formula(ast_manager& m, tbv const& src);
-    expr_ref mk_var(ast_manager& m, unsigned i);
 };
 
 class tbv: private fixed_bit_vector {