From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 8 Apr 2021 22:29:49 +0000 (-0500)
Subject: Fix run_regression for cvc expected outputs (#6317)
X-Git-Tag: cvc5-1.0.0~1938
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d671eff2c953acb5c19e5d912aca581babce57dc;p=cvc5.git

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 9e746c0e4..8b9497020 100644
--- 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 ce99edbb7..159709835 100644
--- 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 67be78912..31065ba41 100644
--- 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 01924559a..a4f2b85df 100755
--- 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 \