diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index 86b421f68..9689ee1a8 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -105,21 +105,6 @@ namespace polysat {
         return *dynamic_cast<ule_constraint const*>(this);
     }
 
-#if 0
-    var_constraint& constraint::to_bit() {
-        return *dynamic_cast<var_constraint*>(this);
-    }
-
-    var_constraint const& constraint::to_bit() const {
-        return *dynamic_cast<var_constraint const*>(this);
-    }
-
-    constraint_ref constraint_manager::viable(unsigned lvl, csign_t sign, pvar v, bdd const& b, p_dependency_ref const& d) {
-        return alloc(var_constraint, *this, lvl, sign, v, b, d);
-    }
-
-#endif
-
     constraint_ref constraint_manager::eq(unsigned lvl, csign_t sign, pdd const& p, p_dependency_ref const& d) {
         return alloc(eq_constraint, *this, lvl, sign, p, d);
     }
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index be0f60060..7a8489863 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -30,7 +30,6 @@ namespace polysat {
     class clause;
     class scoped_clause;
     class eq_constraint;
-    // class var_constraint;
     class ule_constraint;
     using constraint_ref = ref<constraint>;
     using constraint_ref_vector = sref_vector<constraint>;
@@ -85,7 +84,6 @@ namespace polysat {
         friend class constraint_manager;
         friend class clause;
         friend class scoped_clause;
-        // friend class var_constraint;
         friend class eq_constraint;
         friend class ule_constraint;