diff --git a/tests/core/basimul.test b/tests/core/basimul.test
index 68c253fb6..5b423d67a 100755
--- a/tests/core/basimul.test
+++ b/tests/core/basimul.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2013, 2014, 2017 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -22,9 +22,6 @@
 
 set -e
 
-ltl2tgba=ltl2tgba
-
-
 # This bug was found while working on the state-based acceptance
 # output for the LBTT format.  Using ba-simul=2 causes reverse
 # simulation to be applied to the BA automaton obtained after
@@ -60,15 +57,15 @@ ltlcross --seed=0 --products=5 --json=out.json \
     -f '!p2 & (Fp5 R (((p0 U p1) & (p5 | p1)) | (!p5 & (!p0 R !p1))))' \
     -f '! ((p0 /\ p4) <-> ! ((! p0 U (p0 W p4)) /\ (X p5 -> ([] p3 /\ p5))))' \
     -f '(X <> (<> X p0 /\ X (p5 <-> p0)) W (p3 W p0))' \
-    "$ltl2tgba --ba --high --lbtt=t -x ba-simul=0 %f >%T" \
-    "$ltl2tgba --ba --high --lbtt=t -x ba-simul=1 %f >%T" \
-    "$ltl2tgba --ba --high --lbtt=t -x ba-simul=2 %f >%T" \
-    "$ltl2tgba --ba --high --lbtt=t -x ba-simul=3 %f >%T" \
-    "$ltl2tgba --ba --high --lbtt -x ba-simul=0 %f >%T" \
-    "$ltl2tgba --ba --high --lbtt -x ba-simul=1 %f >%T" \
-    "$ltl2tgba --ba --high --lbtt -x ba-simul=2 %f >%T" \
-    "$ltl2tgba --ba --high --lbtt -x ba-simul=3 %f >%T" \
-    "$ltl2tgba --ba --high --spin -x ba-simul=0 %f >%N" \
-    "$ltl2tgba --ba --high --spin -x ba-simul=1 %f >%N" \
-    "$ltl2tgba --ba --high --spin -x ba-simul=2 %f >%N" \
-    "$ltl2tgba --ba --high --spin -x ba-simul=3 %f >%N"
+    "ltl2tgba --ba --high --lbtt=t -x ba-simul=0 %f >%T" \
+    "ltl2tgba --ba --high --lbtt=t -x ba-simul=1 %f >%T" \
+    "ltl2tgba --ba --high --lbtt=t -x ba-simul=2 %f >%T" \
+    "ltl2tgba --ba --high --lbtt=t -x ba-simul=3 %f >%T" \
+    "ltl2tgba --ba --high --lbtt -x ba-simul=0 %f >%T" \
+    "ltl2tgba --ba --high --lbtt -x ba-simul=1 %f >%T" \
+    "ltl2tgba --ba --high --lbtt -x ba-simul=2 %f >%T" \
+    "ltl2tgba --ba --high --lbtt -x ba-simul=3 %f >%T" \
+    "ltl2tgba --ba --high --spin -x ba-simul=0 %f >%N" \
+    "ltl2tgba --ba --high --spin -x ba-simul=1 %f >%N" \
+    "ltl2tgba --ba --high --spin -x ba-simul=2 %f >%N" \
+    "ltl2tgba --ba --high --spin -x ba-simul=3 %f >%N"
diff --git a/tests/core/det.test b/tests/core/det.test
index c04558a0b..7b259e67d 100755
--- a/tests/core/det.test
+++ b/tests/core/det.test
@@ -21,8 +21,6 @@
 . ./defs
 set -e
 
-ltl2tgba=ltl2tgba
-
 cat >formulas <<'EOF'
 1,13,X((a M F((!b & !c) | (b & c))) W (G!c U b))
 1,5,X(((a & b) R (!a U !c)) R b)
@@ -56,7 +54,7 @@ cat >formulas <<'EOF'
 1,4,G(G!a | F!c | G!b)
 EOF
 
-$ltl2tgba -x tba-det --det --stats '%d,%s,%f' -F formulas/3 > out
+ltl2tgba -x tba-det --det --stats '%d,%s,%f' -F formulas/3 > out
 diff formulas out
 
 cat >in.hoa <<'EOF'
diff --git a/tests/core/lbt.test b/tests/core/lbt.test
index cb0ab9151..fce309208 100755
--- a/tests/core/lbt.test
+++ b/tests/core/lbt.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2016 Laboratoire de Recherche et
+# Copyright (C) 2013, 2016, 2017 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -21,10 +21,6 @@
 . ./defs
 set -e
 
-ltlfilt=ltlfilt
-randltl=randltl
-genltl=genltl
-
 # Some example formulas taken from Ruediger Ehlers's dbaminimizer
 #   http://react.cs.uni-saarland.de/tools/dbaminimizer
 # which are expected to be processed by ltl2dstar.
@@ -85,18 +81,18 @@ U p0 & | p0 p5 p1
 EOF
 
 # More examples randomly generated
-$randltl -l -n 100 a p1 "X" "U" "U12" >> formulas
+randltl -l -n 100 a p1 "X" "U" "U12" >> formulas
 
 # Some examples from scalables formulas
-$genltl --rv-counter=1..10 --go-theta=1..10 -l >> formulas
+genltl --rv-counter=1..10 --go-theta=1..10 -l >> formulas
 
 count=`wc -l < formulas`
 
 test $count -eq 168
 
-run 0 $ltlfilt --lbt-input formulas > formulas.2
-run 0 $ltlfilt -l formulas.2 > formulas.3
-run 0 $ltlfilt -l --lbt-input formulas > formulas.4
+run 0 ltlfilt --lbt-input formulas > formulas.2
+run 0 ltlfilt -l formulas.2 > formulas.3
+run 0 ltlfilt -l --lbt-input formulas > formulas.4
 test `wc -l < formulas.2` -eq 168
 test `wc -l < formulas.3` -eq 168
 test `wc -l < formulas.4` -eq 168
@@ -104,15 +100,15 @@ test `wc -l < formulas.4` -eq 168
 # The --csv-escape option is now obsolete and replaced by double
 # quotes in the format string.  So eventually the first two lines
 # should disappear.
-run 0 $ltlfilt formulas.2 --csv-escape --format='%L,%f' > formulas.5
-run 0 $ltlfilt formulas.5/2 --csv-escape --format='%L,%f' > formulas.6
-run 0 $ltlfilt formulas.2 --format='%L,"%f"' > formulas.5a
-run 0 $ltlfilt formulas.5/2 --format='%L,"%f"' > formulas.6a
+run 0 ltlfilt formulas.2 --csv-escape --format='%L,%f' > formulas.5
+run 0 ltlfilt formulas.5/2 --csv-escape --format='%L,%f' > formulas.6
+run 0 ltlfilt formulas.2 --format='%L,"%f"' > formulas.5a
+run 0 ltlfilt formulas.5/2 --format='%L,"%f"' > formulas.6a
 cmp formulas.5 formulas.6
 cmp formulas.5 formulas.5a
 cmp formulas.5a formulas.6a
 
 # Make sure ltl2dstar-style litterals always get quoted.
-test "`$ltlfilt -l --lbt-input -f 'G F a'`" = 'G F "a"'
+test "`ltlfilt -l --lbt-input -f 'G F a'`" = 'G F "a"'
 # Original lbt-style litterals are unquoted.
-test "`$ltlfilt -l --lbt-input -f 'G F p42'`" = 'G F p42'
+test "`ltlfilt -l --lbt-input -f 'G F p42'`" = 'G F p42'
diff --git a/tests/core/lenient.test b/tests/core/lenient.test
index 2e0bdeab4..9097be40f 100755
--- a/tests/core/lenient.test
+++ b/tests/core/lenient.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012 Laboratoire de Recherche et Développement de
+# Copyright (C) 2012, 2017 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -22,8 +22,6 @@
 
 set -e
 
-ltlfilt=ltlfilt
-
 cat >input <<EOF
 (a < b) U (b == c - 1)
 ((a < b) U {b == c - 1})
@@ -48,10 +46,10 @@ cat >expected <<EOF
 Xa
 EOF
 
-run 0 $ltlfilt --lenient input > output
+run 0 ltlfilt --lenient input > output
 cmp output expected
 
 
 
-run 2 $ltlfilt --lenient -f 'F( )' 2> stderr
-grep 'unexpected empty block' stderr
\ No newline at end of file
+run 2 ltlfilt --lenient -f 'F( )' 2> stderr
+grep 'unexpected empty block' stderr
diff --git a/tests/core/ltl2dstar.test b/tests/core/ltl2dstar.test
index 142500aab..d1a00d964 100755
--- a/tests/core/ltl2dstar.test
+++ b/tests/core/ltl2dstar.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
-# Développement de l'Epita (LRDE).
+# Copyright (C) 2013-2017 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -28,16 +28,9 @@ set -e
 # Skip this test if ltl2dstar is not installed.
 (ltl2dstar --version) || exit 77
 
