summaryrefslogtreecommitdiff
path: root/Source/ExecutionEngine/ExecutionEngine.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/ExecutionEngine/ExecutionEngine.cs')
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs2
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);
}