diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-07-30 02:36:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-30 02:36:58 -0500 |
commit | 943a4781526e5d5e9ca943a0955f30fbb9f7ba61 (patch) | |
tree | 32579ebef6aa7c05458200f52c734f522b3f1b80 /test/regress/regress0 | |
parent | f71a719b8000e901af141a326ac12bce59a6153d (diff) |
Remove hard coded option for TPTP regressions in run_regression (#3128)
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/tptp/KRS018+1.p | 2 | ||||
-rw-r--r-- | test/regress/regress0/tptp/MGT019+2.p | 2 | ||||
-rw-r--r-- | test/regress/regress0/tptp/SYN000+2.p | 2 | ||||
-rw-r--r-- | test/regress/regress0/tptp/SYN000-2.p | 2 | ||||
-rw-r--r-- | test/regress/regress0/tptp/SYN000_2.p | 4 | ||||
-rw-r--r-- | test/regress/regress0/tptp/SYN075-1.p | 2 | ||||
-rw-r--r-- | test/regress/regress0/tptp/tptp_parser4.p | 1 | ||||
-rw-r--r-- | test/regress/regress0/tptp/tptp_parser5.p | 1 | ||||
-rw-r--r-- | test/regress/regress0/tptp/tptp_parser6.p | 1 | ||||
-rw-r--r-- | test/regress/regress0/tptp/tptp_parser7.p | 1 | ||||
-rw-r--r-- | test/regress/regress0/tptp/tptp_parser8.p | 1 | ||||
-rw-r--r-- | test/regress/regress0/tptp/tptp_parser9.p | 1 |
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 %-------------------------------------------------------------------------- |