janhaag/PSE2011 — Issue #111: function call assumes not translated properly in some cases
Author: ratefuchs
Created: 2012-03-07 18:56:52+00:00
State: open
Labels: Verifier/SMTLib

This problem arises only if a variable is updated and the assigned value contains a function call which contains the variable
in the parameter expressions (e.g. "i=f(i);") and the parameter is used in the called function's assumptions. Then the variable i in the assumptions is not replaced by the old but with the new value.