-ltlfilt=ltlfilt
-ltl2tgba=ltl2tgba
-ltlcross=ltlcross
-randltl=randltl
-ltlfilt=ltlfilt
-dstar2tgba=dstar2tgba
-
-$ltlfilt -f 'a U b' -l |
-ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - - |
-$dstar2tgba --stats '%s %e %t %a %d' |
+ltlfilt -f 'a U b' -l |
+ltl2dstar --ltl2nba=spin:ltl2tgba@-s - - |
+dstar2tgba --stats '%s %e %t %a %d' |
 tee out
 
 test "`cat out`" = '2 3 7 1 1'
@@ -45,33 +38,33 @@ test "`cat out`" = '2 3 7 1 1'
 RAB=--automata=rabin
 STR=--automata=streett
 
-$randltl -n 15 a b | $ltlfilt --nnf --remove-wm |
-$ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \
+randltl -n 15 a b | ltlfilt --nnf --remove-wm |
+ltlcross -F - -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \
 --timeout=30 \
-"$ltl2tgba -s %f >%N" \
-"ltl2dstar $RAB --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \
-"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
-"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L - | $dstar2tgba --low -s >%N" \
-"ltl2dstar $STR --output=nba --ltl2nba=spin:$ltl2tgba@-s %L %T" \
-"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" \
-"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L - | $dstar2tgba --low -s >%N" \
+"ltl2tgba -s %f >%N" \
+"ltl2dstar $RAB --output=nba --ltl2nba=spin:ltl2tgba@-s %L %T" \
+"ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L %D" \
+"ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L - | dstar2tgba --low -s >%N" \
+"ltl2dstar $STR --output=nba --ltl2nba=spin:ltl2tgba@-s %L %T" \
+"ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L %D" \
+"ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L - | dstar2tgba --low -s >%N" \
 --csv=out.csv
 
 # A bug in ltlcross <=1.2.5 caused it to not use the complement of the
 # negative automaton.
-$ltlcross -f 'GFa' --verbose \
-"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
-"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err
+ltlcross -f 'GFa' --verbose \
+"ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L %D" \
+"ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L %D" 2>err
 test `grep -c 'info: check_empty.*Comp' err` = 2
-$ltlcross -f 'FGa' --verbose \
-"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %D" \
-"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %D" 2>err
+ltlcross -f 'FGa' --verbose \
+"ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L %D" \
+"ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L %D" 2>err
 test `grep -c 'info: check_empty.*Comp' err` = 2
 
 
 # Make sure ltldo preserve the Rabin acceptance by default
 ltldo \
-    "ltl2dstar --ltl2nba=spin:$ltl2tgba@-s --output-format=hoa %L %O" \
+    "ltl2dstar --ltl2nba=spin:ltl2tgba@-s --output-format=hoa %L %O" \
     -f 'GFa -> GFb' -Hi > out.hoa
 cat >expected <<EOF
 HOA: v1
diff --git a/tests/core/ltl2dstar2.test b/tests/core/ltl2dstar2.test
index ff66d3918..25f5f31a1 100755
--- a/tests/core/ltl2dstar2.test
+++ b/tests/core/ltl2dstar2.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2015, 2016 Laboratoire de Recherche et
+# Copyright (C) 2013, 2015-2017 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -28,33 +28,27 @@ set -e
 # Skip this test if ltl2dstar is not installed.
 (ltl2dstar --version) || exit 77
 
-ltlfilt=ltlfilt
-ltl2tgba=ltl2tgba
-dstar2tgba=dstar2tgba
-randltl=randltl
-
-
 # Make sure all recurrence formulas are translated into deterministic
 # Büchi automata by the DRA->TGBA converter.
 # (Note that ltl2tgba is not called with -D when want to make
 # sure we get a deterministic output even if the automaton generated
 # by Spot initially was non-deterministic)
 
-$randltl -n -1 a b --tree-size=5..15 |
-$ltlfilt --syntactic-recurrence --remove-wm -r -u \
+randltl -n -1 a b --tree-size=5..15 |
+ltlfilt --syntactic-recurrence --remove-wm -r -u \
          --size-min=4 --size-max=15 --relabel=abc |
 head -n 20 > formulas
 
-$randltl -n -1 a b --tree-size=5..15 |
-$ltlfilt -v --obligation |
-$ltlfilt --syntactic-recurrence --remove-wm -r -u --size=4..15 --relabel=abc |
+randltl -n -1 a b --tree-size=5..15 |
+ltlfilt -v --obligation |
+ltlfilt --syntactic-recurrence --remove-wm -r -u --size=4..15 --relabel=abc |
 head -n 20 >> formulas
 
 while read f; do
-  $ltlfilt -f "$f" -l |
-  ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - foo
+  ltlfilt -f "$f" -l |
+  ltl2dstar --ltl2nba=spin:ltl2tgba@-s - foo
   echo "$f"
-  det=`$dstar2tgba foo --stats '%d'`
+  det=`dstar2tgba foo --stats '%d'`
   test $det -eq 1;
 done < formulas
 
@@ -62,16 +56,16 @@ echo ==========================
 
 # For obligation formulas, the output of dstar2tgba should
 # have the same size as the input when option -D is used.
-$randltl -n -1 a b --tree-size=5..15 |
-$ltlfilt --obligation --size=4..15 --relabel=abc --remove-wm -r -u |
+randltl -n -1 a b --tree-size=5..15 |
+ltlfilt --obligation --size=4..15 --relabel=abc --remove-wm -r -u |
 head -n 20 > formulas
 
 while read f; do
-  expected=`$ltl2tgba "$f" -BD --stats '%s %e 1 %d'`
-  $ltlfilt -f "$f" -l |
-  ltl2dstar --ltl2nba=spin:$ltl2tgba@-Ds - foo
+  expected=`ltl2tgba "$f" -BD --stats '%s %e 1 %d'`
+  ltlfilt -f "$f" -l |
+  ltl2dstar --ltl2nba=spin:ltl2tgba@-Ds - foo
   echo "$f"
-  output=`$dstar2tgba foo -BD --stats '%s %e %d 1'`
+  output=`dstar2tgba foo -BD --stats '%s %e %d 1'`
   # the '1 %d' matching '%d 1' makes sure input and output are deterministic.
   test "$output" = "$expected";
 done < formulas
@@ -90,9 +84,9 @@ FGa & FGb
 EOF
 
 while read f; do
-  $ltlfilt -f "$f" -l |
-  ltl2dstar --ltl2nba=spin:$ltl2tgba@-s - foo
+  ltlfilt -f "$f" -l |
+  ltl2dstar --ltl2nba=spin:ltl2tgba@-s - foo
   echo "$f"
-  det=`$dstar2tgba foo --stats '%d'`
+  det=`dstar2tgba foo --stats '%d'`
   test $det -eq 0;
 done < formulas
diff --git a/tests/core/ltl2dstar3.test b/tests/core/ltl2dstar3.test
index 4d4c147cb..592bd8bef 100755
--- a/tests/core/ltl2dstar3.test
+++ b/tests/core/ltl2dstar3.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015 Laboratoire de Recherche et
+# Copyright (C) 2015, 2017 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -26,23 +26,16 @@ set -e
 # Skip this test if ltl2dstar is not installed.
 (ltl2dstar --version) || exit 77
 
-ltlfilt=ltlfilt
-ltl2tgba=ltl2tgba
-ltlcross=ltlcross
-randltl=randltl
-ltlfilt=ltlfilt
-dstar2tgba=dstar2tgba
-
 RAB='--automata=rabin --output-format=hoa'
 STR='--automata=streett --output-format=hoa'
 
 # Run ltlcross without product, because this requires too much memory.
-$randltl -n 25 a b | $ltlfilt --remove-wm |
-$ltlcross -F- -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \
+randltl -n 25 a b | ltlfilt --remove-wm |
+ltlcross -F- -f 'GFa & GFb & GFc' -f '(GFa -> GFb) & (GFc -> GFd)' \
 --timeout=30 --verbose --csv=out.csv --products=0 \
-"$ltl2tgba -s %f >%N" \
-"ltl2dstar $RAB --ltl2nba=spin:$ltl2tgba@-s %L %H" \
-"ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L %H"
+"ltl2tgba -s %f >%N" \
+"ltl2dstar $RAB --ltl2nba=spin:ltl2tgba@-s %L %H" \
+"ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L %H"
 
 grep '"in_type"' out.csv && exit 1
 exit 0
diff --git a/tests/core/ltl2dstar4.test b/tests/core/ltl2dstar4.test
index aabc63e1d..a0db47ec4 100755
--- a/tests/core/ltl2dstar4.test
+++ b/tests/core/ltl2dstar4.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
+# Copyright (C) 2013, 2014, 2015, 2017 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -28,42 +28,34 @@ set -e
 # Skip this test if ltl2dstar is not installed.
 (ltl2dstar --version) || exit 77
 
