From 644342f5d4da1ffc90eb047d05cc3cbaca69f283 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 3 Oct 2021 00:48:38 +0200
Subject: [PATCH] simplify: fix some discrepancies between Intel and ARM

* spot/tl/simplify.cc (tl_simplifier_cache::as_bdd): Fix the order in
which as_bdd() is called recursively in binary nodes, do not let the
choice to the compiler.
* tests/core/ltlsynt.test: Adjust expected output.
---
 spot/tl/simplify.cc     | 32 +++++++++++++++++++++++---------
 tests/core/ltlsynt.test |  4 ++--
 2 files changed, 25 insertions(+), 11 deletions(-)

diff --git a/spot/tl/simplify.cc b/spot/tl/simplify.cc
index 1a7f179b3..3a2433197 100644
--- a/spot/tl/simplify.cc
+++ b/spot/tl/simplify.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2011-2020 Laboratoire de Recherche et Developpement
+// Copyright (C) 2011-2021 Laboratoire de Recherche et Developpement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -125,14 +125,23 @@ namespace spot
           result = !as_bdd(f[0]);
           break;
         case op::Xor:
-          result = bdd_apply(as_bdd(f[0]), as_bdd(f[1]), bddop_xor);
-          break;
+          {
+            bdd l = as_bdd(f[0]);
+            result = bdd_apply(l, as_bdd(f[1]), bddop_xor);
+            break;
+          }
         case op::Implies:
-          result = bdd_apply(as_bdd(f[0]), as_bdd(f[1]), bddop_imp);
-          break;
+          {
+            bdd l = as_bdd(f[0]);
+            result = bdd_apply(l, as_bdd(f[1]), bddop_imp);
+            break;
+          }
         case op::Equiv:
-          result = bdd_apply(as_bdd(f[0]), as_bdd(f[1]), bddop_biimp);
-          break;
+          {
+            bdd l = as_bdd(f[0]);
+            result = bdd_apply(l, as_bdd(f[1]), bddop_biimp);
+            break;
+          }
         case op::And:
           {
             result = bddtrue;
@@ -4038,9 +4047,14 @@ namespace spot
     bool result;
 
     if (f.is_boolean() && g.is_boolean())
-      result = bdd_implies(as_bdd(f), as_bdd(g));
+      {
+        bdd l = as_bdd(f);
+        result = bdd_implies(l, as_bdd(g));
+      }
     else
-      result = syntactic_implication_aux(f, g);
+      {
+        result = syntactic_implication_aux(f, g);
+      }
 
     // Cache result
     {
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index 1cd3455a6..9a8582d84 100644
--- a/tests/core/ltlsynt.test
+++ b/tests/core/ltlsynt.test
@@ -522,13 +522,13 @@ REALIZABLE
 HOA: v1
 States: 1
 Start: 0
-AP: 3 "b" "c" "a"
+AP: 3 "a" "b" "c"
 acc-name: all
 Acceptance: 0 t
 properties: trans-labels explicit-labels state-acc deterministic
 --BODY--
 State: 0
-[!0&!1 | !1&!2] 0
+[!0&!2 | !1&!2] 0
 [0&1&2] 0
 --END--
 EOF