janhaag/PSE2011 — Issue #98: Function calls work not properly in SMTLibTranslator
Author: ratefuchs
Created: 2012-03-05 21:25:41+00:00
State: open
Labels: Verifier/SMTLib

In a program like:

int two(){return 2;}
main(){
int y = 0;
int x = two();
}ensure y==0;

the information about y being zero is lost after func call (this can be assumed since y was zero before and there is no global state).