-ltlfilt=ltlfilt
-ltl2tgba=ltl2tgba
-ltlcross=ltlcross
-randltl=randltl
-autfilt=autfilt
-ltldo=ltldo
-
 STR='--automata=streett --output-format=hoa'
 
-$ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l |
-ltl2dstar --ltl2nba=spin:$ltl2tgba@-s $STR - - |
-$autfilt --tgba --stats '%S %E %A %s %e %t %a %d' |
+ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l |
+ltl2dstar --ltl2nba=spin:ltl2tgba@-s $STR - - |
+autfilt --tgba --stats '%S %E %A %s %e %t %a %d' |
 tee out
 test "`cat out`" = '9 144 4 25 149 416 2 0'
 
-$ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l |
-ltl2dstar --ltl2nba=spin:$ltl2tgba@-s $STR - - |
-SPOT_STREETT_CONV_MIN=1 $autfilt --tgba --stats '%S %E %A %s %e %t %a %d' |
+ltlfilt -f '(GFa -> GFb) & (GFc -> GFd)' -l |
+ltl2dstar --ltl2nba=spin:ltl2tgba@-s $STR - - |
+SPOT_STREETT_CONV_MIN=1 autfilt --tgba --stats '%S %E %A %s %e %t %a %d' |
 tee out
 test "`cat out`" = '9 144 4 25 218 482 2 0'
 
-
-LTL2DSTAR="ltl2dstar $STR --ltl2nba=spin:$ltl2tgba@-s %L"
+LTL2DSTAR="ltl2dstar $STR --ltl2nba=spin:ltl2tgba@-s %L"
 
 # Generate 50 formulas for which the streett automaton has at least 3
 # acceptance sets.
-$randltl --ltl-priorities=W=0,M=0 -n 1000 3 |
-$ltldo "$LTL2DSTAR ->%O" -F- --name=%f -H | tee streett |
-$autfilt --acc-set=3.. --stats=%M | head -n 50 > formulas
+randltl --ltl-priorities=W=0,M=0 -n 1000 3 |
+ltldo "$LTL2DSTAR ->%O" -F- --name=%f -H | tee streett |
+autfilt --acc-set=3.. --stats=%M | head -n 50 > formulas
 
 # Add 50 formulas that use less acceptance sets
-$autfilt streett --acc-set=0..2 --stats=%M | head -n 50 >> formulas
+autfilt streett --acc-set=0..2 --stats=%M | head -n 50 >> formulas
 
-$ltlcross -F formulas --timeout=30 \
-"$ltl2tgba -H %f >%O" \
+ltlcross -F formulas --timeout=30 \
+"ltl2tgba -H %f >%O" \
 "$LTL2DSTAR %O" \
-"$LTL2DSTAR - | SPOT_STREETT_CONV_MIN=0 $autfilt --tgba -H >%O" \
-"$LTL2DSTAR - | SPOT_STREETT_CONV_MIN=1 $autfilt --tgba -H >%O" \
+"$LTL2DSTAR - | SPOT_STREETT_CONV_MIN=0 autfilt --tgba -H >%O" \
+"$LTL2DSTAR - | SPOT_STREETT_CONV_MIN=1 autfilt --tgba -H >%O" \
 --csv=out.csv
diff --git a/tests/core/ltlcross2.test b/tests/core/ltlcross2.test
index a6fb3190c..ca60738d3 100755
--- a/tests/core/ltlcross2.test
+++ b/tests/core/ltlcross2.test
@@ -21,28 +21,26 @@
 . ./defs
 set -e
 
-ltl2tgba=ltl2tgba
-
 randltl -P -n 100 p1 p2 p3 p4 p5 p6 --tree-size 5..15 --seed=314 |
 ltlcross --products=3 --timeout=60 \
-"$ltl2tgba --lbtt --any --low %f > %T" \
-"$ltl2tgba --lbtt --any --medium %f > %T" \
-"$ltl2tgba --hoa  --any --high %f > %H" \
-"$ltl2tgba --lbtt --deterministic --low %f > %T" \
-"$ltl2tgba --lbtt --deterministic --medium %f > %T" \
-"$ltl2tgba --lbtt --deterministic --high %f > %T" \
-"$ltl2tgba --lbtt --small --low %f > %T" \
-"$ltl2tgba --hoa  --small --medium %f > %H" \
-"$ltl2tgba --lbtt --small --high %f > %T" \
-"$ltl2tgba --lbtt -x comp-susp --small %f >%T" \
-"$ltl2tgba --lbtt -x comp-susp,!skel-wdba --small %f >%T" \
-"$ltl2tgba --lbtt -x comp-susp,early-susp --small %f >%T" \
-"$ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --small %f >%T" \
-"$ltl2tgba --spin --ba -x degen-lskip=0 %f >%N" \
-"$ltl2tgba --lbtt --ba --high %f > %T" \
-"$ltl2tgba --spin=6 --ba -x degen-order,degen-lcache=2 --medium %f > %N" \
-"$ltl2tgba --hoa -x degen-lcache=3 -BDC %f > %H" \
-"$ltl2tgba --lbtt -BC %f > %T" \
-"$ltl2tgba --lbtt --unambiguous --low %f > %T" \
-"$ltl2tgba --lbtt --unambiguous --high %f > %T" \
+"ltl2tgba --lbtt --any --low %f > %T" \
+"ltl2tgba --lbtt --any --medium %f > %T" \
+"ltl2tgba --hoa  --any --high %f > %H" \
+"ltl2tgba --lbtt --deterministic --low %f > %T" \
+"ltl2tgba --lbtt --deterministic --medium %f > %T" \
+"ltl2tgba --lbtt --deterministic --high %f > %T" \
+"ltl2tgba --lbtt --small --low %f > %T" \
+"ltl2tgba --hoa  --small --medium %f > %H" \
+"ltl2tgba --lbtt --small --high %f > %T" \
+"ltl2tgba --lbtt -x comp-susp --small %f >%T" \
+"ltl2tgba --lbtt -x comp-susp,!skel-wdba --small %f >%T" \
+"ltl2tgba --lbtt -x comp-susp,early-susp --small %f >%T" \
+"ltl2tgba --lbtt -x comp-susp,!skel-wdba,!skel-simul --small %f >%T" \
+"ltl2tgba --spin --ba -x degen-lskip=0 %f >%N" \
+"ltl2tgba --lbtt --ba --high %f > %T" \
+"ltl2tgba --spin=6 --ba -x degen-order,degen-lcache=2 --medium %f > %N" \
+"ltl2tgba --hoa -x degen-lcache=3 -BDC %f > %H" \
+"ltl2tgba --lbtt -BC %f > %T" \
+"ltl2tgba --lbtt --unambiguous --low %f > %T" \
+"ltl2tgba --lbtt --unambiguous --high %f > %T" \
 --json=output.json --csv=output.csv
diff --git a/tests/core/ltlcross3.test b/tests/core/ltlcross3.test
index d78e6554e..84d14dca9 100755
--- a/tests/core/ltlcross3.test
+++ b/tests/core/ltlcross3.test
@@ -31,16 +31,14 @@ check_csv()
   done)
 }
 
-ltl2tgba=ltl2tgba
-
 # Make sure ltlcross quotes formulas correctly
 cat >formula <<\EOF
 G"a'-'>'b"
 FGa
 EOF
 run 0 ltlcross -F formula --csv=out.csv \
-                         "$ltl2tgba -s %f >%N" \
-                         "$ltl2tgba --lenient -s %s >%N" \
+                         "ltl2tgba -s %f >%N" \
+                         "ltl2tgba --lenient -s %s >%N" \
                          --verbose 2> error
 cat >ceplan <<EOF
 info: check_empty P0*N0
@@ -60,8 +58,8 @@ grep 'info: check_empty' error > ce
 diff -u ce ceplan
 
 ltlcross -F formula --csv=out.csv \
-                   --ref "$ltl2tgba -s %f >%N" \
-                   "$ltl2tgba --lenient -s %s >%N" \
+                   --ref "ltl2tgba -s %f >%N" \
+                   "ltl2tgba --lenient -s %s >%N" \
                    --verbose 2> error
 cat >ceplan <<EOF
 info: check_empty P0*N1
@@ -77,8 +75,8 @@ grep 'info: check_empty' error > ce
 diff -u ce ceplan
 
 ltlcross -F formula --csv=out.csv \
-                   -D "$ltl2tgba -s %f >%N" \
-                   "$ltl2tgba --lenient -s %s >%N" \
+                   -D "ltl2tgba -s %f >%N" \
+                   "ltl2tgba --lenient -s %s >%N" \
                    --verbose 2> error
 cat >ceplan <<EOF
 info: check_empty P0*N0
@@ -98,8 +96,8 @@ grep 'info: check_empty' error > ce
 diff -u ce ceplan
 
 ltlcross -F formula --csv=out.csv \
