#184 - added question as TODO

ultimate-pa · May 22, 2017 · c1089d0 · c1089d0
1 parent 65ec375
commit c1089d0
Showing 1 changed file with 9 additions and 1 deletion.
diff --git a/...ultimate/plugins/generator/traceabstraction/predicates/IterativePredicateTransformer.java b/...ultimate/plugins/generator/traceabstraction/predicates/IterativePredicateTransformer.java
@@ -61,8 +61,10 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.predicates.PredicateTransformer;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.predicates.TermDomainOperationProvider;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.Activator;
+import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.FlowSensitiveFaultLocalizer;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.predicates.IterativePredicateTransformer.TraceInterpolationException.Reason;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.singletracecheck.NestedFormulas;
+import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.singletracecheck.TraceCheckerSpWp;
 import de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.singletracecheck.TracePredicates;
 
 /**
@@ -85,6 +87,12 @@ public class IterativePredicateTransformer {
 	private final IPredicate mPrecondition;
 	private final IPredicate mPostcondition;
 	protected final SortedMap<Integer, IPredicate> mPendingContexts;
+	/**
+	 * TODO 2017-05-22 Christian&Matthias: Not sure about this field. There are two users, {@link TraceCheckerSpWp} and
+	 *      {@link FlowSensitiveFaultLocalizer}. The further passe {@code null}, which should, if this field is read,
+	 *      result in a {@code NullPointerException}. The latter passes a predicate for {@code true}, which is counter-
+	 *      intuitive.
+	 */
 	private final IPredicate mFalsePredicate;
 
 	private final IIcfgSymbolTable mSymbolTable;
@@ -104,7 +112,7 @@ public IterativePredicateTransformer(final PredicateFactory predicateFactory, fi
 		mXnfConversionTechnique = xnfConversionTechnique;
 		mMgdScript = mgdScript;
 		mModifiedGlobals = modifiableGlobalsTable;
-		mPredicateTransformer = new PredicateTransformer<Term, IPredicate, TransFormula>(mgdScript, new TermDomainOperationProvider(mServices, mMgdScript));
+		mPredicateTransformer = new PredicateTransformer<>(mgdScript, new TermDomainOperationProvider(mServices, mMgdScript));
 		mPredicateFactory = predicateFactory;
 		mTrace = trace;
 		mPrecondition = precondition;