Remove hard coded option for TPTP regressions in run_regression (#3128)

diff --git a/test/regress/regress0/tptp/KRS018+1.p b/test/regress/regress0/tptp/KRS018+1.p
index 91039877b14b5c2d23ada413e3cf98bbcd292b82..8d0bbe25c4d503bb80ef4cfee34b2018815bf749 100644 (file)
--- 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 fb2cd7f62fb911000200224dce22bbea4ac003f4..e6a2ffe74a127f2aa80b36bb8dec846df6d3c552 100644 (file)
--- 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 8c6f2f9f947817e5b4fa3e4f5d6952e2d4c971d7..161fa2154d0913054142858483924b87ad4c6851 100644 (file)
--- 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 0c6c0b59f92a227b70011eaba72eabc090965af9..9f0cb57be3edc67e087da6404d511c9d72cb77a9 100644 (file)
--- 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 ece5fa6b12d230cfd8f4e56f9d18d073ce4b5a81..15ca478e7d53c93d26c50266dc9a395ad1429a12 100644 (file)
--- 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 40b49fa36ae83b682f88054a7c1d8f32058fba14..85ac2d27818acc8ba3c1b6dde2fe183e435ff936 100644 (file)
--- 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 448db77d27630e5cb8e4140e92bb00d0993c5ec5..6475112b410875fc9981dcf9b205f0052d6c4945 100644 (file)
--- 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 c90d1cdadebacd06c147607450cc9b7d296614c1..62744f65001d5ab337e7e6a946aaaa1df785a7e6 100644 (file)
--- 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 6283eb29ad3b04bdae4fa0f349551acd3787e5d0..4308384f9f7df0b404d98f0c0eefe7e33f77584e 100644 (file)
--- 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 73c2b383498cbc09de7e9573432435e22239c5a9..9288cbbd05c9c08a93ecb48165e4877f958427a6 100644 (file)
--- 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 da281151b53d2c13255ea2319ca161716891c8e0..b60799f1a7ed1d3941a35bd9e4b929c26029a559 100644 (file)
--- 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 9bed197023b7d872fd4a0efd1401a5af87a2dd41..4ce2e02271f566eb0edbf153b8930c8f58fe9d6c 100644 (file)
--- 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
 
 %--------------------------------------------------------------------------

diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 759582afcc3d7dc717e36dd12bc1d6c64c416629..59913a9d63d7af81431a3ff06b1fa56fedf6ecb3 100755 (executable)
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -161,7 +161,6 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper,
     elif benchmark_ext == '.cvc':
         pass
     elif benchmark_ext == '.p':
-        basic_command_line_args.append('--finite-model-find')
         status_regex = r'% Status\s*:\s*(Theorem|Unsatisfiable|CounterSatisfiable|Satisfiable)'
         status_to_output = lambda s: '% SZS status {} for {}'.format(s, benchmark_filename)
     elif benchmark_ext == '.sy':