diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index a501c89f4..98b9d7706 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -3736,7 +3736,7 @@ namespace nlsat {
                 }
             }
 
-            out << "Resolve[Exists[{";
+            out << "Resolve[ForAll[{";
             bool first = true;
             for (var x = 0; x < num_vars(); x++) {
                 if (used_vars[x]) {