#295, incremental improvement towards the new heap separator

ultimate-pa · Jan 15, 2018 · bf31b64 · bf31b64
1 parent 35a6b97
commit bf31b64
Show file tree

Hide file tree

Showing 9 changed files with 121 additions and 60 deletions.
diff --git a/...k/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/VPDomain.java b/...k/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/VPDomain.java
@@ -79,6 +79,15 @@ public class VPDomain<ACTION extends IIcfgTransition<IcfgLocation>>
 
 	private final VPDomainBenchmark mBenchmark;
 
+	/**
+	 *
+	 * @param logger
+	 * @param services
+	 * @param csToolkit
+	 * @param additionalLiterals
+	 * 			This set of program constants will be viewed as "literals" by the analysis. Literals are constants that
+	 *          are unequal from all other constants.
+	 */
 	public VPDomain(final ILogger logger, final IUltimateServiceProvider services, final CfgSmtToolkit csToolkit,
 			final Set<IProgramConst> additionalLiterals) {
 		mLogger = logger;
@@ -91,7 +100,7 @@ public VPDomain(final ILogger logger, final IUltimateServiceProvider services, f
 
 		final IPreferenceProvider ups = mServices.getPreferenceProvider(Activator.PLUGIN_ID);
 
-		mEqNodeAndFunctionFactory = new EqNodeAndFunctionFactory(services, mManagedScript);
+		mEqNodeAndFunctionFactory = new EqNodeAndFunctionFactory(services, mManagedScript, additionalLiterals);
 		mEqConstraintFactory = new EqConstraintFactory<>(mEqNodeAndFunctionFactory, mServices, mManagedScript,
 				prepareWeqSettings(ups), mDebugMode);
 		mEqStateFactory = new EqStateFactory(mEqNodeAndFunctionFactory, mEqConstraintFactory, mSymboltable,

diff --git a/...i_freiburg/informatik/ultimate/plugins/icfgtransformation/IcfgTransformationObserver.java b/...i_freiburg/informatik/ultimate/plugins/icfgtransformation/IcfgTransformationObserver.java
@@ -198,8 +198,8 @@ private <INLOC extends IcfgLocation, OUTLOC extends IcfgLocation> IIcfg<OUTLOC>
 			final IEqualityAnalysisResultProvider<IcfgLocation, IIcfg<?>> equalityProvider) {
 
 		final HeapSepIcfgTransformer<INLOC, OUTLOC> icfgTransformer =
-				new HeapSepIcfgTransformer<>(icfg, locFac, backtranslationTracker, outlocClass, "heap_separated_icfg",
-						equalityProvider);
+				new HeapSepIcfgTransformer<>(icfg, locFac, fac, backtranslationTracker, outlocClass,
+						"heap_separated_icfg", equalityProvider);
 
 		mServices.getResultService().reportResult(Activator.PLUGIN_ID, new GenericResult(Activator.PLUGIN_ID,
 				"HeapSeparationSummary", icfgTransformer.getHeapSeparationSummary(), Severity.INFO));

diff --git a/.../uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/FreezeVarInitializer.java b/.../uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/FreezeVarInitializer.java
@@ -1,7 +1,6 @@
 package de.uni_freiburg.informatik.ultimate.icfgtransformer.heapseparator;
 
 import java.util.ArrayList;
-import java.util.Collections;
 import java.util.HashMap;
 import java.util.HashSet;
 import java.util.List;
@@ -46,31 +45,43 @@ public FreezeVarInitializer(final ILogger logger, //final CfgSmtToolkit csToolki
 			final String resultName,
 			final Class<OUTLOC> outLocClazz, final IIcfg<INLOC> inputCfg,
 			final ILocationFactory<INLOC, OUTLOC> funLocFac, final IBacktranslationTracker backtranslationTracker,
-			final Map<IProgramNonOldVar, IProgramConst> freezeVarTofreezeVarLit) {
+			final Map<IProgramNonOldVar, IProgramConst> freezeVarTofreezeVarLit, final IProgramVar validArray) {
 		super(logger, //csToolkit,
 				resultName, outLocClazz, inputCfg, funLocFac, backtranslationTracker);
-		computeInitializingTerm(freezeVarTofreezeVarLit);
-
-//		inputCfg.getCfgSmtToolkit().getSymbolTable().
+		computeInitializingTerm(freezeVarTofreezeVarLit, validArray);
 	}
 
-	private void computeInitializingTerm(final Map<IProgramNonOldVar, IProgramConst> freezeVarTofreezeVarLit) {
-		// (we could get rid of this field it seems..)
-		mFreezeVarInVars = Collections.emptyMap();
-
+	private void computeInitializingTerm(final Map<IProgramNonOldVar, IProgramConst> freezeVarTofreezeVarLit,
+			final IProgramVar validArray) {
+		mFreezeVarInVars = new HashMap<>();
 		mFreezeVarOutVars = new HashMap<>();
 
-
-		// is this locking necessary?
+		// is this locking necessary? the script is used for creating Terms only
 		mMgdScript.lock(this);
 
 		final List<Term> initializingEquations = new ArrayList<>();
 		for (final Entry<IProgramNonOldVar, IProgramConst> en : freezeVarTofreezeVarLit.entrySet()) {
+			// "frz_l_x"
+			final TermVariable frzVar = en.getKey().getTermVariable();
+			// "lit_frz_l_x"
+			final Term frzLit = en.getValue().getTerm();
+
 			// "frz_l_x = lit_frz_l_x"
-			initializingEquations.add(SmtUtils.binaryEquality(mMgdScript.getScript(), en.getKey().getTermVariable(),
-					en.getValue().getTerm()));
-			mFreezeVarOutVars.put(en.getKey(), en.getKey().getTermVariable());
+			initializingEquations.add(SmtUtils.binaryEquality(mMgdScript.getScript(), frzVar,
+					frzLit));
+			mFreezeVarOutVars.put(en.getKey(), frzVar);
+
+			// "valid[lit_frz_l_x] = 1"
+			final Term select = SmtUtils.select(mMgdScript.getScript(), validArray.getTermVariable(), frzLit);
+			final Term one = mMgdScript.getScript().term("1");
+			initializingEquations.add(SmtUtils.binaryEquality(mMgdScript.getScript(), select, one));
 		}
+
+		if (!freezeVarTofreezeVarLit.isEmpty()) {
+			mFreezeVarInVars.put(validArray, validArray.getTermVariable());
+			mFreezeVarOutVars.put(validArray, validArray.getTermVariable());
+		}
+
 		mInitializingTerm = SmtUtils.and(mMgdScript.getScript(), initializingEquations);
 
 		mMgdScript.unlock(this);

diff --git a/...ni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepIcfgTransformer.java b/...ni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepIcfgTransformer.java
@@ -8,21 +8,26 @@
 import java.util.stream.Collectors;
 
 import de.uni_freiburg.informatik.ultimate.core.model.services.ILogger;
-import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.IBacktranslationTracker;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.IIcfgTransformer;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.ILocationFactory;
+import de.uni_freiburg.informatik.ultimate.icfgtransformer.ITransformulaTransformer;
 import de.uni_freiburg.informatik.ultimate.icfgtransformer.TransformedIcfgBuilder;
-import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.CfgSmtToolkit;
+import de.uni_freiburg.informatik.ultimate.logic.Term;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.BasicIcfg;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfg;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfgReturnTransition;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgEdge;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgEdgeIterator;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocationIterator;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transformations.ReplacementVarFactory;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramConst;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramNonOldVar;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVar;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.IEqualityAnalysisResultProvider;
 import de.uni_freiburg.informatik.ultimate.util.csv.ICsvProviderProvider;
+import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.NestedMap2;
 import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple;
 
 public class HeapSepIcfgTransformer<INLOC extends IcfgLocation, OUTLOC extends IcfgLocation>
@@ -36,6 +41,8 @@ public class HeapSepIcfgTransformer<INLOC extends IcfgLocation, OUTLOC extends I
 
 	private final IEqualityAnalysisResultProvider<IcfgLocation, IIcfg<?>> mEqualityProvider;
 
+	private final HeapSeparatorBenchmark mStatistics;
+
 	/**
 	 * Default constructor.
 	 *
@@ -49,15 +56,20 @@ public class HeapSepIcfgTransformer<INLOC extends IcfgLocation, OUTLOC extends I
 	 *            The class object of the type of locations of the output {@link IIcfg}.
 	 * @param newIcfgIdentifier
 	 *            The identifier of the new {@link IIcfg}
+	 * @param statistics
 	 * @param transformer
 	 *            The transformer that should be applied to each transformula of each transition of the input
 	 *            {@link IIcfg} to create a new {@link IIcfg}.
 	 */
 	public HeapSepIcfgTransformer(final IIcfg<INLOC> originalIcfg, final ILocationFactory<INLOC, OUTLOC> funLocFac,
-			final IBacktranslationTracker backtranslationTracker, final Class<OUTLOC> outLocationClass,
-			final String newIcfgIdentifier, final IEqualityAnalysisResultProvider<IcfgLocation, IIcfg<?>> equalityProvider) {
+			final ReplacementVarFactory replacementVarFactory, final IBacktranslationTracker backtranslationTracker,
+			final Class<OUTLOC> outLocationClass, final String newIcfgIdentifier,
+			final IEqualityAnalysisResultProvider<IcfgLocation, IIcfg<?>> equalityProvider,
+			final HeapSeparatorBenchmark statistics) {
 		mEqualityProvider = equalityProvider;
-		computeResult(originalIcfg, funLocFac, backtranslationTracker, outLocationClass, newIcfgIdentifier);
+		mStatistics = statistics;
+		computeResult(originalIcfg, funLocFac, replacementVarFactory, backtranslationTracker, outLocationClass,
+				newIcfgIdentifier);
 	}
 
 	/**
@@ -75,21 +87,26 @@ public HeapSepIcfgTransformer(final IIcfg<INLOC> originalIcfg, final ILocationFa
 	 *
 	 * @param originalIcfg
 	 * @param funLocFac
+	 * @param replacementVarFactory
 	 * @param backtranslationTracker
 	 * @param outLocationClass
 	 * @param newIcfgIdentifier
 	 * @return
 	 */
 	private void computeResult(final IIcfg<INLOC> originalIcfg, final ILocationFactory<INLOC, OUTLOC> funLocFac,
-			final IBacktranslationTracker backtranslationTracker, final Class<OUTLOC> outLocationClass,
-			final String newIcfgIdentifier) {
+			final ReplacementVarFactory replacementVarFactory, final IBacktranslationTracker backtranslationTracker,
+			final Class<OUTLOC> outLocationClass, final String newIcfgIdentifier) {
 
 
-		final CfgSmtToolkit oldCsToolkit = originalIcfg.getCfgSmtToolkit();
-		final IUltimateServiceProvider services;
+//		final CfgSmtToolkit oldCsToolkit = originalIcfg.getCfgSmtToolkit();
+//		final IUltimateServiceProvider services;
 		// TOOD
 		final ILocationFactory<OUTLOC, OUTLOC> outToOutLocFac = null;
 
+		// TODO : where do we get this variable from?
+		final IProgramVar validArray = null;
+
+		final NestedMap2<Term, TfInfo, IProgramNonOldVar> writeIndexTermToTfInfoToFreezeVar;
 
 		/*
 		 * 1. Execute the preprocessing
@@ -103,36 +120,40 @@ private void computeResult(final IIcfg<INLOC> originalIcfg, final ILocationFacto
 					new StoreIndexFreezerIcfgTransformer<>(mLogger, "icfg_with_uninitialized_freeze_vars",
 							outLocationClass, originalIcfg, funLocFac, backtranslationTracker);
 			final IIcfg<OUTLOC> icfgWFreezeVarsUninitialized = sifit.getResult();
+			writeIndexTermToTfInfoToFreezeVar = sifit.getWriteIndexToTfInfoToFreezeVar();
 
 			/*
 			 * Create a fresh literal/constant for each freeze variable that was introduced, we call them freeze
 			 * literals.
 			 * Announce them to the equality analysis as special literals, which are, by axiom, pairwise disjoint.
 			 */
 			final Map<IProgramNonOldVar, IProgramConst> freezeVarTofreezeVarLit = new HashMap<>();
-			for (final IProgramNonOldVar freezeVar :
-				sifit.getWriteIndexToTfInfoToFreezeVar().values().collect(Collectors.toList())) {
-				// TODO
-//				oldCsToolkit.ge
-			}
 
+			for (final IProgramNonOldVar freezeVar : writeIndexTermToTfInfoToFreezeVar.values()
+					.collect(Collectors.toList())) {
+				// FIXME: how to construct a fresh IProgramConst???
+				freezeVarTofreezeVarLit.put(freezeVar,
+						(IProgramConst) replacementVarFactory.getOrConstuctReplacementVar(null, false));
+			}
 			mEqualityProvider.announceAdditionalLiterals(freezeVarTofreezeVarLit.values());
 
 			/*
-			 * Add initialization code for each of the newly introduce freeze variables.
+			 * Add initialization code for each of the newly introduced freeze variables.
 			 * Each freeze variable is initialized to its corresponding freeze literal.
 			 * Furthermore the valid-array (of the memory model) is assumed to be 1 at each freeze literal.
 			 */
 			final FreezeVarInitializer<OUTLOC, OUTLOC> fvi = new FreezeVarInitializer<>(mLogger,
 					"icfg_with_initialized_freeze_vars", outLocationClass, icfgWFreezeVarsUninitialized, outToOutLocFac,
-					backtranslationTracker, freezeVarTofreezeVarLit);
+					backtranslationTracker, freezeVarTofreezeVarLit, validArray);
 			final IIcfg<OUTLOC> icfgWFreezeVarsInitialized = fvi.getResult();
 
 			preprocessedIcfg = icfgWFreezeVarsInitialized;
 		} else {
 			assert mPreprocessing == Preprocessing.MEMLOC_ARRAY;
 			// TODO implement..
 			preprocessedIcfg = null;
+
+			writeIndexTermToTfInfoToFreezeVar = null;
 		}
 
 
@@ -145,13 +166,17 @@ private void computeResult(final IIcfg<INLOC> originalIcfg, final ILocationFacto
 		 * 3. compute an array partitioning
 		 */
 
+		final HeapSepPreAnalysis heapSepPreanalysis = new HeapSepPreAnalysis(mLogger,
+				originalIcfg.getCfgSmtToolkit().getManagedScript());
+		new IcfgEdgeIterator(originalIcfg).forEachRemaining(edge -> heapSepPreanalysis.processEdge(edge));
 
-//		final HeapSepPreAnalysis heapSepPreanalysis = new HeapSepPreAnalysis(mLogger,
-//				csToolkit.getManagedScript());
-//		new IcfgEdgeIterator(icfg).forEachRemaining(edge -> heapSepPreanalysis.processEdge(edge));
-
-
-//		final NewArrayIdProvider newArrayIdProvider = new NewArrayIdProvider(csToolkit, equalityProvider, hspav, statistics);
+		final NewArrayIdProvider newArrayIdProvider;
+		if (mPreprocessing == Preprocessing.FREEZE_VARIABLES) {
+			newArrayIdProvider = new NewArrayIdProvider(originalIcfg.getCfgSmtToolkit(),
+					mEqualityProvider, heapSepPreanalysis, writeIndexTermToTfInfoToFreezeVar, mStatistics);
+		} else {
+			newArrayIdProvider = null;
+		}
 
 		/*
 		 * 4. Execute the transformer that splits up the arrays according to the result from the equality analysis.
@@ -162,12 +187,14 @@ private void computeResult(final IIcfg<INLOC> originalIcfg, final ILocationFacto
 //				equalityProvider);
 //
 //		hstftf.preprocessIcfg(originalIcfg);
-//		final BasicIcfg<OUTLOC> resultIcfg =
-//				new BasicIcfg<>(newIcfgIdentifier, originalIcfg.getCfgSmtToolkit(), outLocationClass);
-//		final TransformedIcfgBuilder<INLOC, OUTLOC> lst =
-//				new TransformedIcfgBuilder<>(funLocFac, backtranslationTracker, transformer, originalIcfg, resultIcfg);
-//		processLocations(originalIcfg.getInitialNodes(), lst);
-//		lst.finish();
+		final BasicIcfg<OUTLOC> resultIcfg =
+				new BasicIcfg<>(newIcfgIdentifier, originalIcfg.getCfgSmtToolkit(), outLocationClass);
+		final ITransformulaTransformer transformer = null;
+		final TransformedIcfgBuilder<INLOC, OUTLOC> lst =
+				new TransformedIcfgBuilder<>(funLocFac, backtranslationTracker, transformer, originalIcfg, resultIcfg);
+		processLocations(originalIcfg.getInitialNodes(), lst);
+		lst.finish();
+		mResultIcfg = resultIcfg;
 //		return resultIcfg;
 //		final BasicIcfg<OUTLOC> resultIcfg =
 //				new BasicIcfg<>(newIcfgIdentifier, originalIcfg.getCfgSmtToolkit(), outLocationClass);

diff --git a/...de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepPreAnalysis.java b/...de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepPreAnalysis.java
@@ -56,10 +56,10 @@
 /**
  * Does a preanalysis on the program before the actual heap separation is done
  * (using the abstract interpretation result from the equality domain).
- * Computes: - which arrays are equated, anywhere in the program (occur left and
- * right each of an equality in a TransFormula) - for each array in the program
- * the locations where it is accessed (question: does this mean that large block
- * encoding is detrimental to heapseparation?)
+ * Computes:
+ *  <li> which arrays are equated, anywhere in the program (occur left and right each of an equality in a TransFormula)
+ *  <li> for each array in the program the locations where it is accessed (this functionality is deprecated as of
+ *   Jan '18)
  *
  * @author Alexander Nutz
  *

diff --git a/...urg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepTransFormulaTransformer.java b/...urg/informatik/ultimate/icfgtransformer/heapseparator/HeapSepTransFormulaTransformer.java
@@ -521,8 +521,9 @@ public void preprocessIcfg(final IIcfg<?> icfg) {
 		 * compute the partitioning from the above results, in particular compute which array will translate to which
 		 *  new array for which accessing expression
 		 */
-		mNewArrayIdProvider =
-				new NewArrayIdProvider(mCsToolkit, mEqualityProvider, heapSepPreanalysis, mStatistics);
+
+//		mNewArrayIdProvider =
+//				new NewArrayIdProvider(mCsToolkit, mEqualityProvider, heapSepPreanalysis, mStatistics);
 		mNewSymbolTable = mNewArrayIdProvider.getNewSymbolTable();
 
 		mLogger.info("IcfgTransformer_HeapSeparator: Computed the following array partitioning from the given"

diff --git a/...de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/NewArrayIdProvider.java b/...de/uni_freiburg/informatik/ultimate/icfgtransformer/heapseparator/NewArrayIdProvider.java
@@ -49,6 +49,7 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IIcfg;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.structure.IcfgLocation;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.transformations.IntraproceduralReplacementVar;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramNonOldVar;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramVarOrConst;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.ProgramVarUtils;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.arrays.ArrayIndex;
@@ -77,7 +78,9 @@ public class NewArrayIdProvider {
 
 	public NewArrayIdProvider(final CfgSmtToolkit csToolkit,
 			final IEqualityAnalysisResultProvider<IcfgLocation, IIcfg<?>> equalityProvider,
-			final HeapSepPreAnalysis hspav, final HeapSeparatorBenchmark statistics) {
+			final HeapSepPreAnalysis hspav,
+			final NestedMap2<Term, TfInfo, IProgramNonOldVar> writeIndexTermToTfInfoToFreezeVar,
+			final HeapSeparatorBenchmark statistics) {
 		mManagedScript = csToolkit.getManagedScript();
 		mOldSymbolTable = csToolkit.getSymbolTable();
 		mNewSymbolTable = new DefaultIcfgSymbolTable(csToolkit.getSymbolTable(), csToolkit.getProcedures());

diff --git a/...iburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqNodeAndFunctionFactory.java b/...iburg/informatik/ultimate/modelcheckerutils/absint/vpdomain/EqNodeAndFunctionFactory.java
@@ -30,12 +30,14 @@
 import java.util.HashSet;
 import java.util.Map;
 import java.util.Set;
+import java.util.stream.Collectors;
 
 import de.uni_freiburg.informatik.ultimate.core.model.services.IUltimateServiceProvider;
 import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm;
 import de.uni_freiburg.informatik.ultimate.logic.ConstantTerm;
 import de.uni_freiburg.informatik.ultimate.logic.Term;
 import de.uni_freiburg.informatik.ultimate.logic.TermVariable;
+import de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.variables.IProgramConst;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.CommuhashNormalForm;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.linearTerms.AffineTerm;
@@ -51,13 +53,18 @@ public class EqNodeAndFunctionFactory extends AbstractNodeAndFunctionFactory<EqN
 
 	private final IUltimateServiceProvider mServices;
 	private final ManagedScript mMgdScript;
+	private final Set<Term> mAdditionalLiteralTerms;
 
 	private final Map<Term, EqNode> mTermToEqNode = new HashMap<>();
 	private final Map<Term, Term> mNormalizationCache = new HashMap<>();
 
-	public EqNodeAndFunctionFactory(final IUltimateServiceProvider services, final ManagedScript script) {
+
+
+	public EqNodeAndFunctionFactory(final IUltimateServiceProvider services, final ManagedScript script,
+			final Set<IProgramConst> additionalLiterals) {
 		mServices = services;
 		mMgdScript = script;
+		mAdditionalLiteralTerms = additionalLiterals.stream().map(pc -> pc.getTerm()).collect(Collectors.toSet());
 	}
 
 	public ManagedScript getScript() {
@@ -158,8 +165,7 @@ public EqNode getExistingNode(final Term term) {
 	 * Examples of literals (sometimes called constants, but we have other uses for that word) are:
 	 *  1, 2, -1, true, false, 1bv16 (bitvector constant/literal)
 	 *
-	 * The defining trait of literals for our purposes is that two different literals always have a different value,
-	 * too.
+	 * The defining trait of literals for our purposes is that two different literals always have a different value.
 	 *
 	 * @param term
 	 * @return
@@ -175,6 +181,10 @@ private boolean isTermALiteral(final Term term) {
 			return true;
 		}
 
+		if (mAdditionalLiteralTerms.contains(term)) {
+			return true;
+		}
+
 		mMgdScript.lock(this);
 		final AffineTerm affineTerm = (AffineTerm) new AffineTermTransformer(mMgdScript.getScript()).transform(term);
 		mMgdScript.unlock(this);