diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp
index 8d136a4e3..3f867f9cc 100644
--- a/src/math/polysat/clause_builder.cpp
+++ b/src/math/polysat/clause_builder.cpp
@@ -60,7 +60,6 @@ namespace polysat {
 
     void clause_builder::push(signed_constraint c) {
         SASSERT(c);
-        SASSERT(c->has_bvar());
         if (c.is_always_false())  // filter out trivial constraints such as "4 < 2"
             return;
         if (c.is_always_true()) {
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index 9126b9c77..acf738580 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -47,6 +47,7 @@ namespace polysat {
 
     class constraint {
         friend class constraint_manager;
+        friend class signed_constraint;
         friend class clause;
         friend class ule_constraint;
         friend class umul_ovfl_constraint;
@@ -58,14 +59,13 @@ namespace polysat {
         lbool               m_external_sign = l_undef;
         bool                m_is_active = false;
         bool                m_is_pwatched = false;
-        /** The boolean variable associated to this constraint, if any.
-         *  If this is not null_bool_var, then the constraint corresponds to a literal on the assignment stack.
-         *  Convention: the plain constraint corresponds the positive sat::literal.
-         */
+        /** The boolean variable associated to this constraint */
         sat::bool_var       m_bvar = sat::null_bool_var;
 
         constraint(constraint_manager& m, ckind_t k): m_kind(k) {}
 
+        bool has_bvar() const { return m_bvar != sat::null_bool_var; }
+
     public:
         virtual ~constraint() {}
 
@@ -104,7 +104,6 @@ namespace polysat {
         unsigned_vector const& vars() const { return m_vars; }
         unsigned var(unsigned idx) const { return m_vars[idx]; }
         bool contains_var(pvar v) const { return m_vars.contains(v); }
-        bool has_bvar() const { return m_bvar != sat::null_bool_var; }
         sat::bool_var bvar() const { SASSERT(has_bvar()); return m_bvar; }
         std::string bvar2string() const;
         unsigned level(solver& s) const;
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index c211d5c01..7c3346d56 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1245,8 +1245,6 @@ namespace polysat {
             if (m_search[i].is_boolean())
                 skip.insert(m_search[i].lit().var());
         for (auto c : m_constraints) {
-            if (!c->has_bvar())
-                continue;
             if (skip.contains(c->bvar()))
                 continue;