Silicon hangs if smt code sent to Z3 isn't indented

[viper-admin]

Created by @alexanderjsummers on 2015-06-04 09:54

Silicon requires that multi-line constructs (such as axioms) be indented, such that only the first line is without an indent. If modifying e.g. the preamble, and this is not respected, the tool hangs waiting for an acknowledgement from Z3.

There should be some kind of timeout mechanism for this iteraction.

[fabiopakk]

Issue fixed. I've created a message for that now.

[fabiopakk]

This solution slowed down Silicon, so I've removed the fix and reopened the issue.