Merge pull request #27 from boogie-org/update_recommended_Z3_version

Update recommended z3 version

4 files changed, 18 insertions, 16 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/README.md b/README.md
index a976b249..224d7196 100644
--- a/README.md
+++ b/README.md
@@ -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/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