From d743e1b47c44b5f53d67952f9be327e7b5af1b3a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Feb 2024 19:11:35 -0800 Subject: [PATCH] add note that the encoding is a first approximation Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 62b55908a66..7f44cdbcd2f 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -3163,6 +3163,7 @@ namespace nlsat { if (a.i() == 1 && m_pm.degree(a.p(), a.x()) == 1) return display_linear_root_smt2(out, a, proc); #if 1 + // A first approximation: this encoding assumes roots are distinct out << "(exists ("; for (unsigned j = 0; j < a.i(); ++j) { std::string y = std::string("y") + std::to_string(j);