From 63b3602e12aa67bf9a06d3388c65745d2ad64fef Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 6 Jul 2017 15:16:26 -0700
Subject: [PATCH] Calibrated test output to Z3 version 4.5.0 (32-bit x86). 
 Please use this version until further notice.

---
 README.md                                     |  2 +-
 .../daytona_bug2_ioctl_example_2.bpl.expect   |  3 +--
 Test/test15/CaptureState.bpl.expect           | 22 +++++++++----------
 3 files changed, 13 insertions(+), 14 deletions(-)

diff --git a/README.md b/README.md
index beb217fdf..9d5314c70 100644
--- a/README.md
+++ b/README.md
@@ -52,7 +52,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.4.1 or [CVC4](http://cvc4.cs.nyu.edu/web/) **FIXME_VERSION** (note
+- [Z3](https://github.com/Z3Prover/z3) 4.5.0 (earlier versions may also work, but the test suite assumes 4.5.0 to produce the expected output) 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 3c0d0b201..9f960f26c 100644
--- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
+++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
@@ -127,8 +127,7 @@ 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(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(3928,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_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 0363f36ee..32c36207f 100644
--- a/Test/test15/CaptureState.bpl.expect
+++ b/Test/test15/CaptureState.bpl.expect
@@ -14,18 +14,14 @@ $mv_state_const -> 3
 F -> T@FieldName!val!0
 Heap -> |T@[Ref,FieldName]Int!val!0|
 m -> **m
-m@0 -> (- 2)
-m@1 -> (- 1)
-m@3 -> (- 1)
+m@0 -> (- 276)
+m@1 -> (- 275)
+m@3 -> (- 275)
 r -> **r
-r@0 -> (- 2)
+r@0 -> (- 550)
 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 -> (- 2)
-  else -> (- 2)
-}
 $mv_state -> {
   3 0 -> true
   3 1 -> true
@@ -38,6 +34,10 @@ tickleBool -> {
   false -> true
   else -> true
 }
+Select_[Ref,FieldName]$int -> {
+  |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 276)
+  else -> (- 276)
+}
 *** STATE <initial>
   Heap -> |T@[Ref,FieldName]Int!val!0|
   this -> T@Ref!val!0
@@ -49,13 +49,13 @@ tickleBool -> {
 *** STATE top
 *** END_STATE
 *** STATE then
-  m -> (- 2)
+  m -> (- 276)
 *** END_STATE
 *** STATE postUpdate0
-  m -> (- 1)
+  m -> (- 275)
 *** END_STATE
 *** STATE end
-  r -> (- 2)
+  r -> (- 550)
   m -> 7
 *** END_STATE
 *** END_MODEL