Bugfix: Do not always reportUnfinishedBacktranslation for execution

ultimate-pa · Feb 28, 2024 · 53c8dc5 · 53c8dc5
1 parent df723e0
commit 53c8dc5
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/...ormatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieBacktranslator.java b/...ormatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieBacktranslator.java
@@ -334,7 +334,9 @@ assert checkCallStackSourceProgramExecution(mLogger,
 		final List<AtomicTraceElement<CACSLLocation>> checkedTranslatedATEs = checkForSubtreeInclusion(translatedATEs);
 		assert checkCallStackTarget(mLogger,
 				checkedTranslatedATEs) : "callstack broken after subtree inclusion reduction";
-		reportUnfinishedBacktranslation("The program execution was not completely translated back.");
+		if (mBacktranslationWarned) {
+			reportUnfinishedBacktranslation("The program execution was not completely translated back.");
+		}
 		return new CACSLProgramExecution(initialState, checkedTranslatedATEs, translatedProgramStates,
 				oldPE.isConcurrent());
 	}