From 4f9ef6c275462d0c839fc56ee96f2dc851fbe868 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 12 Jun 2026 03:55:49 +0000
Subject: [PATCH] docs(java): clarify SAT model non-canonical behavior in
 Solver#getModel

---
 src/api/java/Solver.java | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 0f3023b50..af9e2c0ba 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -289,7 +289,11 @@ public class Solver extends Z3Object {
      * Remarks:  The result is
      * {@code null} if {@code Check} was not invoked before, if its
      * results was not {@code SATISFIABLE}, or if model production is not
-     * enabled. 
+     * enabled.
+     * For satisfiable formulas with multiple solutions, the returned model is
+     * not canonical: different solver runs (including runs in parallel on
+     * separate {@code Context} objects) may produce different satisfying
+     * models.
      * 
      * @throws Z3Exception
      **/