Proof Refactoring

releaseScripts/default/adds/Ultimate.py

@@ -508,9 +508,9 @@ def create_cli_settings(prop, validate_witness, architecture, c_file):
         # we need to disable hoare triple generation as workaround for an internal bug
         # but only for reachability witness validation
         ret.append(
-            "--traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg"
+            "--traceabstraction.positions.where.we.compute.the.hoare.annotation"
         )
-        ret.append("false")
+        ret.append("None")
     elif not validate_witness:
         # we are not in validation mode, so we should generate a witness and need
         # to pass some things to the witness printer

releaseScripts/legacy/201505ChinmayNarayan/AutomizerConcurrentDefaultSettings.epf

@@ -2,6 +2,6 @@
 file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Size\ of\ a\ code\ block=SingleStatement
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/SMT\ solver=Internal_SMTInterpol
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=None
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=Craig_TreeInterpolation
 /instance/UltimateCore/Generate\ benchmark\ results=false

releaseScripts/legacy/termcomp2014/settings.epf

@@ -47,4 +47,4 @@ file_export_version=3.0
 file_export_version=3.0
 @de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=0.0.1
 \!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=true
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=All

releaseScripts/website-config/backend/settings_whitelist.json

@@ -2,7 +2,6 @@
 	"de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction": [
 		"SMT solver",
 		"Compute Interpolants along a Counterexample",
-		"Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
 		"Positions where we compute the Hoare Annotation",
 		"Trace refinement exception blacklist",
 		"Trace refinement strategy",

releaseScripts/website-config/frontend/config.js

@@ -212,15 +212,6 @@ const _CONFIG = {
 							"default": "External_ModelsAndUnsatCoreMode",
 							"type": "string"
 						},
-						{
-							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
-							"name": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"key": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"id": "traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg",
-							"visible": false,
-							"default": true,
-							"type": "bool"
-						},
 						{
 							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
 							"name": "Positions where we compute the Hoare Annotation",
@@ -354,15 +345,6 @@ const _CONFIG = {
 							"default": "External_ModelsAndUnsatCoreMode",
 							"type": "string"
 						},
-						{
-							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
-							"name": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"key": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"id": "traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg",
-							"visible": false,
-							"default": true,
-							"type": "bool"
-						},
 						{
 							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
 							"name": "Positions where we compute the Hoare Annotation",
@@ -637,15 +619,6 @@ const _CONFIG = {
 							"default": "External_ModelsAndUnsatCoreMode",
 							"type": "string"
 						},
-						{
-							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
-							"name": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"key": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"id": "traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg",
-							"visible": false,
-							"default": true,
-							"type": "bool"
-						},
 						{
 							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
 							"name": "Positions where we compute the Hoare Annotation",
@@ -779,15 +752,6 @@ const _CONFIG = {
 							"default": "External_ModelsAndUnsatCoreMode",
 							"type": "string"
 						},
-						{
-							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
-							"name": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"key": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"id": "traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg",
-							"visible": false,
-							"default": true,
-							"type": "bool"
-						},
 						{
 							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
 							"name": "Positions where we compute the Hoare Annotation",
@@ -1100,15 +1064,6 @@ const _CONFIG = {
 							"default": "USE_PREDICATES",
 							"type": "string"
 						},
-						{
-							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
-							"name": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"key": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"id": "traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg",
-							"visible": false,
-							"default": true,
-							"type": "bool"
-						},
 						{
 							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
 							"name": "Positions where we compute the Hoare Annotation",
@@ -1224,15 +1179,6 @@ const _CONFIG = {
 							"default": "USE_PREDICATES",
 							"type": "string"
 						},
-						{
-							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
-							"name": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"key": "Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG",
-							"id": "traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg",
-							"visible": false,
-							"default": true,
-							"type": "bool"
-						},
 						{
 							"plugin_id": "de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction",
 							"name": "Positions where we compute the Hoare Annotation",

trunk/examples/Arrays/regression/MonniauxAutomizerBplDefault.epf

@@ -18,8 +18,7 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Use\ separate\ solver\ for\ trace\ checks=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/SMT\ solver=External_ModelsAndUnsatCoreMode
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=false
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=LoopHeads
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=None
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ strategy=FIXED_PREFERENCES
 
 

trunk/examples/Backtranslation/regression/bpl/AutomizerBpl.epf

@@ -1,6 +1,6 @@
 #Mon Sep 29 17:45:36 CEST 2014
 \!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=None
 file_export_version=3.0
 @de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=0.0.1
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=ForwardPredicates

trunk/examples/Backtranslation/regression/c/memsafety/AutomizerC_ForwardPredicates_SvcompMemsafety.epf

@@ -13,7 +13,7 @@ file_export_version=3.0
 @de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=0.0.1
 \!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=ForwardPredicates
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=None
 #Wed Jan 15 21:36:24 CET 2014
 file_export_version=3.0
 \!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=

trunk/examples/Backtranslation/regression/c/memsafety/InlineAutomizerC_ForwardPredicates_SvcompMemsafety.epf

@@ -13,7 +13,7 @@ file_export_version=3.0
 @de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=0.0.1
 \!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=ForwardPredicates
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=None
 #Wed Jan 15 21:36:24 CET 2014
 file_export_version=3.0
 \!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=

trunk/examples/Backtranslation/regression/c/standard/Generic.epf

@@ -36,7 +36,6 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Use\ separate\ solver\ for\ trace\ checks=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/SMT\ solver=External_ModelsAndUnsatCoreMode
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=LoopHeads
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ strategy=PENGUIN
 

trunk/examples/Backtranslation/regression/c/standard/GenericBE.epf

@@ -36,7 +36,6 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Use\ separate\ solver\ for\ trace\ checks=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/SMT\ solver=External_ModelsAndUnsatCoreMode
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=LoopHeads
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ strategy=PENGUIN
 

trunk/examples/CToBoogieTranslation/svcomp2019automizer_constarray/svcomp-Reach-32bit-Automizer_Default_ConstArrays.epf

@@ -43,7 +43,6 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Use\ separate\ solver\ for\ trace\ checks=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/SMT\ solver=External_ModelsAndUnsatCoreMode
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=LoopHeads
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ strategy=CAMEL
 

trunk/examples/CToBoogieTranslation/svcomp2019automizer_constarray/svcomp-Reach-32bit-Automizer_Default_Select.epf

@@ -43,7 +43,6 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Use\ separate\ solver\ for\ trace\ checks=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/SMT\ solver=External_ModelsAndUnsatCoreMode
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=LoopHeads
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ strategy=CAMEL
 

trunk/examples/CToBoogieTranslation/svcomp2019automizer_constarray/svcomp-Reach-32bit-Automizer_Default_StoreChains.epf

@@ -43,7 +43,6 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Use\ separate\ solver\ for\ trace\ checks=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/SMT\ solver=External_ModelsAndUnsatCoreMode
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=true
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=LoopHeads
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ strategy=CAMEL
 

trunk/examples/Interactive/settings/GuiResetSettingsExported.epf

@@ -280,7 +280,6 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Assert\ CodeBlocks=NOT_INCREMENTALLY
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Automaton\ type\ used\ in\ concurrency\ analysis=FINITE_AUTOMATA
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:1024 -smt2 -in -t\:12000
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=false
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=ForwardPredicates
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Counterexample\ search\ strategy=BFS
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/DifferenceSenwa\ operation\ instead\ classical\ Difference=false
@@ -303,7 +302,7 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Number\ of\ iteration\ whose\ artifact\ is\ visualized=1000000
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Order\ in\ Petri\ net\ unfolding=Esparza R\u00F6mer Vogler
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Output\ format\ of\ dumped\ automata=ATS
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=All
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=None
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Refine\ always\ when\ using\ abstract\ interpretation=false
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/SMT\ solver=Internal_SMTInterpol
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Simplification\ technique=SIMPLIFY_DDA

trunk/examples/Interactive/settings/ResetSettingsCamel.epf

@@ -275,7 +275,7 @@ file_export_version=3.0
 file_export_version=3.0
 #Thu Feb 16 15:47:28 CET 2017
 \!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=None
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/DifferenceSenwa\ operation\ instead\ classical\ Difference=false
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Dump\ SMT\ script\ to\ file=false
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Dump\ automata\ to\ files=false

trunk/examples/Interactive/settings/ResetSettingsCamelCannibalize.epf

@@ -188,7 +188,7 @@ file_export_version=3.0
 file_export_version=3.0
 #Wed May 10 01:11:15 CEST 2017
 \!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=None
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/DifferenceSenwa\ operation\ instead\ classical\ Difference=false
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Dump\ SMT\ script\ to\ file=false
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Dump\ automata\ to\ files=false

trunk/examples/Interactive/settings/ResetSettingsCamelNoEnhancment.epf

@@ -188,7 +188,7 @@ file_export_version=3.0
 file_export_version=3.0
 #Wed May 10 01:08:21 CEST 2017
 \!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction=
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Hoare\ Annotation\ of\ negated\ interpolant\ automaton,\ abstraction\ and\ CFG=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Positions\ where\ we\ compute\ the\ Hoare\ Annotation=None
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/DifferenceSenwa\ operation\ instead\ classical\ Difference=false
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Dump\ SMT\ script\ to\ file=false
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Dump\ automata\ to\ files=false