Calibrated test output to Z3 version 4.5.0 (32-bit x86). Please use t…

…his version until further notice.

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

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

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