In the method apply of the class ExpectationTransformer of the module wp, a deepcopy is missing in line 276 around expectation. Without this deepcopy, in the subsequent substitution, changes to one occurrence of this expectation are also applied to the other occurrences.
For example, the following code produces the output (5 + 2) + (5 + 2) instead of (5 + 2) + (4 + 2).
v = VarExpr('v')
a = SubstExpr({'x': NatLitExpr(5)}, v)
b = SubstExpr({'x': NatLitExpr(4)}, v)
e = BinopExpr(Binop.PLUS, a, b)
wt = WeightingTransformer('v', e)
print(wt.apply(BinopExpr(Binop.PLUS, VarExpr('x'), NatLitExpr(2))))
In the method apply of the class ExpectationTransformer of the module wp, a deepcopy is missing in line 276 around expectation. Without this deepcopy, in the subsequent substitution, changes to one occurrence of this expectation are also applied to the other occurrences.
For example, the following code produces the output
(5 + 2) + (5 + 2)instead of(5 + 2) + (4 + 2).