@@ -31,15 +31,14 @@ private record Substitution(VCImplication sourceNode, FunctionInvocation invocat
3131 */
3232 @ Override
3333 public VCImplication apply (VCImplication implication ) {
34- VCImplication result = implication .clone ();
35- Optional <Substitution > substitutionOpt = findSubstitution (result );
34+ Optional <Substitution > substitutionOpt = findSubstitution (implication );
3635
3736 if (substitutionOpt .isPresent ()) {
3837 Substitution substitution = substitutionOpt .get ();
39- result = substitute (result , substitution .sourceNode (), substitution .invocation (),
38+ return substitute (implication , substitution .sourceNode (), substitution .invocation (),
4039 substitution .replacement (), substitution .sourceEquality ());
4140 }
42- return result ;
41+ return implication ;
4342 }
4443
4544 /**
@@ -61,7 +60,7 @@ private VCImplication substitute(VCImplication implication, VCImplication node,
6160 }
6261
6362 // preserve the current node and continue rewriting the suffix
64- VCImplication result = copyWithRefinement (implication , implication .getRefinement (). clone () );
63+ VCImplication result = copyWithRefinement (implication , implication .getRefinement ());
6564 result .setNext (substitute (implication .getNext (), node , invocation , replacement , sourceEquality ));
6665 return result ;
6766 }
@@ -77,7 +76,7 @@ private VCImplication removeSourceEquality(VCImplication implication, Expression
7776
7877 Predicate refinement = new Predicate ();
7978 for (Expression conjunct : remaining )
80- refinement = Predicate .createConjunction (refinement , new Predicate (conjunct . clone () ));
79+ refinement = Predicate .createConjunction (refinement , new Predicate (conjunct ));
8180 return copyWithRefinement (implication , refinement );
8281 }
8382
@@ -99,11 +98,11 @@ private VCImplication substituteSuffix(VCImplication implication, FunctionInvoca
9998 */
10099 private VCImplication substituteNode (VCImplication implication , FunctionInvocation invocation ,
101100 Expression replacement ) {
102- Expression expression = implication .getRefinement ().getExpression (). clone () ;
101+ Expression expression = implication .getRefinement ().getExpression ();
103102 if (!containsExpression (expression , invocation ))
104- return copyWithRefinement (implication , new Predicate ( expression ));
103+ return copyWithRefinement (implication , implication . getRefinement ( ));
105104
106- Expression substituted = expression .substitute (invocation , replacement . clone () );
105+ Expression substituted = expression .substitute (invocation , replacement );
107106 return copyWithRefinement (implication , new Predicate (substituted ));
108107 }
109108
@@ -125,7 +124,7 @@ private Optional<Substitution> findSubstitution(VCImplication implication) {
125124 * Extracts a substitution from one VC node refinement
126125 */
127126 private Optional <Substitution > getSubstitution (VCImplication implication ) {
128- return getSubstitution (implication , implication .getRefinement ().getExpression (). clone () );
127+ return getSubstitution (implication , implication .getRefinement ().getExpression ());
129128 }
130129
131130 /**
@@ -145,11 +144,9 @@ private Optional<Substitution> getSubstitution(VCImplication implication, Expres
145144 Expression left = binary .getFirstOperand ();
146145 Expression right = binary .getSecondOperand ();
147146 if (left instanceof FunctionInvocation invocation && !containsExpression (right , left ))
148- return Optional .of (new Substitution (implication , (FunctionInvocation ) invocation .clone (), right .clone (),
149- binary .clone ()));
147+ return Optional .of (new Substitution (implication , invocation , right , binary ));
150148 if (right instanceof FunctionInvocation invocation && !containsExpression (left , right ))
151- return Optional .of (new Substitution (implication , (FunctionInvocation ) invocation .clone (), left .clone (),
152- binary .clone ()));
149+ return Optional .of (new Substitution (implication , invocation , left , binary ));
153150
154151 return Optional .empty ();
155152 }
0 commit comments