-                   -D --ref "$ltl2tgba -s %f >%N" \
-                   "$ltl2tgba --lenient -s %s >%N" \
+                   -D --ref "ltl2tgba -s %f >%N" \
+                   "ltl2tgba --lenient -s %s >%N" \
                    --verbose 2> error
 
 cat >ceplan <<EOF
@@ -116,16 +114,16 @@ grep 'info: check_empty' error > ce
 diff -u ce ceplan
 
 ltlcross -F formula --csv=out.csv \
-                    --ref "$ltl2tgba -s %f >%N" \
-                    --ref "$ltl2tgba --lenient -s %s >%N" \
+                    --ref "ltl2tgba -s %f >%N" \
+                    --ref "ltl2tgba --lenient -s %s >%N" \
                     --verbose 2> error
 grep 'info: check_empty' error && exit 1
 
-run 2 ltlcross "$ltl2tgba -s %f >%N" 'foo bar' 2>stderr -f a
+run 2 ltlcross "ltl2tgba -s %f >%N" 'foo bar' 2>stderr -f a
 grep 'ltlcross.*no input.*in.*foo bar' stderr
 
 # Make sure non-zero exit codes are reported...
-run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
+run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
                          -f a --csv=out.csv 2>stderr
 grep '"exit_status"' out.csv
 grep '"exit_code"' out.csv
@@ -134,7 +132,7 @@ test `grep '"exit code",1' out.csv | wc -l` -eq 2
 check_csv out.csv
 
 # ... unless --omit-missing is supplied.
-run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
+run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
                          -f a --csv=out.csv --omit-missing 2>stderr
 grep '"exit_status"' out.csv && exit 1
 grep '"exit_code"' out.csv && exit 1
@@ -143,7 +141,7 @@ test `grep '"exit code",1' out.csv | wc -l` -eq 0
 check_csv out.csv
 
 # Additional columns should not be an issue
-run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
+run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
                -f a --csv=out.csv --strength 2>stderr
 grep '"exit_status"' out.csv
 grep '"exit_code"' out.csv
@@ -154,7 +152,7 @@ test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
 test `grep '"exit code",1' out.csv | wc -l` -eq 2
 check_csv out.csv
 
-run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
+run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
                -f a --csv=out.csv --ambiguous 2>stderr
 grep '"exit_status"' out.csv
 grep '"exit_code"' out.csv
@@ -164,7 +162,7 @@ test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2
 test `grep '"exit code",1' out.csv | wc -l` -eq 2
 check_csv out.csv
 
-run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
+run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
                -f a --csv=out.csv --ambiguous --strength 2>stderr
 grep '"exit_status"' out.csv
 grep '"exit_code"' out.csv
@@ -219,7 +217,7 @@ test `wc -l < bogous` -eq 1
 check_csv out.csv
 
 # Check with --products=5 --automata
-run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
+run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
       -f a --csv=out.csv --products=5 --automata 2>stderr
 p=`sed 's/[^,]//g;q' out.csv | wc -c`
 grep '"exit_status"' out.csv
@@ -230,7 +228,7 @@ test `grep '"HOA:.*--BODY--.*--END--"' out.csv | wc -l` -eq 2
 check_csv out.csv
 
 # ... unless --omit-missing is supplied.
-run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
+run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
       -f a --csv=out.csv --omit-missing --products=5  2>stderr
 grep '"exit_status"' out.csv && exit 1
 grep '"exit_code"' out.csv && exit 1
@@ -240,7 +238,7 @@ check_csv out.csv
 
 
 # Check with --products=+5
-run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
+run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
       -f a --csv=out.csv --products=+5 --automata 2>stderr
 q=`sed 's/[^,]//g;q' out.csv | wc -c`
 grep '"exit_status"' out.csv
@@ -251,7 +249,7 @@ test `grep '"HOA:.*--BODY--.*--END--"' out.csv | wc -l` -eq 2
 check_csv out.csv
 
 # ... unless --omit-missing is supplied.
-run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
+run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%N' \
       -f a --csv=out.csv --omit-missing --products=+5  2>stderr
 grep '"exit_status"' out.csv && exit 1
 grep '"exit_code"' out.csv && exit 1
@@ -265,7 +263,7 @@ test $q -eq `expr $p + 12`
 # Check with Rabin/Streett output
 first="should not be erased"
 echo "$first" > bug.txt
-run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%D' \
+run 1 ltlcross "ltl2tgba -s %f >%N" 'false %f >%D' \
       -f 'X  a' --csv=out.csv --save-bogus='>>bug.txt' 2>stderr
 q=`sed 's/[^,]//g;q' out.csv | wc -c`
 test $q -eq `expr $p - 1`
diff --git a/tests/core/ltlcross4.test b/tests/core/ltlcross4.test
index 84c0ada0d..dd32abb33 100755
--- a/tests/core/ltlcross4.test
+++ b/tests/core/ltlcross4.test
@@ -23,17 +23,15 @@ set -e
 
 test -z "$PYTHON" && exit 77
 
-ltl2tgba=ltl2tgba
-
 cat >formulas.txt <<EOF
 GFa & GFb
 GFa -> GFb
 EOF
 
 ltlcross -F formulas.txt \
-  "{ltl2tgba any} $ltl2tgba --lbtt --any %f > %T" \
-  "{ltl2tgba det} $ltl2tgba --lbtt --deterministic %f > %T" \
-  "{ltl2tgba sma} $ltl2tgba --lbtt --small %f > %T" \
+  "{ltl2tgba any} ltl2tgba --lbtt --any %f > %T" \
+  "{ltl2tgba det} ltl2tgba --lbtt --deterministic %f > %T" \
+  "{ltl2tgba sma} ltl2tgba --lbtt --small %f > %T" \
   --csv=output.csv
 
 cat >test.py <<EOF
diff --git a/tests/core/ltlcrossce2.test b/tests/core/ltlcrossce2.test
index 3aad24860..3e8861fbc 100755
--- a/tests/core/ltlcrossce2.test
+++ b/tests/core/ltlcrossce2.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015, 2016 Laboratoire de Recherche et
+# Copyright (C) 2015-2017 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -21,8 +21,6 @@
 . ./defs
 set -e
 
-ltl2tgba=ltl2tgba
-
 cat >fake <<\EOF
 #!/bin/sh
 case $1 in
@@ -63,7 +61,7 @@ EOF
 chmod +x fake
 
 run 1 ltlcross -f 'G(a <-> Fb) U c' \
-  "$ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors
+  "ltl2tgba --lbtt %f >%T" "./fake %l >%T" 2> errors
 cat errors
 grep 'error: P0\*N1 is nonempty' errors
 grep 'error: P1\*N1 is nonempty' errors
diff --git a/tests/core/ltldo.test b/tests/core/ltldo.test
index 653bef6c9..204540f05 100755
--- a/tests/core/ltldo.test
+++ b/tests/core/ltldo.test
@@ -21,11 +21,7 @@
 . ./defs
 set -e
 
-ltldo=ltldo
-ltl2tgba=ltl2tgba
-genltl=genltl
-
-run 0 $ltldo -f a -f 'a&b' -f 'a -> b' -t 'echo %f,%s,%[ei]w' >output
+run 0 ltldo -f a -f 'a&b' -f 'a -> b' -t 'echo %f,%s,%[ei]w' >output
 cat >expected <<EOF
 a,a,a=1
 (a) & (b),(a) && (b),(a=1) * (b=1)
@@ -34,7 +30,7 @@ EOF
 diff output expected
 
 # Renaming
-run 0 $ltldo -f a -f 'a&_b' -t 'echo %f,%s' >output
+run 0 ltldo -f a -f 'a&_b' -t 'echo %f,%s' >output
 cat >expected <<EOF
 a,a
 (p0) & (p1),(p0) && (p1)
@@ -43,8 +39,8 @@ diff output expected
 
 
 # Test timeouts.  Each of these runs should take 2*2 seconds.
-$genltl --or-g=1..2 |
-run 0 $ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \
+genltl --or-g=1..2 |
+run 0 ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \
 	     >output 2>stderr
 test -z "`cat output`"
 test 4 = `grep -c warning: stderr`
@@ -65,8 +61,8 @@ grep -q 'aborting here' stderr
 
 test "`echo 1,a,3,4 | ltldo -F-/2 ltl2tgba --stats='%<,%s,%>'`" = '1,2,3,4'
 
-$genltl --and-gf=1..3 |
-run 0 $ltldo "{tgba}$ltl2tgba %f -H >%H" "{ba}$ltl2tgba >%N %f -s" \
+genltl --and-gf=1..3 |
+run 0 ltldo "{tgba}ltl2tgba %f -H >%H" "{ba}ltl2tgba >%N %f -s" \
 	     --stats="%T,%#,%f,%s,%t,%e" >output
 cat output
 cat >expected <<EOF
@@ -80,7 +76,7 @@ EOF
 diff output expected
 
 # Renaming
