From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 30 Jul 2019 07:36:58 +0000 (-0500)
Subject: Remove hard coded option for TPTP regressions in run_regression (#3128)
X-Git-Tag: cvc5-1.0.0~4069
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=943a4781526e5d5e9ca943a0955f30fbb9f7ba61;p=cvc5.git

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 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
 
 %--------------------------------------------------------------------------
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 759582afc..59913a9d6 100755
--- 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':