From 941475fbdb303f5a4bdf1a5ca2b2f9cf88bfaf4e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 2 Sep 2024 17:28:28 +0200
Subject: [PATCH] fix spurious g++-14 warning

* spot/twaalgos/mealy_machine.cc (mm_sat_prob_t<true>::get_sol): Here.
---
 spot/twaalgos/mealy_machine.cc | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc
index e63193cdc..5021f2a94 100644
--- a/spot/twaalgos/mealy_machine.cc
+++ b/spot/twaalgos/mealy_machine.cc
@@ -2604,9 +2604,14 @@ namespace
           return {};
         case PICOSAT_SATISFIABLE:
           {
-            std::vector<int>
-                res(1 + (unsigned) picosat_variables(lm.psat_), -1);
-            SPOT_ASSUME(res.data()); // g++ 11 believes data might be nullptr
+            unsigned nvar = 1 + (unsigned) picosat_variables(lm.psat_);
+            // Asssuming res.data() non-null was enough to prevent g++
+            // 11 from issuing a spurious "potential null pointer
+            // dereference" on the res[0] assignment.  Since g++14 we
+            // also need to assume nvar>0.
+            SPOT_ASSUME(nvar > 0);
+            std::vector<int> res(nvar, -1);
+            SPOT_ASSUME(res.data());
             res[0] = 0; // Convention
             for (int lit : lm.all_lits)
               res[lit] = picosat_deref(lm.psat_, lit);