12 files changed, 19 insertions, 1 deletions
diff --git a/test/regress/regress0/tptp/KRS018+1.p b/test/regress/regress0/tptp/KRS018+1.p
index 91039877b..8d0bbe25c 100644
--- a/test/regress/regress0/tptp/KRS018+1.p
+++ b/test/regress/regress0/tptp/KRS018+1.p
@@ -1,3 +1,5 @@
+% COMMAND-LINE: --finite-model-find
+
 %------------------------------------------------------------------------------
 % File     : KRS018+1 : TPTP v5.5.0. Released v3.1.0.
 % Domain   : Knowledge Representation (Semantic Web)
diff --git a/test/regress/regress0/tptp/MGT019+2.p b/test/regress/regress0/tptp/MGT019+2.p
index fb2cd7f62..e6a2ffe74 100644
--- a/test/regress/regress0/tptp/MGT019+2.p
+++ b/test/regress/regress0/tptp/MGT019+2.p
@@ -1,3 +1,5 @@
+% COMMAND-LINE: --finite-model-find
+
 %--------------------------------------------------------------------------
 % File     : MGT019+2 : TPTP v5.5.0. Released v2.0.0.
 % Domain   : Management (Organisation Theory)
diff --git a/test/regress/regress0/tptp/SYN000+2.p b/test/regress/regress0/tptp/SYN000+2.p
index 8c6f2f9f9..161fa2154 100644
--- a/test/regress/regress0/tptp/SYN000+2.p
+++ b/test/regress/regress0/tptp/SYN000+2.p
@@ -1,3 +1,5 @@
+% COMMAND-LINE: --finite-model-find
+
 %------------------------------------------------------------------------------
 % File     : SYN000+2 : TPTP v5.5.0. Bugfixed v4.1.1.
 % Domain   : Syntactic
diff --git a/test/regress/regress0/tptp/SYN000-2.p b/test/regress/regress0/tptp/SYN000-2.p
index 0c6c0b59f..9f0cb57be 100644
--- a/test/regress/regress0/tptp/SYN000-2.p
+++ b/test/regress/regress0/tptp/SYN000-2.p
@@ -1,3 +1,5 @@
+% COMMAND-LINE: --finite-model-find
+
 %------------------------------------------------------------------------------
 % File     : SYN000-2 : TPTP v5.5.0. Bugfixed v4.1.1.
 % Domain   : Syntactic
diff --git a/test/regress/regress0/tptp/SYN000_2.p b/test/regress/regress0/tptp/SYN000_2.p
index ece5fa6b1..15ca478e7 100644
--- a/test/regress/regress0/tptp/SYN000_2.p
+++ b/test/regress/regress0/tptp/SYN000_2.p
@@ -1,3 +1,5 @@
+% COMMAND-LINE: --finite-model-find
+
 %------------------------------------------------------------------------------
 % File     : SYN000_2 : TPTP v5.5.0. Bugfixed v5.5.1.
 % Domain   : Syntactic
@@ -24,7 +26,7 @@
 %            Maximal term depth    :    2 (   1 average)
 % SPC      : TF0_SAT_EQU_NAR
 
-% Comments : 
+% Comments :
 % Bugfixes : v5.5.1 - Fixed let_binders.
 %------------------------------------------------------------------------------
 %----Quoted symbols
diff --git a/test/regress/regress0/tptp/SYN075-1.p b/test/regress/regress0/tptp/SYN075-1.p
index 40b49fa36..85ac2d278 100644
--- a/test/regress/regress0/tptp/SYN075-1.p
+++ b/test/regress/regress0/tptp/SYN075-1.p
@@ -1,3 +1,5 @@
+% COMMAND-LINE: --finite-model-find
+
 %--------------------------------------------------------------------------
 % File     : SYN075-1 : TPTP v5.5.0. Released v1.0.0.
 % Domain   : Syntactic
diff --git a/test/regress/regress0/tptp/tptp_parser4.p b/test/regress/regress0/tptp/tptp_parser4.p
index 448db77d2..6475112b4 100644
--- a/test/regress/regress0/tptp/tptp_parser4.p
+++ b/test/regress/regress0/tptp/tptp_parser4.p
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --finite-model-find
 % Status: Unsatisfiable
 
 %--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/tptp_parser5.p b/test/regress/regress0/tptp/tptp_parser5.p
index c90d1cdad..62744f650 100644
--- a/test/regress/regress0/tptp/tptp_parser5.p
+++ b/test/regress/regress0/tptp/tptp_parser5.p
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --finite-model-find
 % Status: Satisfiable
 
 %--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/tptp_parser6.p b/test/regress/regress0/tptp/tptp_parser6.p
index 6283eb29a..4308384f9 100644
--- a/test/regress/regress0/tptp/tptp_parser6.p
+++ b/test/regress/regress0/tptp/tptp_parser6.p
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --finite-model-find
 % Status: Satisfiable
 
 %--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/tptp_parser7.p b/test/regress/regress0/tptp/tptp_parser7.p
index 73c2b3834..9288cbbd0 100644
--- a/test/regress/regress0/tptp/tptp_parser7.p
+++ b/test/regress/regress0/tptp/tptp_parser7.p
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --finite-model-find
 % Status: Satisfiable
 
 %--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/tptp_parser8.p b/test/regress/regress0/tptp/tptp_parser8.p
index da281151b..b60799f1a 100644
--- a/test/regress/regress0/tptp/tptp_parser8.p
+++ b/test/regress/regress0/tptp/tptp_parser8.p
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --finite-model-find
 % Status: Satisfiable
 
 %--------------------------------------------------------------------------
diff --git a/test/regress/regress0/tptp/tptp_parser9.p b/test/regress/regress0/tptp/tptp_parser9.p
index 9bed19702..4ce2e0227 100644
--- a/test/regress/regress0/tptp/tptp_parser9.p
+++ b/test/regress/regress0/tptp/tptp_parser9.p
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --finite-model-find
 % Status: CounterSatisfiable
 
 %--------------------------------------------------------------------------