diff --git a/tests/ltsmin/check.test b/tests/ltsmin/check.test
index f0a0fd9c0..2beb82cc3 100755
--- a/tests/ltsmin/check.test
+++ b/tests/ltsmin/check.test
@@ -90,7 +90,7 @@ run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
     --csv --bloemen -p 1 | grep -v Thread > stdout
 test `grep "#" stdout | awk -F',' '{print $8}'` -eq 29115
 
-# Test Bloemen
+# Test Multithreaded Bloemen
 run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
     --csv --bloemen -p 3 | grep -v Thread > stdout
 test `grep "#" stdout | awk -F',' '{print $8}'` -eq 29115
@@ -98,13 +98,22 @@ test `grep "#" stdout | awk -F',' '{print $8}'` -eq 29115
 run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
     --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv  \
     --bloemen-ec -p 3 | grep -v Thread > stdout
+test `grep "#" stdout | awk -F',' '{print $8}'` -eq 1148594
 
 # Test CNDFS
 run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
     --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv  \
     --cndfs -p 3 | grep -v Thread >stdout
+test `grep "#" stdout | awk -F',' '{print $5}'` = "empty"
 
 # Test SWARMING
 run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
     --formula '!GF(P_0.CS|P_1.CS|P_2.CS|P_3.CS)' --csv  \
     --swarming -p 3 | grep -v Thread > stdout
+test `grep "#" stdout | awk -F',' '{print $5}'` = "empty"
+
+# Test REACHABILITY
+run 0 ../modelcheck --model $srcdir/beem-peterson.4.dve \
+    --reachability -p 1 --csv | grep -v Thread > stdout
+test `grep "#" stdout | awk -F',' '{print $6}'` -eq 1119560
+test `grep "#" stdout | awk -F',' '{print $7}'` -eq 3864896
diff --git a/tests/ltsmin/finite.test b/tests/ltsmin/finite.test
index 042f428c6..ad1497035 100755
--- a/tests/ltsmin/finite.test
+++ b/tests/ltsmin/finite.test
@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2011, 2013, 2014, 2016 Laboratoire de Recherche et
+# Copyright (C) 2011, 2013, 2014, 2016, 2020 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -57,6 +57,61 @@ run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
 run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
     --formula '!(G(dead -> ("P.a==2" | "P.b==3")))'
 
+run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '!(G(dead -> ("P.a==2" | "P.b==3")))' -c -p 1
+
+run 1 ../modelcheck --cndfs --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '!(G(dead -> ("P.a==2" | "P.b==3")))' -c -p 1
+
+run 1 ../modelcheck --swarming --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '!(G(dead -> ("P.a==2" | "P.b==3")))' -c -p 1
+
+# Test the various combination for atomic propositions
+run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '(F("P.b == P.a"))' -c -p 1
+
+run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '(F("P.b < P.a"))' -c -p 1
+
+run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '(F("P.b <= P.a"))' -c -p 1
+
+run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '(F("P.b > P.a"))' -c -p 1
+
+run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '!(F("P.b >= P.a"))' -c -p 1
+
+run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '!(F("P.a>4"))' -c -p 1
+
+run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '(F("5==P.a"))' -c -p 1
+
+run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '(F("5<=P.a"))' -c -p 1
+
+run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '!(F("5>P.a"))' -c -p 1
+
+run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '!(F("5>=P.a"))' -c -p 1
+
+run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '!(F("P.b>=P.a"))' -c -p 1
+
+run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '!(F("P.b>P.a"))' -c -p 1
+
+run 1 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '!(F("P.b<P.a"))' -c -p 1
+
+run 0 ../modelcheck --is-empty --selfloopize dead --model $srcdir/finite.dve \
+    --formula  '!(F("P.b<=P.a"))' -c -p 1
+
+run 1 ../modelcheck --model $srcdir/finite.dve \
+    --csv --has-deadlock -p 1 -c
+
 # This used to segfault because of a bug in a
 # function that do not exist anymore.
 run 0 ../modelcheck --dot product --model $srcdir/finite.dve \