Always use IcfgBuilder and remove RCFGBuilder

releaseScripts/default/adds/Ultimate.py

@@ -519,12 +519,6 @@ def create_cli_settings(prop, validate_witness, witness_type, architecture, inpu
             "--traceabstraction.positions.where.we.compute.the.hoare.annotation"
         )
         ret.append("None")
-        # For now disable UnstructureCode in witness validation
-        # This is a workaround, in the future we always want to disable this.
-        ret.append(
-            "--preprocessor.replace.while.statements.and.if-then-else.statements"
-        )
-        ret.append("false")
         # For YAML violation witnesses, disable procedure inlining
         if witness_type == "violation_witness" and any(i.endswith(".yml") for i in input_files):
             ret.append("--procedureinliner.inline.calls.to.implemented.procedures")

releaseScripts/default/makeFresh.sh

@@ -36,22 +36,22 @@ create_tool_zips() {
   for platform in {linux,win32}; do
     # makeZip <toolname> <targetarch> <reachtc> <termtc> <witnessvaltc> <memsafetytc> <ltlc> <termwitnessvaltc>
     # Taipan
-    exit_on_fail bash makeZip.sh Taipan $platform AutomizerCInline_IcfgBuilder_WitnessPrinter.xml NONE AutomizerCInline_IcfgBuilder.xml AutomizerCInline_IcfgBuilder_WitnessPrinter.xml NONE NONE
+    exit_on_fail bash makeZip.sh Taipan $platform AutomizerCInline_WitnessPrinter.xml NONE AutomizerCInline.xml AutomizerCInline_WitnessPrinter.xml NONE NONE
 
     # Automizer without separate blockencoding plugin
-    exit_on_fail bash makeZip.sh Automizer $platform AutomizerCInline_IcfgBuilder_WitnessPrinter.xml BuchiAutomizerCInline_IcfgBuilder_WitnessPrinter.xml AutomizerCInline_IcfgBuilder.xml AutomizerCInline_IcfgBuilder_WitnessPrinter.xml LTLAutomizerC.xml BuchiAutomizerCInline_IcfgBuilder.xml
+    exit_on_fail bash makeZip.sh Automizer $platform AutomizerCInline_WitnessPrinter.xml BuchiAutomizerCInline_WitnessPrinter.xml AutomizerCInline.xml AutomizerCInline_WitnessPrinter.xml LTLAutomizerC.xml BuchiAutomizerCInline.xml
 
     # Automizer with separate blockencoding plugin
     #exit_on_fail bash makeZip.sh Automizer linux AutomizerC_BE_WitnessPrinter.xml BuchiAutomizerCInline_BE_WitnessPrinter.xml AutomizerC.xml AutomizerC_BE_WitnessPrinter.xml LTLAutomizerC.xml BuchiAutomizerCInline.xml
 
     # Kojak
-    exit_on_fail bash makeZip.sh Kojak $platform KojakC_IcfgBuilder_WitnessPrinter.xml NONE KojakC_IcfgBuilder.xml KojakC_IcfgBuilder_WitnessPrinter.xml NONE NONE
+    exit_on_fail bash makeZip.sh Kojak $platform KojakC_WitnessPrinter.xml NONE KojakC.xml KojakC_WitnessPrinter.xml NONE NONE
 
     # GemCutter
-    exit_on_fail bash makeZip.sh GemCutter $platform AutomizerCInline_IcfgBuilder_WitnessPrinter.xml NONE AutomizerCInline_IcfgBuilder.xml AutomizerCInline_IcfgBuilder_WitnessPrinter.xml NONE NONE
+    exit_on_fail bash makeZip.sh GemCutter $platform AutomizerCInline_WitnessPrinter.xml NONE AutomizerCInline.xml AutomizerCInline_WitnessPrinter.xml NONE NONE
 
     # Referee
-    exit_on_fail bash makeZip.sh Referee $platform RefereeCInline_IcfgBuilder.xml NONE RefereeCInline_IcfgBuilder.xml NONE NONE NONE
+    exit_on_fail bash makeZip.sh Referee $platform RefereeCInline.xml NONE RefereeCInline.xml NONE NONE NONE
 
     # DeltaDebugger
     exit_on_fail bash createDeltaDebuggerDir.sh $platform

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

@@ -11,12 +11,12 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Check\ memory\ neutrality=
 @de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator=0.0.1
 #Mon Sep 29 17:45:36 CEST 2014
-\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Simplify\ code\ blocks=true
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Simplify\ code\ blocks=true
 file_export_version=3.0
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Size\ of\ a\ code\ block=SingleStatement
-@de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=0.0.1
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Convert\ code\ blocks\ to\ CNF=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Size\ of\ a\ code\ block=SingleStatement
+@de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=0.0.1
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Convert\ code\ blocks\ to\ CNF=false
 #Mon Sep 29 17:45:36 CEST 2014
 \!/instance/de.uni_freiburg.informatik.ultimate.plugins.output.jungvisualization=
 file_export_version=3.0

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

@@ -3,7 +3,7 @@
 	<toolchain>
 
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
-	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction"/>
 
 	</toolchain>

trunk/examples/Backtranslation/regression/c/float/AutomizerC.xml

@@ -3,7 +3,7 @@
 <toolchain>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
-	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction"/>
 </toolchain>
 </rundefinition>

trunk/examples/Backtranslation/regression/c/float/AutomizerCInline-Reach-32bit-MathSAT-IcSpLv-Float.epf

@@ -14,15 +14,15 @@
 
 
 #Fri Oct 24 16:34:36 CEST 2014
-\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=
 file_export_version=3.0
-@de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=0.0.1
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Convert\ code\ blocks\ to\ CNF=false
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Size\ of\ a\ code\ block=SingleStatement
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Command\ for\ external\ solver=mathsat\ -unsat_core_generation=3
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Logic\ for\ external\ solver=QF_BVFP
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Dump\ SMT\ script\ to\ file=false
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/To\ the\ following\ directory=./dump/
+@de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=0.0.1
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Convert\ code\ blocks\ to\ CNF=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Size\ of\ a\ code\ block=SingleStatement
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Command\ for\ external\ solver=mathsat\ -unsat_core_generation=3
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Logic\ for\ external\ solver=QF_BVFP
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Dump\ SMT\ script\ to\ file=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/To\ the\ following\ directory=./dump/
 
 
 #Thu Nov 06 16:26:23 CET 2014

trunk/examples/Backtranslation/regression/c/float/AutomizerCInline.xml

@@ -4,6 +4,6 @@
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.procedureinliner"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
-	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction"/>
 </toolchain></rundefinition>

trunk/examples/Backtranslation/regression/c/memsafety/AutomizerC.xml

@@ -4,7 +4,7 @@
 
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
-	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction"/>
 
 	</toolchain>

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

@@ -14,9 +14,9 @@ file_export_version=3.0
 /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=
-@de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=0.0.1
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Convert\ code\ blocks\ to\ CNF=true
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=
+@de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=0.0.1
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Convert\ code\ blocks\ to\ CNF=true
 #Sat Mar 15 16:00:32 CET 2014
 file_export_version=3.0
 @de.uni_freiburg.informatik.ultimate.core=0.0.1

trunk/examples/Backtranslation/regression/c/memsafety/InlineAutomizerC.xml

@@ -5,7 +5,7 @@
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.procedureinliner"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
-	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction"/>
 
 	</toolchain>

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

@@ -14,9 +14,9 @@ file_export_version=3.0
 /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=
-@de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=0.0.1
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Convert\ code\ blocks\ to\ CNF=true
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=
+@de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=0.0.1
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Convert\ code\ blocks\ to\ CNF=true
 #Sat Mar 15 16:00:32 CET 2014
 file_export_version=3.0
 @de.uni_freiburg.informatik.ultimate.core=0.0.1

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

@@ -12,13 +12,13 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=FPandBP
 
 #Sun Nov 08 00:43:17 CET 2015
-\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -t\:10000
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -t\:10000
 file_export_version=3.0
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Dump\ SMT\ script\ to\ file=false
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Size\ of\ a\ code\ block=SequenceOfStatements
-@de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=0.0.1
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Convert\ code\ blocks\ to\ CNF=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Dump\ SMT\ script\ to\ file=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Size\ of\ a\ code\ block=SequenceOfStatements
+@de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=0.0.1
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Convert\ code\ blocks\ to\ CNF=false
 
 #Sun Nov 08 00:43:17 CET 2015
 file_export_version=3.0

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

@@ -12,13 +12,13 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=FPandBP
 
 #Sun Nov 08 00:43:17 CET 2015
-\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -t\:10000
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -t\:10000
 file_export_version=3.0
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Dump\ SMT\ script\ to\ file=false
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Size\ of\ a\ code\ block=SequenceOfStatements
-@de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=0.0.1
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Convert\ code\ blocks\ to\ CNF=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Dump\ SMT\ script\ to\ file=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Size\ of\ a\ code\ block=SequenceOfStatements
+@de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=0.0.1
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Convert\ code\ blocks\ to\ CNF=false
 
 #Sun Nov 08 00:43:17 CET 2015
 file_export_version=3.0

trunk/examples/Backtranslation/regression/c/standard/GenericAutomizerC.xml

@@ -4,7 +4,7 @@
 
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
-	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction"/>
 
 	</toolchain>

trunk/examples/Backtranslation/regression/c/standard/GenericAutomizerCInline.xml

@@ -5,7 +5,7 @@
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.procedureinliner"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
-	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction"/>
 
 	</toolchain>

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

@@ -12,13 +12,13 @@ file_export_version=3.0
 /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Compute\ Interpolants\ along\ a\ Counterexample=FPandBP
 
 #Sun Nov 08 00:43:17 CET 2015
-\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -t\:10000
+\!/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Command\ for\ external\ solver=z3 SMTLIB2_COMPLIANT\=true -memory\:2024 -smt2 -in -t\:10000
 file_export_version=3.0
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Dump\ SMT\ script\ to\ file=false
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Size\ of\ a\ code\ block=SingleStatement
-@de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder=0.0.1
-/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Convert\ code\ blocks\ to\ CNF=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Dump\ SMT\ script\ to\ file=false
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Size\ of\ a\ code\ block=SingleStatement
+@de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder=0.0.1
+/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder/Convert\ code\ blocks\ to\ CNF=false
 
 #Sun Nov 08 00:43:17 CET 2015
 file_export_version=3.0

trunk/examples/Backtranslation/regression/c/standard/GenericBEAutomizerC.xml

@@ -4,7 +4,7 @@
 
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
-	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.blockencoding"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction"/>
 

trunk/examples/Backtranslation/regression/c/standard/GenericBEKojakC.xml

@@ -4,7 +4,7 @@
 
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
-	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.blockencoding"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.codecheck"/>
 

trunk/examples/Backtranslation/regression/c/standard/GenericKojakC.xml

@@ -4,7 +4,7 @@
 
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
-	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.codecheck"/>
 
 	</toolchain>

trunk/examples/Backtranslation/regression/c/standard/GenericKojakCInline.xml

@@ -5,7 +5,7 @@
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.procedureinliner"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.boogie.preprocessor"/>
-	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder"/>
+	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.icfgbuilder"/>
 	<plugin id="de.uni_freiburg.informatik.ultimate.plugins.generator.codecheck"/>
 
 	</toolchain>

trunk/examples/Backtranslation/regression/c/standard/Globals_GenericAutomizerCInline_Generic.errorpath

@@ -1,18 +1,15 @@
 [L3]               int a = 5;
 [L4]               int x = 0;
-       VAL         [a=5, x=0]
 [L13]  EXPR        a++
 [L13]  CALL, EXPR  f(a++)
 [L7]   EXPR        ++b
 [L7]               x = ++b
 [L8]               return x;
-       VAL         [\result=6, a=6, x=6]
 [L13]  RET, EXPR   f(a++)
 [L13]  CALL, EXPR  f(f(a++))
 [L7]   EXPR        ++b
 [L7]               x = ++b
 [L8]               return x;
-       VAL         [\result=7, a=6, x=7]
 [L13]  RET, EXPR   f(f(a++))
 [L13]              a = f(f(a++))
 [L15]  COND TRUE   a == x

trunk/examples/Backtranslation/regression/c/standard/Globals_GenericKojakCInline_Generic.errorpath

@@ -1,18 +1,15 @@
 [L3]               int a = 5;
 [L4]               int x = 0;
-       VAL         [a=5, x=0]
 [L13]  EXPR        a++
 [L13]  CALL, EXPR  f(a++)
 [L7]   EXPR        ++b
 [L7]               x = ++b
 [L8]               return x;
-       VAL         [\result=6, a=6, x=6]
 [L13]  RET, EXPR   f(a++)
 [L13]  CALL, EXPR  f(f(a++))
 [L7]   EXPR        ++b
 [L7]               x = ++b
 [L8]               return x;
-       VAL         [\result=7, a=6, x=7]
 [L13]  RET, EXPR   f(f(a++))
 [L13]              a = f(f(a++))
 [L15]  COND TRUE   a == x

trunk/examples/Backtranslation/regression/c/standard/Loops.errorpath

@@ -42,10 +42,12 @@
        VAL         [a=0, c=0, d=0, e=0, f=2]
 [L23]  COND FALSE  !(d>0)
        VAL         [a=0, c=0, e=0, f=2]
+[L29]  COND TRUE   f>0
 [L28]              f--
        VAL         [a=0, c=0, e=0, f=1]
 [L29]  COND TRUE   f>0
        VAL         [a=0, c=0, e=0, f=1]
+[L29]  COND TRUE   f>0
 [L28]              f--
        VAL         [a=0, c=0, e=0, f=0]
 [L29]  COND FALSE  !(f>0)

trunk/examples/Backtranslation/regression/c/standard/Loops_GenericBEAutomizerC_Generic.errorpath

@@ -42,9 +42,11 @@
        VAL         [a=0, c=0, d=0, e=0, f=2]
 [L23]  COND FALSE  !(d>0)
        VAL         [a=0, c=0, e=0, f=2]
+[L29]  COND TRUE   f>0
 [L28]              f--
 [L29]  COND TRUE   f>0
        VAL         [a=0, c=0, e=0, f=1]
+[L29]  COND TRUE   f>0
 [L28]              f--
 [L29]  COND FALSE  !(f>0)
 [L32]  COND TRUE   a == 0