diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp
index 11fb6a964..1f7588655 100644
--- a/src/math/polysat/univariate/univariate_solver.cpp
+++ b/src/math/polysat/univariate/univariate_solver.cpp
@@ -26,11 +26,20 @@ namespace polysat {
 
     class univariate_bitblast_solver : public univariate_solver {
         ast_manager m;
+        bv_util bv;
         scoped_ptr<solver> s;
+        unsigned bit_width;
+        func_decl* x_decl;
 
     public:
-        univariate_bitblast_solver(solver_factory& mk_solver) {
+        univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) :
+            bv(m),
+            bit_width(bit_width)
+        {
             s = mk_solver(m, params_ref::get_empty(), false, true, true, symbol::null);
+            // auto s = bv.mk_sort(bit_width);
+            // auto n = bv.mk_numeral(rational(123), bit_width);
+            x_decl = m.mk_const_decl("x", bv.mk_sort(bit_width));
         }
 
         ~univariate_bitblast_solver() override = default;
@@ -43,9 +52,17 @@ namespace polysat {
             s->pop(n);
         }
 
-        void add_ule(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
-            // s->assert_expr();
+        expr* mk_poly(univariate p) {
             NOT_IMPLEMENTED_YET();
+            return nullptr;
+        }
+
+        void add_ule(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
+            expr* e = bv.mk_ule(mk_poly(lhs), mk_poly(rhs));
+            if (sign)
+                e = m.mk_not(e);
+            // TODO: record dep, and pass second argument to assert_expr (for tracking in the unsat core)
+            s->assert_expr(e);
         }
 
         void add_umul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
@@ -77,8 +94,14 @@ namespace polysat {
             SASSERT(s->status() == l_true);
             model_ref model;
             s->get_model(model);
-            NOT_IMPLEMENTED_YET();
-            return {};
+            expr* val_expr = model->get_const_interp(x_decl);
+            SASSERT(val_expr->get_kind() == AST_APP);
+            app* val = static_cast<app*>(val_expr);
+            SASSERT(val->get_kind() == OP_BV_NUM);
+            SASSERT(val->get_num_parameters() == 2);
+            auto const& p = val->get_parameter(0);
+            SASSERT(p.is_rational());
+            return p.get_rational();
         }
     };
 
@@ -94,8 +117,8 @@ namespace polysat {
 
         ~univariate_bitblast_factory() override = default;
 
-        scoped_ptr<univariate_solver> operator()() override {
-            return alloc(univariate_bitblast_solver, *sf);
+        scoped_ptr<univariate_solver> operator()(unsigned bit_width) override {
+            return alloc(univariate_bitblast_solver, *sf, bit_width);
         }
     };
 
diff --git a/src/math/polysat/univariate/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h
index b404d1603..b5b302620 100644
--- a/src/math/polysat/univariate/univariate_solver.h
+++ b/src/math/polysat/univariate/univariate_solver.h
@@ -50,7 +50,7 @@ namespace polysat {
     class univariate_solver_factory {
     public:
         virtual ~univariate_solver_factory();
-        virtual scoped_ptr<univariate_solver> operator()() = 0;
+        virtual scoped_ptr<univariate_solver> operator()(unsigned bit_width) = 0;
     };
 
     scoped_ptr<univariate_solver_factory> mk_univariate_bitblast_factory();