From 46204d4186b62451012a7d56f266c36a3108c27f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Mon, 19 Aug 2024 17:27:15 +0200 Subject: [PATCH] Fix build in new regression tests --- .../generic/ReqCheckerRedundancyRegressionTestSuite.java | 6 ++++-- .../regressiontest/generic/WitnessRegressionTestSuite.java | 5 +++-- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java index d2026acec37..72bfa775883 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java @@ -76,7 +76,8 @@ public ReqCheckerRedundancyRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { return new ReqCheckerTestResultDecider(runDefinition, false); } @@ -173,7 +174,8 @@ public boolean isSuccess(final ReqCheckerResult actual) { } return false; } - if ((mNoResults != -1 && actual.mNoResults != mNoResults) || DataStructureUtils.isDifferent(actual.mRedundant, mRedundant)) { + if ((mNoResults != -1 && actual.mNoResults != mNoResults) + || DataStructureUtils.isDifferent(actual.mRedundant, mRedundant)) { return false; } return true; diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java index 1d5d85f033c..6a8ff8f0345 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/WitnessRegressionTestSuite.java @@ -61,7 +61,8 @@ public WitnessRegressionTestSuite() { } @Override - protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { return new WitnessSafetyCheckTestResultDecider(runDefinition); } @@ -77,7 +78,7 @@ public Collection createTestCases() { final File[] newFiles = DataStructureUtils.concat(def.getInput(), new File[] { witness }); final UltimateRunDefinition newDef = new UltimateRunDefinition(newFiles, def.getSettings(), def.getToolchain(), def.getTimeout()); - result.add(new UltimateTestCase(getTestResultDecider(def), newDef, List.of(), null)); + result.add(new UltimateTestCase(getTestResultDecider(def, null), newDef, List.of(), null)); } } }