diff options
| author |  rustanleino <unknown> | 2011-03-10 01:20:05 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-10 01:20:05 +0000 |
| commit | e28c62b12194be07e3ecb3301e6b3e0336bcac2a (patch) | |
| tree | d7696df3fee35aeff3cc56f333c0923fbdfa9d4f | |
| parent | b3f70e3d20aa57440ea5b398180581a9933daed4 (diff) | |
Updated PrepareBoogieZip.bat to include BVD and smt2
Ignore duplicated else functions in models
| -rw-r--r-- | Binaries/PrepareBoogieZip.bat | 5 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 3 |
2 files changed, 6 insertions, 2 deletions
diff --git a/Binaries/PrepareBoogieZip.bat b/Binaries/PrepareBoogieZip.bat index 38dff1d1..3c512aaa 100644 --- a/Binaries/PrepareBoogieZip.bat +++ b/Binaries/PrepareBoogieZip.bat @@ -11,22 +11,25 @@ for %%f in ( AIFramework.dll AIFramework.pdb Basetypes.dll Basetypes.pdb Boogie.exe Boogie.pdb + BVD.exe BVD.pdb CodeContractsExtender.dll CodeContractsExtender.pdb Core.dll Core.pdb Dafny.exe Dafny.pdb DafnyPipeline.dll DafnyPipeline.pdb Graph.dll Graph.pdb + Model.dll Model.pdb ParserHelper.dll ParserHelper.pdb Provers.Isabelle.dll Provers.Isabelle.pdb Provers.Simplify.dll Provers.Simplify.pdb Provers.SMTLib.dll Provers.SMTLib.pdb + Provers.TPTP.dll Provers.TPTP.pdb Provers.Z3.dll Provers.Z3.pdb VCExpr.dll VCExpr.pdb VCGeneration.dll VCGeneration.pdb DafnyPrelude.bpl DafnyRuntime.cs TypedUnivBackPred2.sx - UnivBackPred2.smt + UnivBackPred2.smt2 UnivBackPred2.sx ) do ( copy %%f %DEST_DIR% 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]];
|