From 6ed0830f87f6fad09896975ec1250effb90e8279 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 7 Aug 2016 19:45:01 +0200
Subject: [PATCH] fix two minor issues reported by clang-analyzer

These are actually two events that should never happen, but let's just
make sure they do not.

* spot/tl/formula.cc: Add an assert.
* spot/twaalgos/emptiness.cc: Add an exception.
---
 spot/tl/formula.cc         | 3 ++-
 spot/twaalgos/emptiness.cc | 3 ++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc
index 0ca67bb1e..09460762d 100644
--- a/spot/tl/formula.cc
+++ b/spot/tl/formula.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2015 Laboratoire de Recherche et Développement de
+// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -423,6 +423,7 @@ namespace spot
             {
               for (i = v.begin(); i != v.end(); ++i)
                 (*i)->destroy();
+              assert(abs);
               return abs->clone();
             }
           else
diff --git a/spot/twaalgos/emptiness.cc b/spot/twaalgos/emptiness.cc
index 07cbe2716..33552a572 100644
--- a/spot/twaalgos/emptiness.cc
+++ b/spot/twaalgos/emptiness.cc
@@ -816,8 +816,9 @@ namespace spot
               }
             s2->destroy();
           }
-        assert(res);
         s->destroy();
+        if (!the_next)
+          throw std::runtime_error("twa_run::as_twa() unable to replay run");
         s = the_next;