summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/Check.cs
diff options
context:
space:
mode:
authorGravatar rustanleino <unknown>2011-03-10 01:20:05 +0000
committerGravatar rustanleino <unknown>2011-03-10 01:20:05 +0000
commite28c62b12194be07e3ecb3301e6b3e0336bcac2a (patch)
treed7696df3fee35aeff3cc56f333c0923fbdfa9d4f /Source/VCGeneration/Check.cs
parentb3f70e3d20aa57440ea5b398180581a9933daed4 (diff)
Updated PrepareBoogieZip.bat to include BVD and smt2
Ignore duplicated else functions in models
Diffstat (limited to 'Source/VCGeneration/Check.cs')
-rw-r--r--Source/VCGeneration/Check.cs3
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 67333752..5618fafa 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -507,7 +507,8 @@ namespace Microsoft.Boogie {
var args = new Model.Element[arity];
foreach (var l in tuples) {
if (l.Count == 1) {
- f.Else = elts[l[0]];
+ if (f.Else == null)
+ f.Else = elts[l[0]];
} else {
for (int i = 0; i < f.Arity; ++i)
args[i] = elts[l[i]];