-run 0 $ltldo "$ltl2tgba -H %s>%H" -f GF_foo_ -H >output
+run 0 ltldo "ltl2tgba -H %s>%H" -f GF_foo_ -H >output
 cat output
 # The HOA output uses _foo_ as atomic proposition, but the name shows
 # that GFp0 was actually given to ltl2tgba.
@@ -103,7 +99,7 @@ EOF
 diff output expected
 
 # But we can force the name in the output:
-run 0 $ltldo "$ltl2tgba -H %s>%H" -f GF_foo_ -H --name=%f >output
+run 0 ltldo "ltl2tgba -H %s>%H" -f GF_foo_ -H --name=%f >output
 cat output
 cat >expected <<EOF
 HOA: v1
@@ -124,7 +120,7 @@ EOF
 diff output expected
 
 # Not trusting properties
-run 0 $ltldo "$ltl2tgba -H %s>%H" -f GF_foo_ -H --trust-hoa=no >output
+run 0 ltldo "ltl2tgba -H %s>%H" -f GF_foo_ -H --trust-hoa=no >output
 cat output
 cat >expected <<EOF
 HOA: v1
@@ -144,21 +140,21 @@ State: 0
 EOF
 diff output expected
 
-$ltldo ': %s; true>%O' -f GFa 2>stderr && exit 1
+ltldo ': %s; true>%O' -f GFa 2>stderr && exit 1
 test $? = 2
 grep ':.*empty input' stderr
 grep 'ltldo: aborting' stderr
 
-$ltldo ': %s; true>%O' --errors=ignore -f GFa 2>stderr
+ltldo ': %s; true>%O' --errors=ignore -f GFa 2>stderr
 test $? = 0
 test -z "`cat stderr`"
 
-$ltldo ': %s; true>%O' --errors=warn -f GFa 2>stderr
+ltldo ': %s; true>%O' --errors=warn -f GFa 2>stderr
 test $? = 0
 grep ':.*empty input' stderr
 
 
-$ltldo '{name} foo/bar/ltl2baextended' -f GFa 2>stderr && exit 1
+ltldo '{name} foo/bar/ltl2baextended' -f GFa 2>stderr && exit 1
 grep 'error:.*foo/bar/ltl2baextended -f .*>.*' stderr
 
 
diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test
index 5c24e866b..aef29b43f 100755
--- a/tests/core/ltlfilt.test
+++ b/tests/core/ltlfilt.test
@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
-# Développement de l'Epita (LRDE).
+# Copyright (C) 2013-2017 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -25,12 +25,10 @@
 
 set -e
 
-ltlfilt=ltlfilt
-
 checkopt()
 {
   cat >exp
-  run 0 $ltlfilt "$@" formulas > out
+  run 0 ltlfilt "$@" formulas > out
   diff exp out
 }
 
@@ -226,7 +224,7 @@ p0 | Gp1 | FG(p2 | Xp3)
 p0 | Gp1
 EOF
 
-run 0 $ltlfilt -u --nnf --relabel-bool=pnn in >out
+run 0 ltlfilt -u --nnf --relabel-bool=pnn in >out
 diff exp out
 
 cat >exp <<EOF
@@ -250,7 +248,7 @@ p0 || []p1 || <>[](p2 || Xp3)
 p0 || []p1
 EOF
 
-run 0 $ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out
+run 0 ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out
 diff exp out
 
 cat >exp <<EOF
@@ -290,7 +288,7 @@ p0 && []<>(p1 || p2) && ![]<>!(p1 || p2)
 <>(p0 <-> p1) -> !(p2 <-> p3)
 EOF
 
-run 0 $ltlfilt -s -u --relabel=pnn --define in >out
+run 0 ltlfilt -s -u --relabel=pnn --define in >out
 diff exp out
 
 toolong='((p2=0) * (p3=1))' # work around the 80-col check
@@ -326,10 +324,10 @@ cat >exp <<EOF
 #define p3 (b=1)
 ((p0=1) * (p1=0)) + ((p0=0) * (p1=1)) + (G(((p2=1) * (p3=0)) + $toolong))
 EOF
-run 0 $ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out
+run 0 ltlfilt -p --wring -u --nnf --relabel=pnn --define in >out
 diff exp out
 
-run 0 $ltlfilt -0 in > out
+run 0 ltlfilt -0 in > out
 perl -i -pe 's/\0/@\n/g' out
 cat >exp <<EOF
 a & c & Xb@
@@ -343,38 +341,38 @@ EOF
 diff exp out
 
 SPOT_STUTTER_CHECK=0 \
-$ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
+ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
 test $? = 2
 grep 'non-LTL' stderr
 
 SPOT_STUTTER_CHECK=555 \
-$ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
+ltlfilt --stutter-invariant -f '!{a:b*:c}' 2> stderr && exit 1
 test $? = 2
 grep 'invalid' stderr
 
 SPOT_STUTTER_CHECK=5 \
-$ltlfilt --stutter-invariant -f '!{a:b*:c}'
+ltlfilt --stutter-invariant -f '!{a:b*:c}'
 
 # This one was incorrectly diagnosed as stutter invariant because of a
 # bug in the bitvectors.
-$ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1
+ltlfilt --stutter-invariant -f 'F(a & XXXXXX!a)' && exit 1
 
 
-$ltlfilt -c -o 'foo' -f a 2>stderr && exit 1
+ltlfilt -c -o 'foo' -f a 2>stderr && exit 1
 grep 'ltlfilt: options --output and --count are incompatible' stderr
 
-out=`$ltlfilt -f 'G(a xor b) -> F(c <-> Xd)' --unabbreviate='^iF'`
+out=`ltlfilt -f 'G(a xor b) -> F(c <-> Xd)' --unabbreviate='^iF'`
 exp='(1 U (c <-> Xd)) | !G!(a <-> b)'
 test "$out" = "$exp"
 
-$ltlfilt -f 'GF"a\"\\b"' > out
+ltlfilt -f 'GF"a\"\\b"' > out
 test "`cat out`" = 'GF"a\"\\b"'
 
-$ltlfilt --lbt-input -f 'G F "a\"\\b"' -l > out
+ltlfilt --lbt-input -f 'G F "a\"\\b"' -l > out
 test "`cat out`" = 'G F "a\"\\b"'
 
 
-$ltlfilt --size=foo=2..3  2>stderr && exit 1
+ltlfilt --size=foo=2..3  2>stderr && exit 1
 grep 'invalid range.*should start with' stderr
 
 
diff --git a/tests/core/optba.test b/tests/core/optba.test
index 6a8817c56..65ce06824 100755
--- a/tests/core/optba.test
+++ b/tests/core/optba.test
@@ -24,8 +24,6 @@ set -x
 # This is a case where autfilt is used to optimize BA, but used to
 # produce a larger one.   See issue #79.
 
