diff --git a/src/nlsat/nlsat_clause.h b/src/nlsat/nlsat_clause.h
index c8cf4ae06..91467303c 100644
--- a/src/nlsat/nlsat_clause.h
+++ b/src/nlsat/nlsat_clause.h
@@ -64,7 +64,7 @@ namespace nlsat {
         assumption_set assumptions() const { return m_assumptions; }
     };
 
-    typedef std_vector<clause*> clause_vector;
+    typedef ptr_vector<clause> clause_vector;
 
 };
 
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index d5a5018b8..dc6f388e5 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -804,7 +804,7 @@ namespace nlsat {
             del_clause(cls);
         }
 
-        void del_clauses(std_vector<clause*> & cs) {
+        void del_clauses(clause_vector & cs) {
             for (clause* cp : cs) 
                 del_clause(cp);
             cs.clear();