diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt
index 14bcebf46..47323d821 100644
--- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt
+++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt
@@ -4,6 +4,7 @@ z3_add_component(rewriter
     array_rewriter.cpp
     ast_counter.cpp
     bool_rewriter.cpp
+    bv_bounds.cpp
     bv_rewriter.cpp
     datatype_rewriter.cpp
     der.cpp
diff --git a/contrib/cmake/src/tactic/bv/CMakeLists.txt b/contrib/cmake/src/tactic/bv/CMakeLists.txt
index b39d77a0a..90ed65e3f 100644
--- a/contrib/cmake/src/tactic/bv/CMakeLists.txt
+++ b/contrib/cmake/src/tactic/bv/CMakeLists.txt
@@ -5,6 +5,7 @@ z3_add_component(bv_tactics
     bv1_blaster_tactic.cpp
     bvarray2uf_rewriter.cpp
     bvarray2uf_tactic.cpp
+    bv_bound_chk_tactic.cpp
     bv_bounds_tactic.cpp
     bv_size_reduction_tactic.cpp
     dt2bv_tactic.cpp
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index a90d420cb..08fc0b9d7 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -303,6 +303,7 @@ namespace datalog {
     bool context::karr() const { return m_params->xform_karr(); }
     bool context::scale() const { return m_params->xform_scale(); }
     bool context::magic() const { return m_params->xform_magic(); }
+    bool context::compress_unbound() const { return m_params->xform_compress_unbound(); }
     bool context::quantify_arrays() const { return m_params->xform_quantify_arrays(); }
     bool context::instantiate_quantifiers() const { return m_params->xform_instantiate_quantifiers(); }
 
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 3d8b56beb..3c1a7bfaa 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -272,6 +272,7 @@ namespace datalog {
         bool karr() const;
         bool scale() const;
         bool magic() const;
+        bool compress_unbound() const;
         bool quantify_arrays() const;
         bool instantiate_quantifiers() const;
         bool xform_bit_blast() const;        
diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index 86cfb30ac..8e7d6a7cb 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -131,6 +131,7 @@ def_module_params('fixedpoint',
                           ('xform.inline_eager', BOOL, True, "try eager inlining of rules"),
                           ('xform.inline_linear_branch', BOOL, False, 
                            "try linear inlining method with potential expansion"),
+                          ('xform.compress_unbound', BOOL, True, "compress tails with unbound variables"),
                           ('xform.fix_unbound_vars', BOOL, False, "fix unbound variables in tail"),
                           ('xform.unfold_rules', UINT, 0, 
                            "unfold rules statically using iterative squarring"),
diff --git a/src/muz/transforms/dl_mk_unbound_compressor.cpp b/src/muz/transforms/dl_mk_unbound_compressor.cpp
index 7d103568a..41b181450 100644
--- a/src/muz/transforms/dl_mk_unbound_compressor.cpp
+++ b/src/muz/transforms/dl_mk_unbound_compressor.cpp
@@ -344,6 +344,11 @@ namespace datalog {
 
     rule_set * mk_unbound_compressor::operator()(rule_set const & source) {
         // TODO mc
+
+        if (!m_context.compress_unbound()) {
+            return 0;
+        }
+
         m_modified = false;
 
         SASSERT(m_rules.empty());