-autfilt=autfilt
-
 # ltldo -s -f '!(((p1 W c1) U Gp2) || (GXc2 <-> F!F!c1))' 'ltl3ba -M0'
 cat >input <<EOF
 never {
@@ -158,7 +156,7 @@ T0_S18:
 EOF
 
 # 18 states is fine for transition-based acceptance
-test `$autfilt --exclusive-ap=c1,c2 --high --small --stats=%s input` = 18
+test `autfilt --exclusive-ap=c1,c2 --high --small --stats=%s input` = 18
 
 # But we should have 19 with Büchi acceptance, not 20.
-test `$autfilt --exclusive-ap=c1,c2 --high --small -B --stats=%s input` = 19
+test `autfilt --exclusive-ap=c1,c2 --high --small -B --stats=%s input` = 19
diff --git a/tests/core/prodor.test b/tests/core/prodor.test
index 23fb05dbd..cf40c57fd 100755
--- a/tests/core/prodor.test
+++ b/tests/core/prodor.test
@@ -21,9 +21,6 @@
 . ./defs
 set -e
 
-ltl2tgba=ltl2tgba
-autfilt=autfilt
-
 # Two empty automata
 cat >a1.hoa <<EOF
 HOA: v1
@@ -48,11 +45,11 @@ State: 0
 EOF
 
 # the OR product of two empty automata should be empty
-$autfilt --product-or a1.hoa a2.hoa -H | $autfilt --is-empty
+autfilt --product-or a1.hoa a2.hoa -H | autfilt --is-empty
 
-$ltl2tgba -DH 'GFa' > gfa.hoa
-$ltl2tgba -DH 'FGb' > fgb.hoa
-$autfilt --product-or gfa.hoa fgb.hoa -H > por.hoa
+ltl2tgba -DH 'GFa' > gfa.hoa
+ltl2tgba -DH 'FGb' > fgb.hoa
+autfilt --product-or gfa.hoa fgb.hoa -H > por.hoa
 cat por.hoa
 
 cat >exp <<EOF
@@ -81,9 +78,9 @@ State: 2
 EOF
 diff por.hoa exp
 
-test 2 = `$autfilt -c --intersect por.hoa gfa.hoa fgb.hoa`
+test 2 = `autfilt -c --intersect por.hoa gfa.hoa fgb.hoa`
 
-$autfilt --product-and gfa.hoa fgb.hoa -H > pand.hoa
+autfilt --product-and gfa.hoa fgb.hoa -H > pand.hoa
 cat pand.hoa
 
 cat >exp <<EOF
@@ -107,11 +104,11 @@ State: 1
 EOF
 diff pand.hoa exp
 
-test 2 = `$autfilt -c --intersect pand.hoa gfa.hoa fgb.hoa`
+test 2 = `autfilt -c --intersect pand.hoa gfa.hoa fgb.hoa`
 
-$ltl2tgba -BDH 'GFa' > gfa.hoa
-$ltl2tgba -BDH 'Xb' > xb.hoa
-$autfilt --product-or gfa.hoa xb.hoa -H > por.hoa
+ltl2tgba -BDH 'GFa' > gfa.hoa
+ltl2tgba -BDH 'Xb' > xb.hoa
+autfilt --product-or gfa.hoa xb.hoa -H > por.hoa
 cat por.hoa
 
 cat >exp <<EOF
@@ -152,9 +149,9 @@ State: 6
 EOF
 diff por.hoa exp
 
-$ltl2tgba -BDH 'GFa' > gfa.hoa
-$ltl2tgba -x '!wdba-minimize' -DH 'Xb' > xb.hoa
-$autfilt --product-or gfa.hoa xb.hoa -H > por.hoa
+ltl2tgba -BDH 'GFa' > gfa.hoa
+ltl2tgba -x '!wdba-minimize' -DH 'Xb' > xb.hoa
+autfilt --product-or gfa.hoa xb.hoa -H > por.hoa
 cat por.hoa
 
 cat >exp <<EOF
diff --git a/tests/core/rand.test b/tests/core/rand.test
index df52b4562..c5cdf9b67 100755
--- a/tests/core/rand.test
+++ b/tests/core/rand.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -21,9 +21,7 @@
 . ./defs
 set -e
 
-randltl=randltl
-
-run 0 $randltl -S -n 20 a b c --tree-size=10 \
+run 0 randltl -S -n 20 a b c --tree-size=10 \
     --sere-priorities=and=0,andNLM=0 \
     --boolean-priorities=equiv=0,implies=0,xor=0,and=0,not=0 \
     --dump-priorities > stdout
@@ -58,7 +56,7 @@ diff stdout expected
 sere='eword=0,and=0,andNLM=0,fusion=0,star=0,star_b=0'
 sere="$sere,or=0,concat=0,fstar=0,fstar_b=0"
 
-run 0 $randltl -S -n 10000 a b c --tree-size=10..20 \
+run 0 randltl -S -n 10000 a b c --tree-size=10..20 \
    --sere-p=$sere \
    --boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 \
    --dump-pr > stdout
@@ -92,7 +90,7 @@ diff stdout expected
 
 
 # Disabling all operators will prevent more formulas to be generated.
-$randltl -S -n 10000 a b c --tree-size=10..20 \
+randltl -S -n 10000 a b c --tree-size=10..20 \
  --sere-p=$sere \
  --boolean-p=equiv=0,implies=0,xor=0,and=0,not=0,false=0,true=0,or=0 > out &&
   exit 1
@@ -107,7 +105,7 @@ diff expected out2
 
 
 # atomic proposition can be implicitly specified using a number
-$randltl -n 1000 3 --tree-size=10..20 > out
+randltl -n 1000 3 --tree-size=10..20 > out
 grep -q p0 out
 grep -q p1 out
 grep -q p2 out
@@ -116,7 +114,7 @@ grep p3 out && exit 1
 
 # We should be able to generate exactly two formulas with 0 atomic
 # propositions.
-run 0 $randltl -n2 0 | sort > out
+run 0 randltl -n2 0 | sort > out
 cat >expected <<EOF
 0
 1
@@ -124,19 +122,19 @@ EOF
 diff out expected
 
 # requesting more formulas should fail
-run 2 $randltl -n3 0
+run 2 randltl -n3 0
 
 # If more numbers are given, there are interpreted as atomic propositions
-run 0 $randltl -n1000 0 1 > out
+run 0 randltl -n1000 0 1 > out
 grep -q '"0"' out
 grep -q '"1"' out
 
 
-run 0 $randltl -n5 2 -o test-all.ltl
-run 0 $randltl -n5 2 -o test-%L.ltl
+run 0 randltl -n5 2 -o test-all.ltl
+run 0 randltl -n5 2 -o test-%L.ltl
 cat test-1.ltl test-2.ltl test-3.ltl test-4.ltl test-5.ltl > test-cmp.ltl
 diff test-cmp.ltl test-all.ltl
 
 
-$randltl 2 --ltl-prio=X 2>stderr && exit 1
+randltl 2 --ltl-prio=X 2>stderr && exit 1
 grep 'failed to parse LTL priorities near X' stderr
diff --git a/tests/core/randomize.test b/tests/core/randomize.test
index c105b2ada..216a4b05f 100755
--- a/tests/core/randomize.test
+++ b/tests/core/randomize.test
@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
-# l'Epita (LRDE).
+# Copyright (C) 2014, 2015, 2017 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -22,10 +22,7 @@
 
 set -e
 
-ltl2tgba=ltl2tgba
-autfilt=autfilt
-
-$ltl2tgba --hoa 'Ga | Gb | Gc | Gd' > out
+ltl2tgba --hoa 'Ga | Gb | Gc | Gd' > out
 
 cat >expected <<EOF
 HOA: v1
@@ -58,10 +55,10 @@ diff out expected
 
 # The seed and formula where chosen so that these four outputs are
 # different.
-run 0 $autfilt --seed=1 --dot out > 1.dot
-run 0 $autfilt --seed=1 --dot --randomize=t out > 2.dot
-run 0 $autfilt --seed=1 --dot --randomize=s out > 3.dot
-run 0 $autfilt --seed=1 --dot --randomize=st out > 4.dot
+run 0 autfilt --seed=1 --dot out > 1.dot
+run 0 autfilt --seed=1 --dot --randomize=t out > 2.dot
+run 0 autfilt --seed=1 --dot --randomize=s out > 3.dot
+run 0 autfilt --seed=1 --dot --randomize=st out > 4.dot
 
 cmp 1.dot 2.dot && exit 1
 cmp 1.dot 3.dot && exit 1
@@ -70,16 +67,16 @@ cmp 2.dot 4.dot && exit 1
 cmp 3.dot 4.dot && exit 1
 
 # A second run should produce the same output
-$autfilt --seed=1 --dot out > 1b.dot
-$autfilt --seed=1 --dot --randomize=t out > 2b.dot
-$autfilt --seed=1 --dot --randomize=s out > 3b.dot
-$autfilt --seed=1 --dot --randomize=st out > 4b.dot
+autfilt --seed=1 --dot out > 1b.dot
+autfilt --seed=1 --dot --randomize=t out > 2b.dot
+autfilt --seed=1 --dot --randomize=s out > 3b.dot
+autfilt --seed=1 --dot --randomize=st out > 4b.dot
 diff 1.dot 1b.dot
 diff 2.dot 2b.dot
 diff 3.dot 3b.dot
 diff 4.dot 4b.dot
 
-$autfilt --randomize=foo out 2>stderr && exit 1
+autfilt --randomize=foo out 2>stderr && exit 1
 grep "unknown argument for --randomize: 'f'" stderr
 
 
@@ -108,7 +105,7 @@ State: 4 "s0"
 [1] 2
 --END--
 EOF
-$autfilt --randomize --seed=1 input -H > output
+autfilt --randomize --seed=1 input -H > output
 cat >expected <<EOF
 HOA: v1
 States: 5
diff --git a/tests/core/remfin.test b/tests/core/remfin.test
index aa6074496..9003375f8 100755
--- a/tests/core/remfin.test
+++ b/tests/core/remfin.test
@@ -24,8 +24,6 @@
 
 set -e
 
-autfilt=autfilt
-
 cat >test1 <<EOF
 /*
 ** This was a TGBA for GFa & GFb, but
@@ -1412,11 +1410,11 @@ State: 3
 --END--
 EOF
 
-run 0 $autfilt -H --remove-fin test1 > output
+run 0 autfilt -H --remove-fin test1 > output
 cat output
 diff -u output expected
 
-run 0 $autfilt -H --tgba test1 > output
+run 0 autfilt -H --tgba test1 > output
 cat output
 diff -u output expected-tgba
 
diff --git a/tests/core/satmin.test b/tests/core/satmin.test
index 28d61d11e..4f91570c2 100755
--- a/tests/core/satmin.test
+++ b/tests/core/satmin.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013 Laboratoire de Recherche et Développement
+# Copyright (C) 2013, 2017 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -21,9 +21,6 @@
 . ./defs
 set -e
 
-ltl2tgba=ltl2tgba
-ltlcross=ltlcross
-
 # The formulas below have been removed from the list to reduce the time
 # required to complete the test. In the future, we would like to respond
 # quickly to them.
@@ -94,25 +91,25 @@ EOF
 
 # The following tests are named from 1 to 11 in order to reduce the length of
 # each line. If a test fails during the diff, it is easily identifiable.
-$ltlcross -F formulas \
+ltlcross -F formulas \
   --timeout=60 \
-  "{1} $ltl2tgba --det --lbtt %f >%T" \
-  "{2} $ltl2tgba --det --lbtt -x tba-det %f >%T" \
-  "{3} $ltl2tgba --det --lbtt -x sat-acc=1  %f >%T" \
-  "{4} $ltl2tgba --det --lbtt -x sat-acc=3 %f >%T" \
-  "{5} $ltl2tgba --det --lbtt -x sat-states=3 %f >%T" \
-  "{6} $ltl2tgba --det --lbtt -x sat-minimize %f >%T" \
-  "{7} $ltl2tgba --det --lbtt -x 'sat-minimize, sat-langmap' %f >%T" \
-  "{8} $ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=0' %f >%T" \
-  "{9} $ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=1' %f >%T" \
-  "{10} $ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=2' %f >%T" \
-  "{11} $ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=50' %f >%T" \
-  "{12} $ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=-1' %f >%T" \
-  "{13} $ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=0' %f >%T" \
-  "{14} $ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=1' %f >%T" \
-  "{15} $ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=2' %f >%T" \
-  "{16} $ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=50' %f >%T" \
-  "{17} $ltl2tgba --det --lbtt -x sat-minimize=4 %f >%T" \
+  "{1} ltl2tgba --det --lbtt %f >%T" \
+  "{2} ltl2tgba --det --lbtt -x tba-det %f >%T" \
+  "{3} ltl2tgba --det --lbtt -x sat-acc=1  %f >%T" \
+  "{4} ltl2tgba --det --lbtt -x sat-acc=3 %f >%T" \
+  "{5} ltl2tgba --det --lbtt -x sat-states=3 %f >%T" \
+  "{6} ltl2tgba --det --lbtt -x sat-minimize %f >%T" \
+  "{7} ltl2tgba --det --lbtt -x 'sat-minimize, sat-langmap' %f >%T" \
+  "{8} ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=0' %f >%T" \
+  "{9} ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=1' %f >%T" \
+  "{10} ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=2' %f >%T" \
+  "{11} ltl2tgba --det --lbtt -x 'sat-minimize=2, sat-incr-steps=50' %f >%T" \
+  "{12} ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=-1' %f >%T" \
+  "{13} ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=0' %f >%T" \
+  "{14} ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=1' %f >%T" \
+  "{15} ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=2' %f >%T" \
+  "{16} ltl2tgba --det --lbtt -x 'sat-minimize=3, sat-incr-steps=50' %f >%T" \
+  "{17} ltl2tgba --det --lbtt -x sat-minimize=4 %f >%T" \
   --csv=det.csv
 
 grep -v ',\"5\",' det.csv | cut -d ',' -f '1,2,6' > output
diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test
index 65482b54f..4223624a3 100755
--- a/tests/core/sbacc.test
+++ b/tests/core/sbacc.test
@@ -1,7 +1,7 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -22,10 +22,7 @@
 
 set -e
 
-ltl2tgba=ltl2tgba
-autfilt=autfilt
-
-$ltl2tgba 'GFa & GFb' -H | run 0 $autfilt --sbacc -H > out.hoa
+ltl2tgba 'GFa & GFb' -H | run 0 autfilt --sbacc -H > out.hoa
 
 cat >expected<<EOF
 HOA: v1
@@ -94,7 +91,7 @@ State: 1
 
 EOF
 
-run 0 $autfilt --state-based-acceptance in.hoa -H > out.hoa
+run 0 autfilt --state-based-acceptance in.hoa -H > out.hoa
 
 cat >expected <<EOF
 HOA: v1
@@ -130,10 +127,10 @@ EOF
 
 diff out.hoa expected
 
-$autfilt --sba -H expected > out.hoa
+autfilt --sba -H expected > out.hoa
 diff out.hoa expected
 
-$autfilt --strip-acc -H expected -n1 > out.hoa
+autfilt --strip-acc -H expected -n1 > out.hoa
 cat >expected <<EOF
 HOA: v1
 States: 3
@@ -154,9 +151,9 @@ EOF
 diff out.hoa expected
 
 randltl --weak-fairness -n 20 2 |
-    ltlcross "$ltl2tgba -DH %f >%O" \
-             "$ltl2tgba -S %f >%O" \
-             "$ltl2tgba -H %f | $autfilt -H >%O"
+    ltlcross "ltl2tgba -DH %f >%O" \
+             "ltl2tgba -S %f >%O" \
+             "ltl2tgba -H %f | autfilt -H >%O"
 
 test 4 = `ltl2tgba -S 'F(a & X(!a &Xb))' --any --stats=%s`
 
diff --git a/tests/core/strength.test b/tests/core/strength.test
index 6b05029d8..ffb134d08 100755
--- a/tests/core/strength.test
+++ b/tests/core/strength.test
@@ -22,8 +22,6 @@
 
 set -e
 
-autfilt=autfilt
-
 cat >in <<EOF
 HOA: v1
 name: "a U b"
@@ -113,7 +111,7 @@ State: 4
 --END--
 EOF
 
-run 0 $autfilt -H --check=strength in | tee out
+run 0 autfilt -H --check=strength in | tee out
 
 cat >expected <<EOF
 HOA: v1
@@ -221,12 +219,12 @@ EOF
 diff out expected
 
 
-run 0 $autfilt -H --decompose-strength=t in | tee out.t
-run 0 $autfilt -H --decompose-strength=w in | tee out.w
-run 0 $autfilt -H --decompose-strength=s in | tee out.s
-run 0 $autfilt -H --decompose-strength=tw in | tee out.tw
-run 0 $autfilt -H --decompose-strength=ws in | tee out.ws
-run 0 $autfilt -H --decompose-strength=tws in | tee out.tws
+run 0 autfilt -H --decompose-strength=t in | tee out.t
+run 0 autfilt -H --decompose-strength=w in | tee out.w
+run 0 autfilt -H --decompose-strength=s in | tee out.s
+run 0 autfilt -H --decompose-strength=tw in | tee out.tw
+run 0 autfilt -H --decompose-strength=ws in | tee out.ws
+run 0 autfilt -H --decompose-strength=tws in | tee out.tws
 echo '/******************************/' > sep
 cat out.t sep out.w sep out.s sep out.tw sep out.ws sep out.tws > out
 
diff --git a/tests/core/stutter-ltl.test b/tests/core/stutter-ltl.test
index c9665a2cc..663f9fdbf 100755
--- a/tests/core/stutter-ltl.test
+++ b/tests/core/stutter-ltl.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
+# Copyright (C) 2013, 2014, 2015, 2017 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -24,9 +24,6 @@
 
 set -e
 
-randltl=randltl
-ltlfilt=ltlfilt
-
 # Use time only if it is available
 time=time
 if ($time ls) >/dev/null 2>&1; then
@@ -38,15 +35,15 @@ fi
 FILE=formulae
 rm -f $FILE
 for i in 10 12 14 16 18 20; do
-  $randltl --seed 0   --tree-size $i a b c       -n 100 >> $FILE
-  $randltl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE
+  randltl --seed 0   --tree-size $i a b c       -n 100 >> $FILE
+  randltl --seed 100 --tree-size $i a b c d e f -n 100 >> $FILE
 done
 
 # We do not check i=0 and i=9, as they are too slow.
 for i in 1 2 3 4 5 6 7 8; do
     SPOT_STUTTER_CHECK=$i
     export SPOT_STUTTER_CHECK
-    $time $ltlfilt --stutter-invariant -F $FILE > res.$i
+    $time ltlfilt --stutter-invariant -F $FILE > res.$i
 done
 
 # All results should be equal
@@ -69,7 +66,7 @@ EOF
 for i in 0 1 2 3 4 5 6 7 8 9; do
     SPOT_STUTTER_CHECK=$i
     export SPOT_STUTTER_CHECK
-    $time $ltlfilt --stutter-invariant -F $FILE > res.$i
+    $time ltlfilt --stutter-invariant -F $FILE > res.$i
 done
 
 # All results should be equal
diff --git a/tests/core/stutter-tgba.test b/tests/core/stutter-tgba.test
index 9967d2f21..90d0c8e65 100755
--- a/tests/core/stutter-tgba.test
+++ b/tests/core/stutter-tgba.test
@@ -22,32 +22,29 @@
 
 set -e
 
-ltl2tgba=ltl2tgba
-autfilt=autfilt
+ltl2tgba '!FG(a | Xa | G!a)' -H | autfilt -H --destut > pos.hoa
+ltl2tgba 'FG(a | Xa | G!a)' -H | autfilt -H --destut > neg.hoa
+autfilt pos.hoa --product neg.hoa -H > prod.hoa
+autfilt --is-empty prod.hoa -q && exit 1
+autfilt --states=7 prod.hoa -q
 
-$ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --destut > pos.hoa
-$ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --destut > neg.hoa
-$autfilt pos.hoa --product neg.hoa -H > prod.hoa
-$autfilt --is-empty prod.hoa -q && exit 1
-$autfilt --states=7 prod.hoa -q
-
-$ltl2tgba '!FG(a | Xa | G!a)' -H | $autfilt -H --instut > pos.hoa
-$ltl2tgba 'FG(a | Xa | G!a)' -H | $autfilt -H --instut > neg.hoa
-$autfilt pos.hoa --product neg.hoa -H > prod.hoa
-$autfilt --is-empty prod.hoa -q && exit 1
-$autfilt --states=9 prod.hoa -q
+ltl2tgba '!FG(a | Xa | G!a)' -H | autfilt -H --instut > pos.hoa
+ltl2tgba 'FG(a | Xa | G!a)' -H | autfilt -H --instut > neg.hoa
+autfilt pos.hoa --product neg.hoa -H > prod.hoa
+autfilt --is-empty prod.hoa -q && exit 1
+autfilt --states=9 prod.hoa -q
 
 
 # Check for issue #7.
 #
 # We just run those without checking the output, it is enough to
 # trigger assertions in the HOA output routines.
-$ltl2tgba -H 'X(a U b)' > det.hoa
-run 0 $autfilt --destut det.hoa -H
-run 0 $autfilt --instut=1 det.hoa -H
-run 0 $autfilt --instut=2 det.hoa -H
+ltl2tgba -H 'X(a U b)' > det.hoa
+run 0 autfilt --destut det.hoa -H
+run 0 autfilt --instut=1 det.hoa -H
+run 0 autfilt --instut=2 det.hoa -H
 
-$ltl2tgba -H 'a & Fb' | $autfilt --destut -H > output
+ltl2tgba -H 'a & Fb' | autfilt --destut -H > output
 
 cat >expected <<EOF
 HOA: v1
@@ -72,36 +69,36 @@ EOF
 
 diff output expected
 
-$ltl2tgba -H 'F(a & X(!a & b))' > input
+ltl2tgba -H 'F(a & X(!a & b))' > input
 grep ' stutter-invariant' input && exit 1
-run 0 $ltl2tgba --check=stutter 'F(a & X(!a & b))' > input.2
+run 0 ltl2tgba --check=stutter 'F(a & X(!a & b))' > input.2
 grep ' stutter-invariant' input.2
-run 0 $autfilt --check=stutter input > input.2
+run 0 autfilt --check=stutter input > input.2
 grep ' stutter-invariant' input.2
 
-$ltl2tgba 'F(a & X(a & b))' > input
+ltl2tgba 'F(a & X(a & b))' > input
 grep stutter-invariant input && exit 1
 # HOA v1.1 calls it "!stutter-invariant"
-run 0 $ltl2tgba -H1.1 --check=stutter 'F(a & X(a & b))' > input.2
+run 0 ltl2tgba -H1.1 --check=stutter 'F(a & X(a & b))' > input.2
 grep '!stutter-invariant' input.2
 # HOA v1 has no name, so we use "stutter-sensitive"
-run 0 $autfilt --check=stutter input > input.2
+run 0 autfilt --check=stutter input > input.2
 test `autfilt -c -v --is-stutter-invariant input` = 1
 grep stutter-sensitive input.2
 
-$ltl2tgba 'F(a & X(!a & Gb))' > input
+ltl2tgba 'F(a & X(!a & Gb))' > input
 grep stutter-invariant input && exit 1
 grep deterministic input && exit 1
 # This will involve a complementation
-run 0 $autfilt --check=stutter input > input.2
+run 0 autfilt --check=stutter input > input.2
 test `autfilt -c --is-stutter-invariant input` = 1
 grep ' stutter-invariant' input.2
 
-$ltl2tgba 'F(a & X(a & Gb))' > input
+ltl2tgba 'F(a & X(a & Gb))' > input
 grep stutter input && exit 1
 grep deterministic input && exit 1
 # This will involve a complementation
-run 0 $autfilt -H1.1 --check=stutter input > input.2
+run 0 autfilt -H1.1 --check=stutter input > input.2
 test `autfilt -c --is-stutter-invariant input` = 0
 grep '!deterministic' input.2
 grep '!stutter-invariant' input.2
diff --git a/tests/core/unabbrevwm.test b/tests/core/unabbrevwm.test
index a9d266a6a..089df24c3 100755
--- a/tests/core/unabbrevwm.test
+++ b/tests/core/unabbrevwm.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2015 Laboratoire de Recherche et Développement
+# Copyright (C) 2012, 2015, 2017 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -25,10 +25,8 @@
 
 set -e
 
-ltlfilt=ltlfilt
-
 # Removing W,M in this formula caused a segfault at some point.
-run 0 $ltlfilt --remove-wm >out <<EOF
+run 0 ltlfilt --remove-wm >out <<EOF
 (!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0))
 (Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))
 EOF
