testing a fix in SI

also changing back the output path in BoogieDriver
also disabling z3api for now since it does not build

3 files changed, 2 insertions, 5 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 1f9c96a3..1e733880 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -133,7 +133,6 @@ Global
 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|x86.ActiveCfg = z3apidebug|x86

 		{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}.z3apidebug|x86.Build.0 = z3apidebug|x86

-		{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|.NET.ActiveCfg = Checked|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.Checked|Any CPU.Build.0 = Checked|Any CPU

@@ -160,7 +159,6 @@ Global
 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|x86.ActiveCfg = z3apidebug|Any CPU

 		{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU

-		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.z3apidebug|x86.Build.0 = z3apidebug|Any CPU

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|.NET.ActiveCfg = Checked|Any CPU

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Any CPU.ActiveCfg = Checked|Any CPU

 		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Checked|Any CPU.Build.0 = Checked|Any CPU

@@ -246,7 +244,6 @@ Global
 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Any CPU.Build.0 = Debug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

-		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Debug|x86.ActiveCfg = Debug|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|.NET.ActiveCfg = Release|Any CPU

 		{966DD87B-A29D-4F3C-9406-F680A61DC0E0}.Release|Any CPU.ActiveCfg = Release|Any CPU

@@ -434,7 +431,6 @@ Global
 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.ActiveCfg = Release|Any CPU

 		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.Build.0 = Release|Any CPU

-		{A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|x86.Build.0 = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|.NET.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.ActiveCfg = Release|Any CPU

 		{CF41E903-78EB-43BA-A355-E5FEB5ECECD4}.Checked|Any CPU.Build.0 = Release|Any CPU

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 18f94929..57aeb4d9 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -40,7 +40,7 @@
     <DebugSymbols>true</DebugSymbols>

     <DebugType>full</DebugType>

     <Optimize>false</Optimize>

-    <OutputPath>..\Provers\Z3api\bin\z3apidebug\</OutputPath>

+    <OutputPath>..\..\Binaries\</OutputPath>

     <DefineConstants>TRACE;DEBUG</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 2d518a54..abe93783 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -144,6 +144,7 @@ namespace VC {
       for (int i = 0; i < interfaceExprs.Count; i++) {

         ret = gen.And(ret, gen.Eq(interfaceExprs[i], svc.interfaceExprVars[i]));

       }

+      ret = gen.Or(blockExpr, ret);

       return ret;

     }

   }