PR# 16339 freeze needed after a run that ended with an exception, otherwise wrong code is executed

If a program has a contract violation and is closed, a freeze is needed before the next execution. Otherwise wrong code will be executed...
I stripped down my current application to provide a reproducible testcase. The problem might be connected with using external C stuff.
Please note that this bug is - at least in my opinion - pretty severe. Programmers will most likely debug their code for a long time before having the idea that it might be a bug in Eiffel and that a clean build is required (at least I needed quite a lot of time). With the described issue, it's never clear if a problem is a bug in the written code or EiffelStudio.

Extract the attached zip and:
1. Open EiffelStudio (e2eiffel.ecf); compile the project
2. Press "Run". The console output is:
   struct teststruct {
      int a;
      int b;
   };
3. close the application, comment for instance "visit (specifiers_and_qualifiers, v)" in AST_STRUCT_DECLARATION
4. Press "Run"; the application will abort with a invariant violation; stop the execution
5. uncomment "visit (specifiers_and_qualifiers, v)" again
6. Press "Run". The output is:
   struct teststruct {
      ;
      ;
   };
Now I would definitely expect the original output since nothing was changed and the project was recompiled after uncomenting the statement.   
Depending on the exception at runtime (and I also think static compilation errors), the output might vary. It can also be completely empty.

If you close the application, do a freeze and run it again, the whole source reappears.

Seems to be related to a problem report I sent to the mailinglist:

Subject: inconsistent supplier precondition checking
Message:

Dear all

In one of my Vision2 projects (minimized code showing the problem is 
attached at the end) I have all assertions turned on for my own target. 
But if I call enable_select on a EV_LIST_ITEM, it's preconditions are 
not evaluated (`is_selectable' should actually fail).
But, if I change invariant checking to False or no longer inherit from 
ARGUMENTS, the enable_select will all the sudden be executed again.

I think, since supplier precondition checking is enabled, it should 
always check the enable_select assertions. And I fail to see why 
changing the inheritance structure or invariant checking could have any 
influence on that.
So, I'm quite puzzled by this. I guess I'm doing something stupid here 
but I can't figure out what it is. If no one is seeing an obvious 
problem, I'll create a bugreport.

Ah yeah, I'm working on Windows Vista with MSC and 
....
Output truncated, Click download to get the full message

Attachments for problem report #16339