From c54627bebde673b8b4d08ee8909a58a75cd7df14 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 30 Oct 2011 18:37:42 +0100
Subject: [PATCH] Avoid containment checks on equal formulae.

* src/ltlvisit/contain.cc
(language_containment_checker::contained,
language_containment_checker::neg_contained,
language_containment_checker::contained_neg): Detect
cases where both formulae are equal.
---
 src/ltlvisit/contain.cc | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc
index e11dbcf64..cd05ed706 100644
--- a/src/ltlvisit/contain.cc
+++ b/src/ltlvisit/contain.cc
@@ -89,6 +89,8 @@ namespace spot
     bool
     language_containment_checker::contained(const formula* l, const formula* g)
     {
+      if (l == g)
+	return true;
       record_* rl = register_formula_(l);
       const formula* ng = unop::instance(unop::Not, g->clone());
       record_* rng = register_formula_(ng);
@@ -101,12 +103,16 @@ namespace spot
     language_containment_checker::neg_contained(const formula* l,
 						const formula* g)
     {
+      if (l == g)
+	return false;
       const formula* nl = unop::instance(unop::Not, l->clone());
       record_* rnl = register_formula_(nl);
       const formula* ng = unop::instance(unop::Not, g->clone());
       record_* rng = register_formula_(ng);
       nl->destroy();
       ng->destroy();
+      if (nl == g)
+	return true;
       return incompatible_(rnl, rng);
     }
 
@@ -115,6 +121,8 @@ namespace spot
     language_containment_checker::contained_neg(const formula* l,
 						const formula* g)
     {
+      if (l == g)
+	return false;
       record_* rl = register_formula_(l);
       record_* rg = register_formula_(g);
       return incompatible_(rl, rg);