From d0e139f2b3dc6878e6d33b20b14e89ea4513d955 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Thu, 13 Nov 2025 19:43:58 -1000
Subject: [PATCH] t

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

diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 4e19eb555..1816bc4c8 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -3685,6 +3685,11 @@ namespace nlsat {
                 out << "    (< " << y1 << " " << y2 << ")\n";
             }
 
+            auto y0 = mk_y_name(0);
+            out << "    (forall ((y Real)) (=> (< y " << y0 << ") (not (= ";
+            printer(out, "y");
+            out << " 0))))\n";
+
             for (unsigned j = 0; j + 1 < idx; ++j) {
                 auto y1 = mk_y_name(j);
                 auto y2 = mk_y_name(j + 1);