summaryrefslogtreecommitdiff
path: root/Source/ExecutionEngine/ExecutionEngine.cs
diff options
context:
space:
mode:
authorGravatar Pantazis Deligiannis <pdeligia@me.com>2013-08-15 12:48:24 +0100
committerGravatar Pantazis Deligiannis <pdeligia@me.com>2013-08-15 12:48:24 +0100
commit819c1f07fe1e0244e14306ad1dee213a9a034f1e (patch)
treebd2f6fd92b7c4b0a2e2aa6ca930aad30c1968c85 /Source/ExecutionEngine/ExecutionEngine.cs
parent35e161373f445f56c31caf99117e562c2105770f (diff)
new option to disable checking for loop maintained invariants - this leads to an underapproximation that helps to speedup houdini refutation of candidates
Diffstat (limited to 'Source/ExecutionEngine/ExecutionEngine.cs')
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs1
1 files changed, 0 insertions, 1 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index f81150b1..34a32dfd 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -686,7 +686,6 @@ namespace Microsoft.Boogie
}
}
-
/// <summary>
/// Given a resolved and type checked Boogie program, infers invariants for the program
/// and then attempts to verify it. Returns: