Merge branch 'master' of https://github.com/boogie-org/boogie

9 files changed, 21 insertions, 58 deletions

diff --git a/.travis.yml b/.travis.yml
index 11ed4d64..41ee569f 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -6,14 +6,15 @@ env:
   - BOOGIE_CONFIG=Debug
   - BOOGIE_CONFIG=Release
 install:
-  - sudo apt-key adv --recv-keys --keyserver keyserver.ubuntu.com C504E590
-  # FIXME: We should not be using GPUVerify's repo for Z3
-  - sudo sh -c 'echo "deb http://ppa.launchpad.net/delcypher/gpuverify-smt/ubuntu precise main" > /etc/apt/sources.list.d/smt.list'
+  - wget http://download.opensuse.org/repositories/home:delcypher:z3/xUbuntu_12.04/Release.key
+  - sudo apt-key add - < Release.key
+  # Use Z3 package built by the OpenSUSE build service https://build.opensuse.org/package/show/home:delcypher:z3/z3
+  - sudo sh -c "echo 'deb http://download.opensuse.org/repositories/home:/delcypher:/z3/xUbuntu_12.04/ /' >> /etc/apt/sources.list.d/z3.list"
   - sudo apt-get update
   # NuGet is a little flakey in legacy TravisCI, use travis_retry command to retry the command if it fails
   - travis_retry nuget restore ${TRAVIS_SOLUTION}
-  # Install Z3
-  - sudo apt-get -y install z3=4.3.2-0~precise2
+  # Install Z3 executable
+  - sudo apt-get -y install 'z3=4.4.1-*'
   # Install needed python tools
   - sudo pip install lit OutputCheck pyyaml
   - mkdir -p Source/packages && cd Source/packages && travis_retry nuget install NUnit.Runners -Version 2.6.3
diff --git a/Build/CodePlex.Tools.MsBuild.dll b/Build/CodePlex.Tools.MsBuild.dll
deleted file mode 100644
index 2e400e8e..00000000
--- a/Build/CodePlex.Tools.MsBuild.dll
+++ /dev/null
diff --git a/Build/CodePlex.Tools.Wiki.dll b/Build/CodePlex.Tools.Wiki.dll
deleted file mode 100644
index 9ea2bea8..00000000
--- a/Build/CodePlex.Tools.Wiki.dll
+++ /dev/null
diff --git a/Build/updateVersionFile.xml b/Build/updateVersionFile.xml
deleted file mode 100644
index cb083c7a..00000000
--- a/Build/updateVersionFile.xml
+++ /dev/null
@@ -1,19 +0,0 @@
-<Project xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
-  <UsingTask AssemblyFile="CodePlex.Tools.MsBuild.dll" TaskName="CreateAssemblyInfo" />
-    
-  <Target Name="CreateAssemblyInfo">
-    <CreateAssemblyInfo
-      Version="$(CCNetLabel)"
-      CreateVersionFile="true"
-      ForceReadOnly="true"
-      VersionFileName="..\Source\version.ssc"
-    />
-    <CreateAssemblyInfo
-      Version="$(CCNetLabel)"
-      CreateVersionFile="true"
-      ForceReadOnly="true"
-      VersionFileName="..\Source\version.cs"
-    />
-  </Target>
-</Project>
-
diff --git a/README.md b/README.md
index a976b249..1dd0ba5a 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@
 |-------------------------------|---------------------------------|
 | [![linux build status][1]][2] | [![windows_build_status][3]][4] |
 
-[1]: https://travis-ci.org/boogie-org/boogie.svg
+[1]: https://travis-ci.org/boogie-org/boogie.svg?branch=master
 [2]: https://travis-ci.org/boogie-org/boogie
 [3]: https://pmbuilds.inf.ethz.ch/buildStatus/icon?job=boogie
 [4]: #FIXME
@@ -48,7 +48,7 @@ You can also report issues on our [issue tracker](https://github.com/boogie-org/
 ### Requirements
 
 - [NuGet](https://www.nuget.org/)
-- [Z3](https://github.com/Z3Prover/z3) 4.3.2 or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note
+- [Z3](https://github.com/Z3Prover/z3) 4.4.1 or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note
   CVC4 support is experimental)
 
 #### Windows specific
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index da445a00..8c1ae407 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -356,16 +356,8 @@ namespace Microsoft.Boogie {
       hasOutput = false;
       outputExn = null;
       this.handler = handler;
-
-      if (namedAssumeVars != null && namedAssumeVars.Any())
-      {
-        // TODO(wuestholz): Avoid doing a full reset. This is currently necessary for old versions of Z3 due to a bug.
-        thmProver.FullReset(gen);
-      }
-      else
-      {
-        thmProver.Reset(gen);
-      }
+      
+      thmProver.Reset(gen);
       SetTimeout();
       proverStart = DateTime.UtcNow;
       thmProver.NamedAssumeVars = namedAssumeVars;
diff --git a/Source/version.ssc b/Source/version.ssc
deleted file mode 100644
index 5bdcf170..00000000
--- a/Source/version.ssc
+++ /dev/null
@@ -1,12 +0,0 @@
-// ==++==
-// 
-//   
-// 
-// ==--==
-// Warning: Automatically generated file. DO NOT EDIT
-// Generated at Dienstag, 5. Juli 2011 11:26:45
-
-using System.Reflection;
-[assembly: AssemblyVersion("2.2.30705.1126")]
-[assembly: AssemblyFileVersion("2.2.30705.1126")]
-
diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
index 9f960f26..3c0d0b20 100644
--- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
+++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
@@ -127,7 +127,8 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(3832,3): inline$storm_IoCancelIrp$0$anon10#2
     daytona_bug2_ioctl_example_2.bpl(3892,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2
     daytona_bug2_ioctl_example_2.bpl(3902,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2
-    daytona_bug2_ioctl_example_2.bpl(3928,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Then#2
+    daytona_bug2_ioctl_example_2.bpl(3915,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2
+    daytona_bug2_ioctl_example_2.bpl(3923,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2
     daytona_bug2_ioctl_example_2.bpl(3933,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2
     daytona_bug2_ioctl_example_2.bpl(3944,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2
     daytona_bug2_ioctl_example_2.bpl(3949,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2
diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect
index 5d9d41c5..6939fee4 100644
--- a/Test/test15/CaptureState.bpl.expect
+++ b/Test/test15/CaptureState.bpl.expect
@@ -14,17 +14,17 @@ $mv_state_const -> 3
 F -> T@FieldName!val!0
 Heap -> |T@[Ref,FieldName]Int!val!0|
 m -> **m
-m@0 -> (- 276)
-m@1 -> (- 275)
-m@3 -> (- 275)
+m@0 -> (- 2)
+m@1 -> (- 1)
+m@3 -> (- 1)
 r -> **r
-r@0 -> (- 550)
+r@0 -> (- 2)
 this -> T@Ref!val!0
 x -> 719
 y -> **y
 Select_[Ref,FieldName]$int -> {
-  |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 276)
-  else -> (- 276)
+  |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 2)
+  else -> (- 2)
 }
 $mv_state -> {
   3 0 -> true
@@ -49,13 +49,13 @@ tickleBool -> {
 *** STATE top
 *** END_STATE
 *** STATE then
-  m -> (- 276)
+  m -> (- 2)
 *** END_STATE
 *** STATE postUpdate0
-  m -> (- 275)
+  m -> (- 1)
 *** END_STATE
 *** STATE end
-  r -> (- 550)
+  r -> (- 2)
   m -> 7
 *** END_STATE
 *** END_MODEL