add quick workaround for problem (new fixpoint checks says UNKNOWN mo…

…re often) that was introduced in 2b22b30
ultimate-pa · Oct 1, 2022 · cf36bb6 · cf36bb6
1 parent b55dc6b
commit cf36bb6
Showing 1 changed file with 10 additions and 1 deletion.
diff --git a/.../src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/LassoCheck.java b/.../src/de/uni_freiburg/informatik/ultimate/plugins/generator/buchiautomizer/LassoCheck.java
@@ -556,7 +556,16 @@ private SynthesisResult synthesize(final boolean withStem, UnmodifiableTransForm
 		if (fixpointCheck.getResult() == HasFixpoint.YES) {
 			if (withStem) {
 				if (TRACE_CHECK_BASED_FIXPOINT_CHECK) {
-					final FixpointCheck2<L> fixpointCheck2 = new FixpointCheck2<L>(mServices, mLogger, mCsToolkit, mPredicateFactory, mCounterexample.getStem(), loopTF);
+					final FixpointCheck2<L> fixpointCheck2 = new FixpointCheck2<L>(mServices, mLogger, mCsToolkit,
+							mPredicateFactory, mCounterexample.getStem(), loopTF);
+					if (fixpointCheck2.getResult() == HasFixpoint.UNKNOWN) {
+						mNonterminationArgument = fixpointCheck.getTerminationArgument();
+					} else {
+						throw new AssertionError(String.format(
+								"Contradiciting results of nontermination analyses: Old %s, New %s, Stem length %s, Loop length %s",
+								fixpointCheck.getResult(), fixpointCheck2.getResult(),
+								mCounterexample.getStem().getLength(), mCounterexample.getLoop().getLength()));
+					}
 					mNonterminationArgument = fixpointCheck2.getTerminationArgument();
 				} else {
 					mNonterminationArgument = fixpointCheck.getTerminationArgument();