remove unused method IAbstractPredicate::getProcedures

It is not clearly defined (let alone documented) what the procedures
of a predicate are. Since this method is not used (except to provide
procedures to other predicates), this commit removes it.

Also remove procedure collection from TermVarsProc, as this was only
used to provide procedures for IPredicates. Consequently, rename the
class TermVarsFuns to reflect its current functionality.

trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/algorithm/rcfg/RcfgDebugHelper.java

@@ -17,7 +17,7 @@
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.AbsIntPredicate;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.BasicPredicate;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate;
-import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsProc;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsFuns;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.IncrementalPlicationChecker.Validity;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.logic.Term;
@@ -87,9 +87,10 @@ private boolean isPostSound(final IPredicate precondHier, final ACTION transitio
 
 	private IPredicate createPredicateFromState(final DisjunctiveAbstractState<STATE> state) {
 		final Term acc = state.getTerm(mMgdScript.getScript());
-		final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(acc, mMgdScript, mSymbolTable);
-		return new AbsIntPredicate<>(new BasicPredicate(getIllegalPredicateId(), tvp.getProcedures(), acc,
-				tvp.getVars(), tvp.getFuns(), tvp.getClosedFormula()), state);
+		final TermVarsFuns tvp = TermVarsFuns.computeTermVarsFuns(acc, mMgdScript, mSymbolTable);
+		return new AbsIntPredicate<>(
+				new BasicPredicate(getIllegalPredicateId(), acc, tvp.getVars(), tvp.getFuns(), tvp.getClosedFormula()),
+				state);
 	}
 
 	private static int getIllegalPredicateId() {

trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/arraytheory/SMTTheoryStateFactoryAndPredicateHelper.java

@@ -42,7 +42,7 @@
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.BasicPredicate;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.BasicPredicateFactory;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate;
-import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsProc;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsFuns;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils.SimplificationTechnique;
@@ -123,7 +123,7 @@ private IPredicate getOrConstructPredicate(final Term resTerm, final Set<IProgra
 					.collect(Collectors.toSet());
 			mMgdScript.lock(this);
 			mMgdScript.push(this, 1);
-			final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(resTerm, mMgdScript, mCsToolkit.getSymbolTable());
+			final TermVarsFuns tvp = TermVarsFuns.computeTermVarsFuns(resTerm, mMgdScript, mCsToolkit.getSymbolTable());
 			mMgdScript.assertTerm(this, tvp.getClosedFormula());
 //					PredicateUtils.computeClosedFormula(resTerm, vars, mMgdScript.getScript()));
 			final LBool checkSatResult = mMgdScript.checkSat(this);
@@ -241,7 +241,7 @@ public boolean impliesLiteral(final SMTTheoryState arrayTheoryState, final Term
 		mMgdScript.lock(this);
 		mMgdScript.push(this, 1);
 		mMgdScript.assertTerm(this, arrayTheoryState.getPredicate().getClosedFormula());
-		final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(literalTerm, mMgdScript, mCsToolkit.getSymbolTable());
+		final TermVarsFuns tvp = TermVarsFuns.computeTermVarsFuns(literalTerm, mMgdScript, mCsToolkit.getSymbolTable());
 		mMgdScript.assertTerm(this, SmtUtils.not(mMgdScript.getScript(), tvp.getClosedFormula()));
 		final LBool checkSatResult = mMgdScript.checkSat(this);
 		mMgdScript.pop(this, 1);

trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/EqPredicate.java

@@ -38,7 +38,7 @@
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramFunction;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramVar;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate;
-import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsProc;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsFuns;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SubTermFinder;
@@ -54,24 +54,22 @@
 public class EqPredicate implements IPredicate {
 
 	private final EqDisjunctiveConstraint<EqNode> mConstraint;
-	private final String[] mProcedures;
 	private final ImmutableSet<IProgramVar> mVars;
 	private final ImmutableSet<IProgramFunction> mFuns;
 	private final Term mClosedFormula;
 	private final Term mFormula;
 	private EqNodeAndFunctionFactory mEqNodeAndFunctionFactory;
 
 	public EqPredicate(final EqDisjunctiveConstraint<EqNode> constraint, final ImmutableSet<IProgramVar> vars,
-			final String[] procedures, final IIcfgSymbolTable symbolTable, final ManagedScript mgdScript,
+			final IIcfgSymbolTable symbolTable, final ManagedScript mgdScript,
 			final EqNodeAndFunctionFactory eqNodeAndFunctionFactory) {
 		assert vars != null;
 		assert vars.stream().allMatch(Objects::nonNull);
 		mConstraint = constraint;
 		mVars = vars;
-		mProcedures = procedures;
 
 		final Term constraintFormula = constraint.getTerm(mgdScript.getScript());
-		final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(constraintFormula, mgdScript,	symbolTable);
+		final TermVarsFuns tvp = TermVarsFuns.computeTermVarsFuns(constraintFormula, mgdScript,	symbolTable);
 		mFuns = ImmutableSet.copyOf(tvp.getFuns());
 
 //		final Term literalDisequalities = getLiteralDisequalities(constraint, mgdScript);
@@ -83,23 +81,20 @@ public EqPredicate(final EqDisjunctiveConstraint<EqNode> constraint, final Immut
 		mFormula = SmtUtils.and(mgdScript.getScript(), literalDisequalities, tvp.getFormula());
 	}
 
-
-
 	public EqPredicate(final Term formula, final ImmutableSet<IProgramVar> vars,
-			final ImmutableSet<IProgramFunction> funs, final String[] procedures, final IIcfgSymbolTable symbolTable,
+			final ImmutableSet<IProgramFunction> funs, final IIcfgSymbolTable symbolTable,
 			final ManagedScript mgdScript, final EqNodeAndFunctionFactory eqNodeAndFunctionFactory,
 			final EqConstraintFactory<EqNode> eqConstraintFactory) {
 		mConstraint = null;
 		assert vars.stream().allMatch(Objects::nonNull);
 		mVars = vars;
 		mFuns = funs;
-		mProcedures = procedures;
 
 		mEqNodeAndFunctionFactory = eqNodeAndFunctionFactory;
 
 
 		final Term acc = formula;
-		final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(acc, mgdScript, symbolTable);
+		final TermVarsFuns tvp = TermVarsFuns.computeTermVarsFuns(acc, mgdScript, symbolTable);
 
 //		final Term literalDisequalities = getLiteralDisequalities(constraint, mgdScript);
 
@@ -134,12 +129,6 @@ private Set<Term> collectLiteralsInFormula(final Term formula) {
 //		return literalDisequalities;
 //	}
 
-
-	@Override
-	public String[] getProcedures() {
-		return mProcedures;
-	}
-
 	@Override
 	public ImmutableSet<IProgramVar> getVars() {
 		return mVars;

trunk/source/AbstractInterpretationV2/src/de/uni_freiburg/informatik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/EqStateFactory.java

@@ -123,13 +123,9 @@ public ManagedScript getManagedScript() {
 	}
 
 	public EqPredicate stateToPredicate(final EqState state) {
-		// TODO: what procedures does the predicate need?
 		return new EqPredicate(
 				getEqConstraintFactory().getDisjunctiveConstraint(Collections.singleton(state.getConstraint())),
-				state.getConstraint().getVariables(getSymbolTable()),
-				null,
-				getSymbolTable(),
-				getManagedScript(),
+				state.getConstraint().getVariables(getSymbolTable()), getSymbolTable(), getManagedScript(),
 				mEqNodeAndFunctionFactory);
 	}
 
@@ -142,16 +138,15 @@ public EqPredicate statesToPredicate(final List<EqState> states) {
 			constraints.add(state.getConstraint());
 		}
 
-		// TODO: what procedures does the predicate need?
 		return new EqPredicate(getEqConstraintFactory().getDisjunctiveConstraint(constraints),
-				ImmutableSet.of(variables), null, getSymbolTable(), getManagedScript(), mEqNodeAndFunctionFactory);
+				ImmutableSet.of(variables), getSymbolTable(), getManagedScript(), mEqNodeAndFunctionFactory);
 	}
 
 	public EqPredicate termToPredicate(final Term spPrecise,
 			final IPredicate postConstraint) {
 		return new EqPredicate(spPrecise, ImmutableSet.copyOf(postConstraint.getVars()),
-				ImmutableSet.copyOf(postConstraint.getFuns()), postConstraint.getProcedures(), mSymbolTable, mMgdScript,
-				mEqNodeAndFunctionFactory, mEqConstraintFactory);
+				ImmutableSet.copyOf(postConstraint.getFuns()), mSymbolTable, mMgdScript, mEqNodeAndFunctionFactory,
+				mEqConstraintFactory);
 
 	}
 

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

@@ -201,8 +201,8 @@ public AxiomTransformationResult transform(final IPredicate oldAxioms) {
 		// Quantify auxiliary variables
 		final Term withoutAuxVars = SmtUtils.quantifier(mMgdScript.getScript(), QuantifiedFormula.EXISTS,
 				result.getSecond(), result.getFirst());
-		final IPredicate transformedAxiom = new BasicPredicate(0, new String[0], withoutAuxVars, Collections.emptySet(),
-				oldAxioms.getFuns(), withoutAuxVars);
+		final IPredicate transformedAxiom =
+				new BasicPredicate(0, withoutAuxVars, Collections.emptySet(), oldAxioms.getFuns(), withoutAuxVars);
 		final boolean isOverappoximation = result.getThird();
 		return new AxiomTransformationResult(transformedAxiom, isOverappoximation);
 	}

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

@@ -69,7 +69,7 @@
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramVar;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramVarOrConst;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate;
-import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsProc;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsFuns;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils;
 import de.uni_freiburg.informatik.ultimate.logic.Term;
@@ -526,7 +526,7 @@ private SmtFunctionsAndAxioms transformSmtFunctionsAndAxioms(final SmtFunctionsA
 		newAxiomsClosed.add(translationResult.getAxiom().getClosedFormula());
 
 		final Term newAxioms = SmtUtils.and(script.getScript(), newAxiomsClosed);
-		final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(newAxioms, mgdScript, symbolTable);
+		final TermVarsFuns tvp = TermVarsFuns.computeTermVarsFuns(newAxioms, mgdScript, symbolTable);
 		return new SmtFunctionsAndAxioms(newAxioms, tvp.getFuns(), script);
 	}
 

trunk/source/Library-IcfgTransformer/src/de/uni_freiburg/informatik/ultimate/icfgtransformer/loopacceleration/qvasr/QvasrSummarizer.java

@@ -229,8 +229,8 @@ public static UnmodifiableTransFormula intVasrAbstractionToFormula(final Managed
 				}
 			}
 		}
-		final IPredicate guardPred = new BasicPredicate(0, new String[0], script.getScript().term("true"),
-				Collections.emptySet(), Collections.emptySet(), script.getScript().term("true"));
+		final IPredicate guardPred = new BasicPredicate(0, script.getScript().term("true"), Collections.emptySet(),
+				Collections.emptySet(), script.getScript().term("true"));
 		final Term post = predTransformer.strongestPostcondition(guardPred, tf);
 		final Term postSub = Substitution.apply(script, defaultToOut, post);
 		qvasrDimensionConjunction.add(postSub);

trunk/source/Library-LassoRanker/src/de/uni_freiburg/informatik/ultimate/lassoranker/preprocessors/rewriteArrays/EqualitySupportingInvariantAnalysis.java

@@ -38,7 +38,7 @@
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.BasicPredicate;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.PredicateUtils;
-import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsProc;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsFuns;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.logic.QuotedObject;
 import de.uni_freiburg.informatik.ultimate.logic.Script.LBool;
@@ -148,12 +148,12 @@ private boolean isInVariant(final Doubleton<Term> definingDoubleton, final boole
 		} else {
 			invariantCandidateTerm = EqualityAnalysisResult.notEqualTerm(mScript.getScript(), definingDoubleton);
 		}
-		final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(invariantCandidateTerm, mScript, mSymbolTable);
-		final IPredicate invariantCandidate = new BasicPredicate(0, tvp.getProcedures(), tvp.getFormula(),
-				tvp.getVars(), tvp.getFuns(), tvp.getClosedFormula());
+		final TermVarsFuns tvp = TermVarsFuns.computeTermVarsFuns(invariantCandidateTerm, mScript, mSymbolTable);
+		final IPredicate invariantCandidate =
+				new BasicPredicate(0, tvp.getFormula(), tvp.getVars(), tvp.getFuns(), tvp.getClosedFormula());
 		final Set<IProgramVar> emptyVarSet = Collections.emptySet();
-		final IPredicate truePredicate = new BasicPredicate(0, new String[0], mScript.getScript().term("true"),
-				emptyVarSet, Collections.emptySet(), mScript.getScript().term("true"));
+		final IPredicate truePredicate = new BasicPredicate(0, mScript.getScript().term("true"), emptyVarSet,
+				Collections.emptySet(), mScript.getScript().term("true"));
 		final LBool impliedByStem = PredicateUtils.isInductiveHelper(mScript.getScript(), truePredicate,
 				invariantCandidate, mOriginalStem, mModifiableGlobalsAtStart, mModifiableGlobalsAtHonda);
 		if (impliedByStem == LBool.UNSAT) {

trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/boogie/Boogie2SMT.java

@@ -43,7 +43,7 @@
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.SmtFunctionsAndAxioms;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramVar;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.ProgramConst;
-import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsProc;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsFuns;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.scripttransfer.HistoryRecordingScript;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils;
@@ -90,7 +90,7 @@ public Boogie2SMT(final ManagedScript mgdScript, final BoogieDeclarations boogie
 
 		final List<Term> axiomList = declareAxioms(boogieDeclarations, script, mExpression2Term,
 				mBoogie2SmtSymbolTable);
-		final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(SmtUtils.and(script, axiomList), mScript,
+		final TermVarsFuns tvp = TermVarsFuns.computeTermVarsFuns(SmtUtils.and(script, axiomList), mScript,
 				mBoogie2SmtSymbolTable);
 		assert tvp.getVars().isEmpty() : "axioms must not have variables";
 		if (!(script instanceof HistoryRecordingScript)) {

trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/cfg/SmtFunctionsAndAxioms.java

@@ -37,7 +37,7 @@
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramFunction;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.BasicPredicate;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate;
-import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsProc;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsFuns;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.scripttransfer.DeclarableFunctionSymbol;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.scripttransfer.HistoryRecordingScript;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.scripttransfer.ISmtDeclarable;
@@ -102,8 +102,8 @@ public SmtFunctionsAndAxioms(final ManagedScript mgdScript) {
 	 */
 	public SmtFunctionsAndAxioms(final Term axioms, final Set<IProgramFunction> funs,
 			final ManagedScript mgdScript) {
-		this(new BasicPredicate(HARDCODED_SERIALNUMBER_FOR_AXIOMS, new String[0], axioms, Collections.emptySet(), funs,
-				axioms), mgdScript);
+		this(new BasicPredicate(HARDCODED_SERIALNUMBER_FOR_AXIOMS, axioms, Collections.emptySet(), funs, axioms),
+				mgdScript);
 	}
 
 	/**
@@ -122,8 +122,6 @@ public SmtFunctionsAndAxioms(final IPredicate axioms, final ManagedScript mgdScr
 				HistoryRecordingScript.extractHistoryRecordingScript(Objects.requireNonNull(mgdScript.getScript())));
 		assert axioms.getClosedFormula() == axioms.getFormula() : "Axioms are not closed";
 		assert axioms.getFormula().getFreeVars().length == 0 : "Axioms are not closed";
-		assert axioms.getProcedures() != null;
-
 	}
 
 	/**
@@ -137,9 +135,9 @@ public SmtFunctionsAndAxioms addAxiom(final Term additionalAxioms, final IIcfgSy
 		// TODO: Use an Ultimate result to report inconsistent axioms; we do not want to disallow inconsistent axioms,
 		// we just want to be informed about them.
 		assert quickCheckAxioms != LBool.UNSAT : "Axioms are inconsistent";
-		final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(newAxioms, mMgdScript, symbolTable);
-		final IPredicate newAxiomsPred = new BasicPredicate(HARDCODED_SERIALNUMBER_FOR_AXIOMS, tvp.getProcedures(),
-				tvp.getFormula(), tvp.getVars(), tvp.getFuns(), tvp.getClosedFormula());
+		final TermVarsFuns tvp = TermVarsFuns.computeTermVarsFuns(newAxioms, mMgdScript, symbolTable);
+		final IPredicate newAxiomsPred = new BasicPredicate(HARDCODED_SERIALNUMBER_FOR_AXIOMS, tvp.getFormula(),
+				tvp.getVars(), tvp.getFuns(), tvp.getClosedFormula());
 		return new SmtFunctionsAndAxioms(newAxiomsPred, mMgdScript);
 	}
 

trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/cfg/transitions/TransFormulaBuilder.java

@@ -45,7 +45,7 @@
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.cfg.variables.IProgramVar;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.TransferrerWithVariableCache;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.IPredicate;
-import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsProc;
+import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.predicates.TermVarsFuns;
 import de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.scripttransfer.TermTransferrer;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript;
 import de.uni_freiburg.informatik.ultimate.lib.smtlibutils.SmtUtils;
@@ -451,7 +451,7 @@ private static UnmodifiableTransFormula constructEquality(final List<? extends I
 			if (!consts.isEmpty()) {
 				throw new UnsupportedOperationException("constants not yet supported");
 			}
-			final TermVarsProc tvp = TermVarsProc.computeTermVarsProc(rhs.get(i), mgdScript, symbolTable);
+			final TermVarsFuns tvp = TermVarsFuns.computeTermVarsFuns(rhs.get(i), mgdScript, symbolTable);
 			rhsPvs.addAll(tvp.getVars());
 		}
 

trunk/source/Library-ModelCheckerUtils/src/de/uni_freiburg/informatik/ultimate/lib/modelcheckerutils/smt/TransferrerWithVariableCache.java

@@ -105,8 +105,8 @@ private BasicPredicate transferPredicateHelper(final IPredicate predicate) {
 		final Set<IProgramFunction> functions = predicate.getFuns();
 		final Term transferredFormula = transferTerm(predicate.getFormula());
 		final Term transferredClosed = transferTerm(predicate.getClosedFormula());
-		return mFactory.construct(serial -> new BasicPredicate(serial, predicate.getProcedures(), transferredFormula,
-				variables, functions, transferredClosed));
+		return mFactory.construct(
+				serial -> new BasicPredicate(serial, transferredFormula, variables, functions, transferredClosed));
 	}
 
 	public <T extends Term> T transferTerm(final T term) {