summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-01 21:43:07 -0800
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-02-01 21:43:07 -0800
commit0ad7d270e9a989919d9291a86a018fe55349022b (patch)
treee3896e25ce0c3c8ded1075cffc819e88123c8acc /Source/BoogieDriver
parent06055fdd22eeb9015d215e71996e4714c183ef19 (diff)
fixed bug in OG
added another OG sample illustrating rely-guarantee encoding
Diffstat (limited to 'Source/BoogieDriver')
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 69fb547c..c4db46f4 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -197,7 +197,7 @@ namespace Microsoft.Boogie {
}
LinearSetTransform linearTransform = new LinearSetTransform(program);
linearTransform.Transform();
-
+
EliminateDeadVariablesAndInline(program);
int errorCount, verified, inconclusives, timeOuts, outOfMemories;