summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2011-09-27 15:50:25 -0700
committerGravatar qadeer <qadeer@microsoft.com>2011-09-27 15:50:25 -0700
commit11c497c205a6303f7412857289a69afb9c0ef5b5 (patch)
treefc3a6da4ceef00693ad25700c3660dce1c7cc464 /Source
parent7e24d7cbf6b9e408c8d3426d8bf98ec95ea97abf (diff)
fixed houdini so that it is cognizant of inlined procedures
Diffstat (limited to 'Source')
-rw-r--r--Source/Houdini/Houdini.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 714ecd3b..9646ef85 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -333,7 +333,7 @@ namespace Microsoft.Boogie.Houdini {
Queue<Implementation> queue = new Queue<Implementation>();
foreach (Declaration decl in program.TopLevelDeclarations) {
Implementation impl = decl as Implementation;
- if (impl != null) {
+ if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {
queue.Enqueue(impl);
}
}