#295, add method to TransformedIcfgBuilder that is needed for its use…

… in IcfgTransitionTransformer (scan created transformulas for fresh variables even when there is a corresponding formula in the old icfg)

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/TransformedIcfgBuilder.java

@@ -60,6 +60,7 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transitions.TransFormulaBuilder;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transitions.UnmodifiableTransFormula;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramConst;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramOldVar;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVar;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVarOrConst;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.managedscript.ManagedScript;
@@ -160,6 +161,24 @@ public IcfgEdge createNewTransition(final OUTLOC newSource, final OUTLOC newTarg
 		return newTransition;
 	}
 
+	/**
+	 * Just like {@link createNewTransition} but in addition scans the new TransFormula for program variables that do
+	 * not yet have an entry in the symbol table. Schedules those program variables for adding them to the result icfg's
+	 * symbol table.
+	 *
+	 * @param newSource
+	 * @param newTarget
+	 * @param oldTransition
+	 * @return
+	 */
+	public IcfgEdge createNewTransitionWithNewProgramVars(final OUTLOC newSource, final OUTLOC newTarget,
+			final IcfgEdge oldTransition) {
+		final IcfgEdge newTransition = createNewTransition(newSource, newTarget, oldTransition);
+		rememberNewVariables(newTransition.getTransformula());
+		return newTransition;
+	}
+
+
 	/**
 	 * @return true if the corresponding call was already created and one can safely create a new transition for this
 	 *         return transition.
@@ -201,8 +220,17 @@ public IcfgInternalTransition createNewInternalTransition(final OUTLOC source, f
 	private void rememberNewVariables(final UnmodifiableTransFormula transformula) {
 		final IIcfgSymbolTable symbolTable = mOriginalIcfg.getCfgSmtToolkit().getSymbolTable();
 
+		/**
+		 * Checks if a given IProgramVar is already present in the symbolTable.
+		 */
 		final Predicate<Entry<IProgramVar, TermVariable>> checkVar = a -> {
 			final IProgramVar invar = a.getKey();
+
+			if (invar instanceof IProgramOldVar) {
+				// oldvars are not added to the symbol table
+				return true;
+			}
+
 			if (invar.getProcedure() == null) {
 				// should be a global
 				if (symbolTable.getGlobals().contains(invar)) {