@@ -40,7 +38,7 @@ test `uniq out | wc -l` = 1
 for i in 'GFa' 'a R b' 'a W b' 'a M b'; do
     for fg in '' F G GF; do
 	for rwm in '' R W M RW RM WM RWM; do
-	    $ltlfilt -f "$i" --unabbrev=$fg$rwm --equivalent-to "$i" >out
+	    ltlfilt -f "$i" --unabbrev=$fg$rwm --equivalent-to "$i" >out
 	    test -n "$rwm" && grep "[$rwm]" out && exit 1
 	done
     done
diff --git a/tests/core/unambig.test b/tests/core/unambig.test
index 2ba0d3bfc..25c52752d 100755
--- a/tests/core/unambig.test
+++ b/tests/core/unambig.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2013, 2015, 2016 Laboratoire de Recherche et
+# Copyright (C) 2013, 2015-2017 Laboratoire de Recherche et
 # Developpement de l'Epita
 #
 # This file is part of Spot, a model checking library.
@@ -22,9 +22,6 @@
 
 set -e
 
-ltl2tgba=ltl2tgba
-autfilt=autfilt
-
 for f in 'Ga' \
          'Ga | Gb' \
          'Ga | GFb' \
@@ -34,18 +31,18 @@ for f in 'Ga' \
 	 'F(a & !b & (!c W b))' \
          'G({{1;1}*}<>->a)'
 do
