diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp
index c5beb5ab2..f17d4a735 100644
--- a/src/math/polysat/univariate/univariate_solver.cpp
+++ b/src/math/polysat/univariate/univariate_solver.cpp
@@ -144,6 +144,10 @@ namespace polysat {
             add(bv->mk_ule(mk_numeral(val), x), sign, dep);
         }
 
+        void add_bit(unsigned idx, bool sign, dep_t dep) override {
+            add(bv->mk_bit2bool(x, idx), sign, dep);
+        }
+
         lbool check() override {
             return s->check_sat();
         }
diff --git a/src/math/polysat/univariate/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h
index 0a19081ed..65bc9c65a 100644
--- a/src/math/polysat/univariate/univariate_solver.h
+++ b/src/math/polysat/univariate/univariate_solver.h
@@ -63,8 +63,8 @@ namespace polysat {
         void add_ugt_const(rational const& val, bool sign, dep_t dep) { add_ule_const(val, !sign, dep); }
         void add_ult_const(rational const& val, bool sign, dep_t dep) { add_uge_const(val, !sign, dep); }
 
-        // TODO: assert bit; use bv->mk_bit2bool(x, idx)
-        // virtual void add_bit(unsigned idx, bool sign, dep_t dep);
+        /// Assert i-th bit of x
+        virtual void add_bit(unsigned idx, bool sign, dep_t dep) = 0;
 
         virtual std::ostream& display(std::ostream& out) const = 0;
     };