Fix run_regression for cvc expected outputs (#6317)

Previously, we were not checking models / proofs / unsat cores for cvc inputs on CI.

diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc
index 9e746c0e43d10472b316db18f2b9f7e9ef48ee09..8b94970206d4330c970fab359cc87bac24b91e62 100644 (file)
--- a/test/regress/regress0/datatypes/datatype1.cvc
+++ b/test/regress/regress0/datatypes/datatype1.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: -q
 % EXPECT: not_entailed
 
 DATATYPE

diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc
index ce99edbb7b251485e30d5b3091b2a27e9229bf83..1597098355e1d444f2d15b2b5404461285375181 100644 (file)
--- a/test/regress/regress0/datatypes/datatype3.cvc
+++ b/test/regress/regress0/datatypes/datatype3.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: -q
 % EXPECT: not_entailed
 
 DATATYPE

diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc
index 67be78912a1fb31e261ff82441a0ceafd34d0ea2..31065ba41a6fc0e97ad475867c1dafab751dca28 100644 (file)
--- a/test/regress/regress0/datatypes/wrong-sel-simp.cvc
+++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: -q
 % EXPECT: not_entailed
 DATATYPE
   nat = succ(pred : nat) | zero

diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 01924559abd232e6cef68c8e5f7a7aa132a14c4b..a4f2b85df2027bfc3a2338019522fde282780ffa 100755 (executable)
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -329,13 +329,13 @@ def run_regression(check_unsat_cores, check_proofs, dump, use_skip_return_code,
             '--check-synth-sol' not in all_args:
             extra_command_line_args += ['--check-synth-sol']
         if ('sat' in expected_output_lines or \
-            'invalid' in expected_output_lines or \
+            'not_entailed' in expected_output_lines or \
             'unknown' in expected_output_lines) and \
            '--no-debug-check-models' not in all_args and \
            '--no-check-models' not in all_args and \
            '--debug-check-models' not in all_args:
             extra_command_line_args += ['--debug-check-models']
-        if 'unsat' in expected_output_lines or 'valid' in expected_output_lines:
+        if 'unsat' in expected_output_lines or 'entailed' in expected_output_lines:
             if check_unsat_cores and \
                '--no-produce-unsat-cores' not in all_args and \
                '--no-check-unsat-cores' not in all_args and \