diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp
index d8c0e23e8..65da19615 100644
--- a/src/math/polysat/boolean.cpp
+++ b/src/math/polysat/boolean.cpp
@@ -46,7 +46,7 @@ namespace polysat {
     }
 
     void bool_var_manager::del_var(sat::bool_var var) {
-        SASSERT(std::count(m_unused.begin(), m_unused.end(), var) == 0);
+        SASSERT(count(m_unused, var) == 0);
         auto lit = sat::literal(var);
         m_value[lit.index()]    = l_undef;
         m_value[(~lit).index()] = l_undef;
diff --git a/src/math/polysat/clause.h b/src/math/polysat/clause.h
index 4e652873b..4ce1e35bd 100644
--- a/src/math/polysat/clause.h
+++ b/src/math/polysat/clause.h
@@ -50,7 +50,7 @@ namespace polysat {
 
         clause(sat::literal_vector literals):
             m_literals(std::move(literals)) {
-            SASSERT(std::count(m_literals.begin(), m_literals.end(), sat::null_literal) == 0);
+            SASSERT(count(m_literals, sat::null_literal) == 0);
         }
 
     public:
@@ -69,6 +69,7 @@ namespace polysat {
         const_iterator begin() const { return m_literals.begin(); }
         const_iterator end() const { return m_literals.end(); }
 
+        // evaluates under pvar assignment
         bool is_always_false(solver& s) const;
         bool is_currently_false(solver& s) const;
 
diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 12b80088c..242996459 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -343,9 +343,9 @@ namespace polysat {
         //       resolvent: ~y \/ ~z \/ u \/ v; as core: y, z, ~u, ~v
 
         SASSERT(contains(lit));
-        SASSERT(std::count(cl.begin(), cl.end(), lit) > 0);
+        SASSERT(count(cl, lit) > 0);
         SASSERT(!contains(~lit));
-        SASSERT(std::count(cl.begin(), cl.end(), ~lit) == 0);
+        SASSERT(count(cl, ~lit) == 0);
 
         remove(s.lit2cnstr(lit));
         for (sat::literal other : cl)
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 67886cfff..8215f7500 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1195,7 +1195,7 @@ namespace polysat {
             int64_t num_watches = 0;
             signed_constraint sc(c, is_positive);
             for (auto const& wlist : m_pwatch) {
-                auto n = std::count(wlist.begin(), wlist.end(), c);
+                auto n = count(wlist, c);
                 if (n > 1)
                     std::cout << sc << "\n" << * this << "\n";
                 VERIFY(n <= 1);  // no duplicates in the watchlist
diff --git a/src/util/util.h b/src/util/util.h
index 273129307..d2a4771e9 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -384,3 +384,11 @@ bool all_of(Container const& c, Predicate f)
     using std::begin, std::end;  // allows begin(c) to also find c.begin()
     return std::all_of(begin(c), end(c), std::forward<Predicate>(f));
 }
+
+/** Compact version of std::count */
+template <typename Container, typename Item>
+std::size_t count(Container const& c, Item x)
+{
+    using std::begin, std::end;  // allows begin(c) to also find c.begin()
+    return std::count(begin(c), end(c), std::forward<Item>(x));
+}