diff --git a/src/sanity/style.test b/src/sanity/style.test
index 33416b6da..dfa58e4d6 100755
--- a/src/sanity/style.test
+++ b/src/sanity/style.test
@@ -246,7 +246,8 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do
       grep '[^a-zA-Z0-9_](\*[a-zA-Z0-9_]*)\.' $tmp &&
 	diag 'Use "x->y", not "(*x).y"'
 
-      egrep 'bdd_(false|true)[	]*\(' $tmp &&
+      # we allow these functions only in ?...:...
+      egrep 'bdd_(false|true)[	]*\(' $tmp | grep -v '[?:]' &&
 	diag 'Use bddfalse and bddtrue instead of bdd_false() and bdd_true()'
 
       res=`perl -ne '$/ = undef;
diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc
index 067ad9046..d32e18fbd 100644
--- a/src/tgbaalgos/dtgbasat.cc
+++ b/src/tgbaalgos/dtgbasat.cc
@@ -768,8 +768,9 @@ namespace spot
 
 					    bdd f2 = p.acc_cand |
 					      d.all_cand_acc[f];
-					    bdd f2p = is_weak ? bddfalse
-					      : p.acc_ref | curacc;
+					    bdd f2p = bddfalse;
+					    if (!is_weak)
+					      f2p = p.acc_ref | curacc;
 
 					    path p2(p.src_cand, p.src_ref,
 						    q3, dp, f2, f2p);
diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc
index 5e5d37242..fb631ca2f 100644
--- a/src/tgbaalgos/eltl2tgba_lacim.cc
+++ b/src/tgbaalgos/eltl2tgba_lacim.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2012, 2013 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2010, 2012, 2013, 2014 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -195,7 +195,10 @@ namespace spot
 
 	// Update finish_ with finish(node).
 	// FIXME: when node is loop, it does not make sense; hence the bddtrue.
-	finish_[node] = !node->get_nfa()->is_loop() ? bddtrue : finish;
+	if (!node->get_nfa()->is_loop())
+	  finish_[node] = bddtrue;
+	else
+	  finish_[node] = finish;
 
 	bdd tmp = bddtrue;
 	for (nmap::iterator it = m.begin(); it != m.end(); ++it)
diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc
index 505a7d2c7..577c56377 100644
--- a/src/tgbaalgos/simulation.cc
+++ b/src/tgbaalgos/simulation.cc
@@ -470,8 +470,10 @@ namespace spot
 	    // simplifications in the signature by removing a
 	    // transition which has as a destination a state with
 	    // no outgoing transition.
-	    now_to_next[p.first] =
-	      (p.first == bddfalse) ? bddfalse : *it_bdd;
+	    bdd acc = bddfalse;
+	    if (p.first != bddfalse)
+	      acc = *it_bdd;
+	    now_to_next[p.first] = acc;
 	    ++it_bdd;
           }
 
@@ -650,15 +652,17 @@ namespace spot
 
 		    if (Cosimulation)
 		      {
-			gb->new_transition(dst.id(), src.id(),
-					   cond, Sba ? bddfalse : acc);
 			if (Sba)
-			  // acc should be attached to src, or rather,
-			  // in our transition-based representation)
-			  // to all transitions leaving src.  As we
-			  // can't do this here, store this in a table
-			  // so we can fix it later.
-			  accst[gb->get_state(src.id())] = acc;
+			  {
+			    // acc should be attached to src, or rather,
+			    // in our transition-based representation)
+			    // to all transitions leaving src.  As we
+			    // can't do this here, store this in a table
+			    // so we can fix it later.
+			    accst[gb->get_state(src.id())] = acc;
+			    acc = bddfalse;
+			  }
+			gb->new_transition(dst.id(), src.id(), cond, acc);
 		      }
 		    else
 		      {
diff --git a/src/tgbaalgos/tau03opt.cc b/src/tgbaalgos/tau03opt.cc
index 7365f6696..f4ab2d751 100644
--- a/src/tgbaalgos/tau03opt.cc
+++ b/src/tgbaalgos/tau03opt.cc
@@ -347,7 +347,7 @@ namespace spot
 		else if (c_prime.get_color() == CYAN &&
 			 (all_acc == ((use_red_weights ?
 				       (current_weight - c_prime.get_weight())
-				       : bddfalse)
+				       : bdd_false())
 				      | c_prime.get_acc()
 				      | acc
 				      | acu)))