diff options
| author |  qadeer <unknown> | 2014-02-28 14:55:45 -0800 |
|---|---|---|
| committer | qadeer <unknown> | 2014-02-28 14:55:45 -0800 |
| commit | b5c99d5d7cc09081c12334bb58346b9230b7519f (patch) | |
| tree | ec1b4b85ed6ac8af3bbfcd92e5ccd219ea5091a7 /Source | |
| parent | c77f823f177067df9810896fca015fc77a16d5ab (diff) | |
Added a fix to inlining so that it becomes cognizant of procedures that the user wants to check
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 77bbae43..19245c43 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -737,7 +737,7 @@ namespace Microsoft.Boogie }
foreach (var impl in TopLevelDeclarations.OfType<Implementation>())
{
- if (!impl.SkipVerification)
+ if (CommandLineOptions.Clo.UserWantsToCheckRoutine(impl.Name) && !impl.SkipVerification)
{
Inliner.ProcessImplementation(program, impl);
}
|