-  $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous
-  $ltl2tgba -UH "!($f)" | $autfilt -q --is-unambiguous
-  $ltl2tgba -UH "$f" | $autfilt --check |
+  ltl2tgba -UH "$f" | autfilt -q --is-unambiguous
+  ltl2tgba -UH "!($f)" | autfilt -q --is-unambiguous
+  ltl2tgba -UH "$f" | autfilt --check |
       grep -E 'properties:.* (unambiguous|deterministic)'
-  $ltl2tgba -UH "!($f)" | $autfilt --check |
+  ltl2tgba -UH "!($f)" | autfilt --check |
       grep -E 'properties:.* (unambiguous|deterministic)'
 done
 
 for f in FGa '{[*1..4]}<>-> (p1 & (p1 U p0))'
 do
-  $ltl2tgba -H "$f" | $autfilt -qv --is-unambiguous
-  $ltl2tgba -UH "$f" | $autfilt -q --is-unambiguous
+  ltl2tgba -H "$f" | autfilt -qv --is-unambiguous
+  ltl2tgba -UH "$f" | autfilt -q --is-unambiguous
 done
 
 # All these should be detected as ambiguous automata
@@ -147,13 +144,13 @@ State: 2
 --END--
 EOF
 
-run 1 $autfilt -q --is-unambiguous input
-run 0 $autfilt --check input > output
+run 1 autfilt -q --is-unambiguous input
+run 0 autfilt --check input > output
 test `grep -c unambiguous output` = 0
 
 # Check 1000 random PSL formulas
-randltl --psl -n 1000 3 | $ltl2tgba -U -H |
-  $autfilt -v --is-unamb --stats=%M && exit 1
+randltl --psl -n 1000 3 | ltl2tgba -U -H |
+  autfilt -v --is-unamb --stats=%M && exit 1
 
 cat >input <<EOF
 HOA: v1
@@ -194,7 +191,7 @@ ltl2tgba --lbt-input -B -U -x wdba-minimize=0 "U p0 & p1 X ! p0" |
 
 
 # Make sure we preserve the "unambiguous" property if it is given.
-run 0 $autfilt -H --is-unambiguous input >output
+run 0 autfilt -H --is-unambiguous input >output
 
 cat >expected <<EOF
 HOA: v1