#295, only havoc variable when removing pvocs from an EqState

ultimate-pa · Jan 23, 2018 · 5ab50b2 · 5ab50b2
1 parent 17948a9
commit 5ab50b2
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/...ik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/EqState.java b/...ik/ultimate/plugins/analysis/abstractinterpretationv2/domain/transformula/vp/EqState.java
@@ -41,6 +41,7 @@
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.absint.vpdomain.EqNodeAndFunctionFactory;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.boogie.BoogieConst;
 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.equalityanalysis.IEqualityProvidingIntermediateState;
 import de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.equalityanalysis.IEqualityProvidingState;
@@ -99,8 +100,13 @@ public EqState addVariables(final Collection<IProgramVarOrConst> variables) {
 
 	@Override
 	public EqState removeVariables(final Collection<IProgramVarOrConst> variables) {
+
+		final Set<IProgramVarOrConst> variablesFiltered = variables.stream().filter(var -> var instanceof IProgramVar)
+				.collect(Collectors.toSet());
+
 		final Set<Term> termsFromPvocs =
-				variables.stream().map(pvoc -> pvoc.getTerm()).collect(Collectors.toSet());
+				variablesFiltered.stream().map(pvoc -> pvoc.getTerm()).collect(Collectors.toSet());
+//				variables.stream().map(pvoc -> pvoc.getTerm()).collect(Collectors.toSet());
 		final EqConstraint<EqNode> projectedConstraint =
 				mFactory.getEqConstraintFactory().projectExistentially(termsFromPvocs, mConstraint, false);