From e4897fff004706f178568d2537a1c93c7abc4891 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 27 Mar 2025 12:32:37 -0700
Subject: [PATCH] replace Exists by ForAll in the mathematica lemmas

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/nlsat/nlsat_solver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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]) {