added HOL-Boogie
authorboehmes
Tue, 03 Nov 2009 17:54:24 +0100
changeset 33419 8ae45e87b992
parent 33418 1312e8337ce5
child 33423 281a01e5f68b
added HOL-Boogie
CONTRIBUTORS
NEWS
src/HOL/Boogie/Boogie.thy
src/HOL/Boogie/Examples/Boogie_Dijkstra.b2i
src/HOL/Boogie/Examples/Boogie_Dijkstra.thy
src/HOL/Boogie/Examples/Boogie_Max.b2i
src/HOL/Boogie/Examples/Boogie_Max.thy
src/HOL/Boogie/Examples/ROOT.ML
src/HOL/Boogie/Examples/VCC_Max.b2i
src/HOL/Boogie/Examples/VCC_Max.thy
src/HOL/Boogie/Examples/cert/Boogie_b_Dijkstra
src/HOL/Boogie/Examples/cert/Boogie_b_Dijkstra.proof
src/HOL/Boogie/Examples/cert/Boogie_b_max
src/HOL/Boogie/Examples/cert/Boogie_b_max.proof
src/HOL/Boogie/Examples/cert/VCC_b_maximum
src/HOL/Boogie/Examples/cert/VCC_b_maximum.proof
src/HOL/Boogie/ROOT.ML
src/HOL/Boogie/Tools/boogie_commands.ML
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/Boogie/Tools/boogie_split.ML
src/HOL/Boogie/Tools/boogie_vcs.ML
src/HOL/IsaMakefile
--- a/CONTRIBUTORS	Tue Nov 03 14:51:55 2009 +0100
+++ b/CONTRIBUTORS	Tue Nov 03 17:54:24 2009 +0100
@@ -7,6 +7,9 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* November 2009: Sascha Boehme, TUM
+  HOL-Boogie: an interactive prover back-end for Boogie and VCC
+
 * October 2009: Jasmin Blanchette, TUM
   Nitpick: yet another counterexample generator for Isabelle/HOL
 
--- a/NEWS	Tue Nov 03 14:51:55 2009 +0100
+++ b/NEWS	Tue Nov 03 17:54:24 2009 +0100
@@ -55,6 +55,10 @@
 this method is proof-producing. Certificates are provided to
 avoid calling the external solvers solely for re-checking proofs.
 
+* New commands to load and prove verification conditions
+generated by the Boogie program verifier or derived systems
+(e.g. the Verifying C Compiler (VCC) or Spec#).
+
 * New counterexample generator tool "nitpick" based on the Kodkod
 relational model finder.
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Boogie/Boogie.thy	Tue Nov 03 17:54:24 2009 +0100
@@ -0,0 +1,208 @@
+(*  Title:      HOL/Boogie/Boogie.thy
+    Author:     Sascha Boehme, TU Muenchen
+*)
+
+header {* Integration of the Boogie program verifier *}
+
+theory Boogie
+imports SMT
+uses
+  ("Tools/boogie_vcs.ML")
+  ("Tools/boogie_loader.ML")
+  ("Tools/boogie_commands.ML")
+  ("Tools/boogie_split.ML")
+begin
+
+section {* Built-in types and functions of Boogie *}
+
+subsection {* Labels *}
+
+text {*
+See "Generating error traces from verification-condition counterexamples"
+by Leino e.a. (2004) for a description of Boogie's labelling mechanism and
+semantics.
+*}
+
+definition assert_at :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "assert_at l P = P"
+definition block_at :: "bool \<Rightarrow> bool \<Rightarrow> bool" where "block_at l P = P"
+
+lemmas labels = assert_at_def block_at_def
+
+
+subsection {* Arrays *}
+
+abbreviation (input) boogie_select :: "('i \<Rightarrow> 'v) \<Rightarrow> 'i \<Rightarrow> 'v"
+where "boogie_select \<equiv> (\<lambda>f x. f x)"
+
+abbreviation (input) boogie_store :: 
+  "('i \<Rightarrow> 'v) \<Rightarrow> 'i \<Rightarrow> 'v \<Rightarrow> 'i \<Rightarrow> 'v"
+where "boogie_store \<equiv> fun_upd"
+
+
+subsection {* Integer arithmetics *}
+
+text {*
+The operations @{text div} and @{text mod} are built-in in Boogie, but
+without a particular semantics due to different interpretations in
+programming languages. We assume that each application comes with a
+proper axiomatization.
+*}
+
+axiomatization
+  boogie_div :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "div'_b" 70) and
+  boogie_mod :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "mod'_b" 70)
+
+
+subsection {* Bitvectors *}
+
+text {*
+Boogie's and Z3's built-in bitvector functions are modelled with
+functions of the HOL-Word library and the SMT theory of bitvectors.
+Every of the following bitvector functions is supported by the SMT
+binding.
+*}
+
+abbreviation (input) boogie_bv_concat :: 
+  "'a::len0 word \<Rightarrow> 'b::len0 word \<Rightarrow> 'c::len0 word"
+where "boogie_bv_concat \<equiv> (\<lambda>w1 w2. word_cat w1 w2)"
+
+abbreviation (input) boogie_bv_extract :: 
+  "nat \<Rightarrow> nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'b::len0 word"
+where "boogie_bv_extract \<equiv> (\<lambda>mb lb w. slice lb w)"
+
+abbreviation (input) z3_bvnot :: "'a::len0 word \<Rightarrow> 'a word"
+where "z3_bvnot \<equiv> (\<lambda>w. NOT w)"
+
+abbreviation (input) z3_bvand :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvand \<equiv> (\<lambda>w1 w2. w1 AND w2)"
+
+abbreviation (input) z3_bvor :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvor \<equiv> (\<lambda>w1 w2. w1 OR w2)"
+
+abbreviation (input) z3_bvxor :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvxor \<equiv> (\<lambda>w1 w2. w1 XOR w2)"
+
+abbreviation (input) z3_bvneg :: "'a::len0 word \<Rightarrow> 'a word"
+where "z3_bvneg \<equiv> (\<lambda>w. - w)"
+
+abbreviation (input) z3_bvadd :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvadd \<equiv> (\<lambda>w1 w2. w1 + w2)"
+
+abbreviation (input) z3_bvsub :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvsub \<equiv> (\<lambda>w1 w2. w1 - w2)"
+
+abbreviation (input) z3_bvmul :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvmul \<equiv> (\<lambda>w1 w2. w1 * w2)"
+
+abbreviation (input) z3_bvudiv :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvudiv \<equiv> (\<lambda>w1 w2. w1 div w2)"
+
+abbreviation (input) z3_bvurem :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvurem \<equiv> (\<lambda>w1 w2. w1 mod w2)"
+
+abbreviation (input) z3_bvsdiv :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvsdiv \<equiv> (\<lambda>w1 w2. w1 sdiv w2)"
+
+abbreviation (input) z3_bvsrem :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvsrem \<equiv> (\<lambda>w1 w2. w1 srem w2)"
+
+abbreviation (input) z3_bvshl :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvshl \<equiv> (\<lambda>w1 w2. bv_shl w1 w2)"
+
+abbreviation (input) z3_bvlshr :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvlshr \<equiv> (\<lambda>w1 w2. bv_lshr w1 w2)"
+
+abbreviation (input) z3_bvashr :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+where "z3_bvashr \<equiv> (\<lambda>w1 w2. bv_ashr w1 w2)"
+
+abbreviation (input) z3_sign_extend :: "'a::len word \<Rightarrow> 'b::len word"
+where "z3_sign_extend \<equiv> (\<lambda>w. scast w)"
+
+abbreviation (input) z3_zero_extend :: "'a::len0 word \<Rightarrow> 'b::len0 word"
+where "z3_zero_extend \<equiv> (\<lambda>w. ucast w)"
+
+abbreviation (input) z3_rotate_left :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'a word"
+where "z3_rotate_left \<equiv> (\<lambda>n w. word_rotl n w)"
+
+abbreviation (input) z3_rotate_right :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'a word"
+where "z3_rotate_right \<equiv> (\<lambda>n w. word_rotr n w)"
+
+abbreviation (input) z3_bvult :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> bool"
+where "z3_bvult \<equiv> (\<lambda>w1 w2. w1 < w2)"
+
+abbreviation (input) z3_bvule :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> bool"
+where "z3_bvule \<equiv> (\<lambda>w1 w2. w1 \<le> w2)"
+
+abbreviation (input) z3_bvugt :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> bool" 
+where "z3_bvugt \<equiv> (\<lambda>w1 w2. w1 > w2)"
+
+abbreviation (input) z3_bvuge :: "'a::len0 word \<Rightarrow> 'a word \<Rightarrow> bool" 
+where "z3_bvuge \<equiv> (\<lambda>w1 w2. w1 \<ge> w2)"
+
+abbreviation (input) z3_bvslt :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool"
+where "z3_bvslt \<equiv> (\<lambda>w1 w2. w1 <s w2)"
+
+abbreviation (input) z3_bvsle :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool"
+where "z3_bvsle \<equiv> (\<lambda>w1 w2. w1 <=s w2)"
+
+abbreviation (input) z3_bvsgt :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool"
+where "z3_bvsgt \<equiv> (\<lambda>w1 w2. w2 <s w1)"
+
+abbreviation (input) z3_bvsge :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool"
+where "z3_bvsge \<equiv> (\<lambda>w1 w2. w2 <=s w1)"
+
+
+section {* Boogie environment *}
+
+text {*
+Proving Boogie-generated verification conditions happens inside
+a Boogie environment:
+
+  boogie_open "b2i file without extension"
+  boogie_vc "verification condition 1" ...
+  boogie_vc "verification condition 2" ...
+  boogie_vc "verification condition 3" ...
+  boogie_end
+
+See the Boogie examples for more details.
+ 
+At most one Boogie environment should occur per theory,
+otherwise unexpected effects may arise.
+*}
+
+
+section {* Setup *}
+
+ML {*
+structure Boogie_Axioms = Named_Thms
+(
+  val name = "boogie"
+  val description = ("Boogie background axioms" ^
+    " loaded along with Boogie verification conditions")
+)
+*}
+setup Boogie_Axioms.setup
+
+text {*
+Opening a Boogie environment causes the following list of theorems to be
+enhanced by all theorems found in Boogie_Axioms.
+*}
+ML {*
+structure Split_VC_SMT_Rules = Named_Thms
+(
+  val name = "split_vc_smt"
+  val description = ("Theorems given to the SMT sub-tactic" ^
+    " of the split_vc method")
+)
+*}
+setup Split_VC_SMT_Rules.setup
+
+use "Tools/boogie_vcs.ML"
+use "Tools/boogie_loader.ML"
+use "Tools/boogie_commands.ML"
+setup Boogie_Commands.setup
+
+use "Tools/boogie_split.ML"
+setup Boogie_Split.setup
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.b2i	Tue Nov 03 17:54:24 2009 +0100
@@ -0,0 +1,1879 @@
+type-decl Vertex 0 0
+fun-decl G 1 0
+    array 3
+      type-con Vertex 0
+      type-con Vertex 0
+      int
+fun-decl Infinity 1 0
+    int
+fun-decl Source 1 0
+    type-con Vertex 0
+axiom 0
+    forall 2 0 3
+      var x
+        type-con Vertex 0
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.3:15
+      attribute uniqueId 1
+        string-attr 0
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    not
+    =
+    var x
+      type-con Vertex 0
+    var y
+      type-con Vertex 0
+    <
+    int-num 0
+    select 3
+    fun G 0
+    var x
+      type-con Vertex 0
+    var y
+      type-con Vertex 0
+axiom 0
+    forall 2 0 3
+      var x
+        type-con Vertex 0
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.4:15
+      attribute uniqueId 1
+        string-attr 1
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    =
+    var x
+      type-con Vertex 0
+    var y
+      type-con Vertex 0
+    =
+    select 3
+    fun G 0
+    var x
+      type-con Vertex 0
+    var y
+      type-con Vertex 0
+    int-num 0
+axiom 0
+    <
+    int-num 0
+    fun Infinity 0
+var-decl SP 0
+    array 2
+      type-con Vertex 0
+      int
+vc Dijkstra 1
+    implies
+    label pos 26 3
+    true
+    implies
+    true
+    implies
+    forall 1 0 3
+      var x
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.27:18
+      attribute uniqueId 1
+        string-attr 5
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    =
+    var x
+      type-con Vertex 0
+    fun Source 0
+    =
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var x
+      type-con Vertex 0
+    int-num 0
+    implies
+    forall 1 0 3
+      var x
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.28:18
+      attribute uniqueId 1
+        string-attr 6
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    not
+    =
+    var x
+      type-con Vertex 0
+    fun Source 0
+    =
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var x
+      type-con Vertex 0
+    fun Infinity 0
+    implies
+    forall 1 0 3
+      var x
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.31:18
+      attribute uniqueId 1
+        string-attr 7
+      attribute bvZ3Native 1
+        string-attr False
+    not
+    select 2
+    var Visited@0
+      array 2
+        type-con Vertex 0
+        bool
+    var x
+      type-con Vertex 0
+    implies
+    true
+    and 2
+    label neg 34 5
+    =
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    fun Source 0
+    int-num 0
+    implies
+    =
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    fun Source 0
+    int-num 0
+    and 2
+    label neg 35 5
+    forall 1 0 3
+      var x
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.35:23
+      attribute uniqueId 1
+        string-attr 9
+      attribute bvZ3Native 1
+        string-attr False
+    >=
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var x
+      type-con Vertex 0
+    int-num 0
+    implies
+    forall 1 0 3
+      var x
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.35:23
+      attribute uniqueId 1
+        string-attr 9
+      attribute bvZ3Native 1
+        string-attr False
+    >=
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var x
+      type-con Vertex 0
+    int-num 0
+    and 2
+    label neg 36 5
+    forall 2 0 3
+      var y
+        type-con Vertex 0
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.36:23
+      attribute uniqueId 1
+        string-attr 10
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    select 2
+    var Visited@0
+      array 2
+        type-con Vertex 0
+        bool
+    var z
+      type-con Vertex 0
+    select 2
+    var Visited@0
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    <=
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    implies
+    forall 2 0 3
+      var y
+        type-con Vertex 0
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.36:23
+      attribute uniqueId 1
+        string-attr 10
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    select 2
+    var Visited@0
+      array 2
+        type-con Vertex 0
+        bool
+    var z
+      type-con Vertex 0
+    select 2
+    var Visited@0
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    <=
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    and 2
+    label neg 38 5
+    forall 2 0 3
+      var z
+        type-con Vertex 0
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.38:23
+      attribute uniqueId 1
+        string-attr 11
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    select 2
+    var Visited@0
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    <
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    <=
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    implies
+    forall 2 0 3
+      var z
+        type-con Vertex 0
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.38:23
+      attribute uniqueId 1
+        string-attr 11
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    select 2
+    var Visited@0
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    <
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    <=
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    and 2
+    label neg 40 5
+    forall 1 0 3
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.40:23
+      attribute uniqueId 1
+        string-attr 13
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    =
+    var z
+      type-con Vertex 0
+    fun Source 0
+    <
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    exists 1 0 3
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.41:15
+      attribute uniqueId 1
+        string-attr 12
+      attribute bvZ3Native 1
+        string-attr False
+    and 3
+    <
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    select 2
+    var Visited@0
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    =
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    implies
+    forall 1 0 3
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.40:23
+      attribute uniqueId 1
+        string-attr 13
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    =
+    var z
+      type-con Vertex 0
+    fun Source 0
+    <
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    exists 1 0 3
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.41:15
+      attribute uniqueId 1
+        string-attr 12
+      attribute bvZ3Native 1
+        string-attr False
+    and 3
+    <
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    select 2
+    var Visited@0
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    =
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@0
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    implies
+    label pos 33 3
+    true
+    implies
+    true
+    implies
+    =
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    fun Source 0
+    int-num 0
+    implies
+    forall 1 0 3
+      var x
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.35:23
+      attribute uniqueId 1
+        string-attr 9
+      attribute bvZ3Native 1
+        string-attr False
+    >=
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var x
+      type-con Vertex 0
+    int-num 0
+    implies
+    forall 2 0 3
+      var y
+        type-con Vertex 0
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.36:23
+      attribute uniqueId 1
+        string-attr 10
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    select 2
+    var Visited@1
+      array 2
+        type-con Vertex 0
+        bool
+    var z
+      type-con Vertex 0
+    select 2
+    var Visited@1
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    <=
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    implies
+    forall 2 0 3
+      var z
+        type-con Vertex 0
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.38:23
+      attribute uniqueId 1
+        string-attr 11
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    select 2
+    var Visited@1
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    <
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    <=
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    implies
+    forall 1 0 3
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.40:23
+      attribute uniqueId 1
+        string-attr 13
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    =
+    var z
+      type-con Vertex 0
+    fun Source 0
+    <
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    exists 1 0 3
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.41:15
+      attribute uniqueId 1
+        string-attr 12
+      attribute bvZ3Native 1
+        string-attr False
+    and 3
+    <
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    select 2
+    var Visited@1
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    =
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    implies
+    true
+    and 2
+    implies
+    label pos 33 3
+    true
+    implies
+    true
+    implies
+    not
+    exists 1 0 3
+      var x
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.33:18
+      attribute uniqueId 1
+        string-attr 8
+      attribute bvZ3Native 1
+        string-attr False
+    and 2
+    not
+    select 2
+    var Visited@1
+      array 2
+        type-con Vertex 0
+        bool
+    var x
+      type-con Vertex 0
+    <
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var x
+      type-con Vertex 0
+    fun Infinity 0
+    implies
+    true
+    implies
+    label pos 0 0
+    true
+    implies
+    =
+    var Visited@3
+      array 2
+        type-con Vertex 0
+        bool
+    var Visited@1
+      array 2
+        type-con Vertex 0
+        bool
+    implies
+    =
+    var v@2
+      type-con Vertex 0
+    var v@0
+      type-con Vertex 0
+    implies
+    =
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    implies
+    =
+    var oldSP@1
+      array 2
+        type-con Vertex 0
+        int
+    var oldSP@0
+      array 2
+        type-con Vertex 0
+        int
+    implies
+    label pos 0 0
+    true
+    and 2
+    label neg 17 3
+    forall 1 0 3
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.17:19
+      attribute uniqueId 1
+        string-attr 4
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    =
+    var z
+      type-con Vertex 0
+    fun Source 0
+    <
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    exists 1 0 3
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.18:13
+      attribute uniqueId 1
+        string-attr 3
+      attribute bvZ3Native 1
+        string-attr False
+    and 2
+    <
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    =
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    implies
+    forall 1 0 3
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.17:19
+      attribute uniqueId 1
+        string-attr 4
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    =
+    var z
+      type-con Vertex 0
+    fun Source 0
+    <
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    exists 1 0 3
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.18:13
+      attribute uniqueId 1
+        string-attr 3
+      attribute bvZ3Native 1
+        string-attr False
+    and 2
+    <
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    =
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    and 2
+    label neg 15 3
+    forall 2 0 3
+      var z
+        type-con Vertex 0
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.15:19
+      attribute uniqueId 1
+        string-attr 2
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    fun Infinity 0
+    <
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    <=
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    implies
+    forall 2 0 3
+      var z
+        type-con Vertex 0
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.15:19
+      attribute uniqueId 1
+        string-attr 2
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    fun Infinity 0
+    <
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    <=
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    and 2
+    label neg 14 3
+    =
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    fun Source 0
+    int-num 0
+    implies
+    =
+    select 2
+    var SP@3
+      array 2
+        type-con Vertex 0
+        int
+    fun Source 0
+    int-num 0
+    true
+    implies
+    label pos 44 5
+    true
+    implies
+    true
+    implies
+    exists 1 0 3
+      var x
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.33:18
+      attribute uniqueId 1
+        string-attr 8
+      attribute bvZ3Native 1
+        string-attr False
+    and 2
+    not
+    select 2
+    var Visited@1
+      array 2
+        type-con Vertex 0
+        bool
+    var x
+      type-con Vertex 0
+    <
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var x
+      type-con Vertex 0
+    fun Infinity 0
+    implies
+    not
+    select 2
+    var Visited@1
+      array 2
+        type-con Vertex 0
+        bool
+    var v@1
+      type-con Vertex 0
+    implies
+    <
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var v@1
+      type-con Vertex 0
+    fun Infinity 0
+    implies
+    forall 1 0 3
+      var x
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.47:20
+      attribute uniqueId 1
+        string-attr 14
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    not
+    select 2
+    var Visited@1
+      array 2
+        type-con Vertex 0
+        bool
+    var x
+      type-con Vertex 0
+    <=
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var v@1
+      type-con Vertex 0
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var x
+      type-con Vertex 0
+    implies
+    =
+    var Visited@2
+      array 2
+        type-con Vertex 0
+        bool
+    store 3
+    var Visited@1
+      array 2
+        type-con Vertex 0
+        bool
+    var v@1
+      type-con Vertex 0
+    true
+    implies
+    forall 1 0 3
+      var u
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.53:20
+      attribute uniqueId 1
+        string-attr 15
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <
+    select 3
+    fun G 0
+    var v@1
+      type-con Vertex 0
+    var u
+      type-con Vertex 0
+    fun Infinity 0
+    <
+    +
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var v@1
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var v@1
+      type-con Vertex 0
+    var u
+      type-con Vertex 0
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var u
+      type-con Vertex 0
+    =
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var u
+      type-con Vertex 0
+    +
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var v@1
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var v@1
+      type-con Vertex 0
+    var u
+      type-con Vertex 0
+    implies
+    forall 1 0 3
+      var u
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.56:20
+      attribute uniqueId 1
+        string-attr 16
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    not
+    and 2
+    <
+    select 3
+    fun G 0
+    var v@1
+      type-con Vertex 0
+    var u
+      type-con Vertex 0
+    fun Infinity 0
+    <
+    +
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var v@1
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var v@1
+      type-con Vertex 0
+    var u
+      type-con Vertex 0
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var u
+      type-con Vertex 0
+    =
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var u
+      type-con Vertex 0
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var u
+      type-con Vertex 0
+    and 2
+    label neg 59 5
+    forall 1 0 3
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.59:20
+      attribute uniqueId 1
+        string-attr 17
+      attribute bvZ3Native 1
+        string-attr False
+    <=
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    implies
+    forall 1 0 3
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.59:20
+      attribute uniqueId 1
+        string-attr 17
+      attribute bvZ3Native 1
+        string-attr False
+    <=
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    and 2
+    label neg 60 5
+    forall 1 0 3
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.60:20
+      attribute uniqueId 1
+        string-attr 18
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    select 2
+    var Visited@2
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    =
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    implies
+    forall 1 0 3
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.60:20
+      attribute uniqueId 1
+        string-attr 18
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    select 2
+    var Visited@2
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    =
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@1
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    implies
+    true
+    implies
+    label pos 0 0
+    true
+    and 2
+    label neg 34 5
+    =
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    fun Source 0
+    int-num 0
+    implies
+    =
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    fun Source 0
+    int-num 0
+    and 2
+    label neg 35 5
+    forall 1 0 3
+      var x
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.35:23
+      attribute uniqueId 1
+        string-attr 9
+      attribute bvZ3Native 1
+        string-attr False
+    >=
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var x
+      type-con Vertex 0
+    int-num 0
+    implies
+    forall 1 0 3
+      var x
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.35:23
+      attribute uniqueId 1
+        string-attr 9
+      attribute bvZ3Native 1
+        string-attr False
+    >=
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var x
+      type-con Vertex 0
+    int-num 0
+    and 2
+    label neg 36 5
+    forall 2 0 3
+      var y
+        type-con Vertex 0
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.36:23
+      attribute uniqueId 1
+        string-attr 10
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    select 2
+    var Visited@2
+      array 2
+        type-con Vertex 0
+        bool
+    var z
+      type-con Vertex 0
+    select 2
+    var Visited@2
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    <=
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    implies
+    forall 2 0 3
+      var y
+        type-con Vertex 0
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.36:23
+      attribute uniqueId 1
+        string-attr 10
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    select 2
+    var Visited@2
+      array 2
+        type-con Vertex 0
+        bool
+    var z
+      type-con Vertex 0
+    select 2
+    var Visited@2
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    <=
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    and 2
+    label neg 38 5
+    forall 2 0 3
+      var z
+        type-con Vertex 0
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.38:23
+      attribute uniqueId 1
+        string-attr 11
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    select 2
+    var Visited@2
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    <
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    <=
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    implies
+    forall 2 0 3
+      var z
+        type-con Vertex 0
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.38:23
+      attribute uniqueId 1
+        string-attr 11
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    select 2
+    var Visited@2
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    <
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    <=
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    and 2
+    label neg 40 5
+    forall 1 0 3
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.40:23
+      attribute uniqueId 1
+        string-attr 13
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    =
+    var z
+      type-con Vertex 0
+    fun Source 0
+    <
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    exists 1 0 3
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.41:15
+      attribute uniqueId 1
+        string-attr 12
+      attribute bvZ3Native 1
+        string-attr False
+    and 3
+    <
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    select 2
+    var Visited@2
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    =
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    implies
+    forall 1 0 3
+      var z
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.40:23
+      attribute uniqueId 1
+        string-attr 13
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    =
+    var z
+      type-con Vertex 0
+    fun Source 0
+    <
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    fun Infinity 0
+    exists 1 0 3
+      var y
+        type-con Vertex 0
+      attribute qid 1
+        string-attr BoogieDi.41:15
+      attribute uniqueId 1
+        string-attr 12
+      attribute bvZ3Native 1
+        string-attr False
+    and 3
+    <
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    select 2
+    var Visited@2
+      array 2
+        type-con Vertex 0
+        bool
+    var y
+      type-con Vertex 0
+    =
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var z
+      type-con Vertex 0
+    +
+    select 2
+    var SP@2
+      array 2
+        type-con Vertex 0
+        int
+    var y
+      type-con Vertex 0
+    select 3
+    fun G 0
+    var y
+      type-con Vertex 0
+    var z
+      type-con Vertex 0
+    implies
+    false
+    true
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy	Tue Nov 03 17:54:24 2009 +0100
@@ -0,0 +1,92 @@
+(*  Title:      HOL/Boogie/Examples/Boogie_Dijkstra.thy
+    Author:     Sascha Boehme, TU Muenchen
+*)
+
+header {* Boogie example: Dijkstra's algorithm *}
+
+theory Boogie_Dijkstra
+imports Boogie
+begin
+
+text {*
+We prove correct the verification condition generated from the following
+Boogie code:
+
+\begin{verbatim}
+type Vertex;
+const G: [Vertex, Vertex] int;
+axiom (forall x: Vertex, y: Vertex ::  x != y ==> 0 < G[x,y]);
+axiom (forall x: Vertex, y: Vertex ::  x == y ==> G[x,y] == 0);
+
+const Infinity: int;
+axiom 0 < Infinity;
+
+const Source: Vertex;
+var SP: [Vertex] int;
+
+procedure Dijkstra();
+  modifies SP;
+  ensures (SP[Source] == 0);
+  ensures (forall z: Vertex, y: Vertex ::
+    SP[y] < Infinity && G[y,z] < Infinity ==> SP[z] <= SP[y] + G[y,z]);
+  ensures (forall z: Vertex :: z != Source && SP[z] < Infinity ==>
+    (exists y: Vertex :: SP[y] < SP[z] && SP[z] == SP[y] + G[y,z]));
+
+implementation Dijkstra()
+{
+  var v: Vertex;
+  var Visited: [Vertex] bool;
+  var oldSP: [Vertex] int;
+
+  havoc SP;
+  assume (forall x: Vertex :: x == Source ==> SP[x] == 0);
+  assume (forall x: Vertex :: x != Source ==> SP[x] == Infinity);
+
+  havoc Visited;
+  assume (forall x: Vertex :: !Visited[x]);
+            
+  while ((exists x: Vertex :: !Visited[x] && SP[x] < Infinity))
+    invariant (SP[Source] == 0);
+    invariant (forall x: Vertex :: SP[x] >= 0);
+    invariant (forall y: Vertex, z: Vertex :: 
+      !Visited[z] && Visited[y] ==> SP[y] <= SP[z]);
+    invariant (forall z: Vertex, y: Vertex ::
+      Visited[y] && G[y,z] < Infinity ==> SP[z] <= SP[y] + G[y,z]);
+    invariant (forall z: Vertex :: z != Source && SP[z] < Infinity ==>
+      (exists y: Vertex :: SP[y] < SP[z] && Visited[y] && 
+        SP[z] == SP[y] + G[y,z]));
+  {
+    havoc v;
+    assume (!Visited[v]);
+    assume (SP[v] < Infinity); 
+    assume (forall x: Vertex :: !Visited[x] ==> SP[v] <= SP[x]);
+
+    Visited[v] := true;
+
+    oldSP := SP;
+    havoc SP;
+    assume (forall u: Vertex :: 
+      G[v,u] < Infinity && oldSP[v] + G[v,u] < oldSP[u] ==> 
+        SP[u] == oldSP[v] + G[v,u]);
+    assume (forall u: Vertex :: 
+      !(G[v,u] < Infinity && oldSP[v] + G[v,u] < oldSP[u]) ==> 
+        SP[u] == oldSP[u]);
+    assert (forall z: Vertex:: SP[z] <= oldSP[z]);
+    assert (forall y: Vertex:: Visited[y] ==> SP[y] == oldSP[y]);
+  }
+}
+\end{verbatim}
+*}
+
+
+boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Dijkstra"
+
+boogie_vc b_Dijkstra
+  unfolding labels
+  using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_b_Dijkstra"]]
+  using [[z3_proofs=true]]
+  by (smt boogie)
+
+boogie_end 
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Boogie/Examples/Boogie_Max.b2i	Tue Nov 03 17:54:24 2009 +0100
@@ -0,0 +1,748 @@
+vc max 1
+    implies
+    label pos 10 7
+    true
+    implies
+    <
+    int-num 0
+    var length
+      int
+    implies
+    true
+    implies
+    =
+    var max@0
+      int
+    select 2
+    var array
+      array 2
+        int
+        int
+    int-num 0
+    implies
+    and 4
+    <=
+    int-num 0
+    int-num 0
+    <=
+    int-num 0
+    int-num 0
+    <=
+    int-num 1
+    int-num 1
+    <=
+    int-num 1
+    int-num 1
+    and 2
+    label neg 14 5
+    forall 1 0 3
+      var i
+        int
+      attribute qid 1
+        string-attr BoogieMa.14:23
+      attribute uniqueId 1
+        string-attr 2
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    int-num 1
+    <=
+    select 2
+    var array
+      array 2
+        int
+        int
+    var i
+      int
+    var max@0
+      int
+    implies
+    forall 1 0 3
+      var i
+        int
+      attribute qid 1
+        string-attr BoogieMa.14:23
+      attribute uniqueId 1
+        string-attr 2
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    int-num 1
+    <=
+    select 2
+    var array
+      array 2
+        int
+        int
+    var i
+      int
+    var max@0
+      int
+    and 2
+    label neg 15 5
+    =
+    select 2
+    var array
+      array 2
+        int
+        int
+    int-num 0
+    var max@0
+      int
+    implies
+    =
+    select 2
+    var array
+      array 2
+        int
+        int
+    int-num 0
+    var max@0
+      int
+    implies
+    label pos 13 3
+    true
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@0
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    implies
+    forall 1 0 3
+      var i
+        int
+      attribute qid 1
+        string-attr BoogieMa.14:23
+      attribute uniqueId 1
+        string-attr 2
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var p@0
+      int
+    <=
+    select 2
+    var array
+      array 2
+        int
+        int
+    var i
+      int
+    var max@1
+      int
+    implies
+    =
+    select 2
+    var array
+      array 2
+        int
+        int
+    var k@0
+      int
+    var max@1
+      int
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@0
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    and 2
+    implies
+    label pos 13 3
+    true
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@0
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    implies
+    >=
+    var p@0
+      int
+    var length
+      int
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@0
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    implies
+    label pos 0 0
+    true
+    implies
+    =
+    var k@2
+      int
+    var k@0
+      int
+    implies
+    =
+    var max@4
+      int
+    var max@1
+      int
+    implies
+    =
+    var p@2
+      int
+    var p@0
+      int
+    implies
+    label pos 0 0
+    true
+    and 2
+    label neg 5 3
+    exists 1 0 3
+      var i
+        int
+      attribute qid 1
+        string-attr BoogieMa.5:19
+      attribute uniqueId 1
+        string-attr 1
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var length
+      int
+    =
+    select 2
+    var array
+      array 2
+        int
+        int
+    var i
+      int
+    var max@4
+      int
+    implies
+    exists 1 0 3
+      var i
+        int
+      attribute qid 1
+        string-attr BoogieMa.5:19
+      attribute uniqueId 1
+        string-attr 1
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var length
+      int
+    =
+    select 2
+    var array
+      array 2
+        int
+        int
+    var i
+      int
+    var max@4
+      int
+    and 2
+    label neg 4 3
+    forall 1 0 3
+      var i
+        int
+      attribute qid 1
+        string-attr BoogieMa.4:19
+      attribute uniqueId 1
+        string-attr 0
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var length
+      int
+    <=
+    select 2
+    var array
+      array 2
+        int
+        int
+    var i
+      int
+    var max@4
+      int
+    implies
+    forall 1 0 3
+      var i
+        int
+      attribute qid 1
+        string-attr BoogieMa.4:19
+      attribute uniqueId 1
+        string-attr 0
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var length
+      int
+    <=
+    select 2
+    var array
+      array 2
+        int
+        int
+    var i
+      int
+    var max@4
+      int
+    true
+    implies
+    label pos 17 5
+    true
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@0
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    implies
+    <
+    var p@0
+      int
+    var length
+      int
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@0
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    and 2
+    implies
+    label pos 17 31
+    true
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@0
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    implies
+    >
+    select 2
+    var array
+      array 2
+        int
+        int
+    var p@0
+      int
+    var max@1
+      int
+    implies
+    =
+    var max@2
+      int
+    select 2
+    var array
+      array 2
+        int
+        int
+    var p@0
+      int
+    implies
+    and 2
+    <=
+    int-num 1
+    var p@0
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    implies
+    label pos 0 0
+    true
+    implies
+    =
+    var k@1
+      int
+    var p@0
+      int
+    implies
+    =
+    var max@3
+      int
+    var max@2
+      int
+    implies
+    label pos 18 7
+    true
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@1
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    implies
+    =
+    var p@1
+      int
+    +
+    var p@0
+      int
+    int-num 1
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@1
+      int
+    <=
+    int-num 2
+    var p@1
+      int
+    implies
+    label pos 0 0
+    true
+    and 2
+    label neg 14 5
+    forall 1 0 3
+      var i
+        int
+      attribute qid 1
+        string-attr BoogieMa.14:23
+      attribute uniqueId 1
+        string-attr 2
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var p@1
+      int
+    <=
+    select 2
+    var array
+      array 2
+        int
+        int
+    var i
+      int
+    var max@3
+      int
+    implies
+    forall 1 0 3
+      var i
+        int
+      attribute qid 1
+        string-attr BoogieMa.14:23
+      attribute uniqueId 1
+        string-attr 2
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var p@1
+      int
+    <=
+    select 2
+    var array
+      array 2
+        int
+        int
+    var i
+      int
+    var max@3
+      int
+    and 2
+    label neg 15 5
+    =
+    select 2
+    var array
+      array 2
+        int
+        int
+    var k@1
+      int
+    var max@3
+      int
+    implies
+    =
+    select 2
+    var array
+      array 2
+        int
+        int
+    var k@1
+      int
+    var max@3
+      int
+    implies
+    false
+    true
+    implies
+    label pos 17 5
+    true
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@0
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    implies
+    <=
+    select 2
+    var array
+      array 2
+        int
+        int
+    var p@0
+      int
+    var max@1
+      int
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@0
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    implies
+    label pos 0 0
+    true
+    implies
+    =
+    var k@1
+      int
+    var k@0
+      int
+    implies
+    =
+    var max@3
+      int
+    var max@1
+      int
+    implies
+    label pos 18 7
+    true
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@1
+      int
+    <=
+    int-num 1
+    var p@0
+      int
+    implies
+    =
+    var p@1
+      int
+    +
+    var p@0
+      int
+    int-num 1
+    implies
+    and 2
+    <=
+    int-num 0
+    var k@1
+      int
+    <=
+    int-num 2
+    var p@1
+      int
+    implies
+    label pos 0 0
+    true
+    and 2
+    label neg 14 5
+    forall 1 0 3
+      var i
+        int
+      attribute qid 1
+        string-attr BoogieMa.14:23
+      attribute uniqueId 1
+        string-attr 2
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var p@1
+      int
+    <=
+    select 2
+    var array
+      array 2
+        int
+        int
+    var i
+      int
+    var max@3
+      int
+    implies
+    forall 1 0 3
+      var i
+        int
+      attribute qid 1
+        string-attr BoogieMa.14:23
+      attribute uniqueId 1
+        string-attr 2
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var p@1
+      int
+    <=
+    select 2
+    var array
+      array 2
+        int
+        int
+    var i
+      int
+    var max@3
+      int
+    and 2
+    label neg 15 5
+    =
+    select 2
+    var array
+      array 2
+        int
+        int
+    var k@1
+      int
+    var max@3
+      int
+    implies
+    =
+    select 2
+    var array
+      array 2
+        int
+        int
+    var k@1
+      int
+    var max@3
+      int
+    implies
+    false
+    true
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Tue Nov 03 17:54:24 2009 +0100
@@ -0,0 +1,49 @@
+(*  Title:      HOL/Boogie/Examples/Boogie_Dijkstra.thy
+    Author:     Sascha Boehme, TU Muenchen
+*)
+
+header {* Boogie example: get the greatest element of a list *}
+
+theory Boogie_Max
+imports Boogie
+begin
+
+text {*
+We prove correct the verification condition generated from the following
+Boogie code:
+
+\begin{verbatim}
+procedure max(array : [int]int, length : int)
+  returns (max : int);
+  requires (0 < length);
+  ensures (forall i: int :: 0 <= i && i < length ==> array[i] <= max);
+  ensures (exists i: int :: 0 <= i && i < length ==> array[i] == max);
+
+implementation max(array : [int]int, length : int) returns (max : int)
+{
+  var p : int, k : int;
+  max := array[0];
+  k := 0;
+  p := 1;
+  while (p < length)
+    invariant (forall i: int :: 0 <= i && i < p ==> array[i] <= max);
+    invariant (array[k] == max);
+  {
+    if (array[p] > max) { max := array[p]; k := p; }
+    p := p + 1;
+  }
+}
+\end{verbatim}
+*}
+
+boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
+
+boogie_vc b_max
+  unfolding labels
+  using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_b_max"]]
+  using [[z3_proofs=true]]
+  by (smt boogie)
+
+boogie_end
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Boogie/Examples/ROOT.ML	Tue Nov 03 17:54:24 2009 +0100
@@ -0,0 +1,3 @@
+use_thy "Boogie_Max";
+use_thy "Boogie_Dijkstra";
+use_thy "VCC_Max";
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Boogie/Examples/VCC_Max.b2i	Tue Nov 03 17:54:24 2009 +0100
@@ -0,0 +1,19619 @@
+type-decl $ctype 0 0
+type-decl $ptr 0 0
+type-decl $field 0 0
+type-decl $kind 0 0
+type-decl $type_state 0 0
+type-decl $status 0 0
+type-decl $primitive 0 0
+type-decl $struct 0 0
+type-decl $token 0 0
+type-decl $state 0 0
+type-decl $pure_function 0 0
+type-decl $label 0 0
+type-decl $memory_t 0 0
+type-decl $typemap_t 0 0
+type-decl $statusmap_t 0 0
+type-decl $record 0 0
+type-decl $version 0 0
+type-decl $vol_version 0 0
+type-decl $ptrset 0 0
+fun-decl $kind_of 2 0
+    type-con $ctype 0
+    type-con $kind 0
+fun-decl $kind_composite 1 1
+    type-con $kind 0
+  attribute unique 0
+fun-decl $kind_primitive 1 1
+    type-con $kind 0
+  attribute unique 0
+fun-decl $kind_array 1 1
+    type-con $kind 0
+  attribute unique 0
+fun-decl $kind_thread 1 1
+    type-con $kind 0
+  attribute unique 0
+fun-decl $sizeof 2 0
+    type-con $ctype 0
+    int
+fun-decl ^^i1 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^i2 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^i4 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^i8 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^u1 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^u2 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^u4 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^u8 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^void 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^bool 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^f4 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^f8 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^claim 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^root_emb 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^^mathint 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^$#thread_id_t 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^$#ptrset 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^$#state_t 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl ^$#struct 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl $ptr_to 2 0
+    type-con $ctype 0
+    type-con $ctype 0
+fun-decl $unptr_to 2 0
+    type-con $ctype 0
+    type-con $ctype 0
+fun-decl $ptr_level 2 0
+    type-con $ctype 0
+    int
+fun-decl $map_t 3 0
+    type-con $ctype 0
+    type-con $ctype 0
+    type-con $ctype 0
+fun-decl $map_domain 2 0
+    type-con $ctype 0
+    type-con $ctype 0
+fun-decl $map_range 2 0
+    type-con $ctype 0
+    type-con $ctype 0
+fun-decl $is_primitive 2 1
+    type-con $ctype 0
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $is_primitive_ch 2 1
+    type-con $ctype 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_composite 2 1
+    type-con $ctype 0
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $is_composite_ch 2 1
+    type-con $ctype 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_arraytype 2 1
+    type-con $ctype 0
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $is_arraytype_ch 2 1
+    type-con $ctype 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_threadtype 2 1
+    type-con $ctype 0
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $is_thread 2 1
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_ptr_to_composite 2 1
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $field_offset 2 0
+    type-con $field 0
+    int
+fun-decl $field_parent_type 2 0
+    type-con $field 0
+    type-con $ctype 0
+fun-decl $is_non_primitive 2 0
+    type-con $ctype 0
+    bool
+fun-decl $is_non_primitive_ch 2 1
+    type-con $ctype 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_non_primitive_ptr 2 1
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $me_ref 1 0
+    int
+fun-decl $me 1 0
+    type-con $ptr 0
+fun-decl $current_state 2 1
+    type-con $state 0
+    type-con $state 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $select.mem 3 0
+    type-con $memory_t 0
+    type-con $ptr 0
+    int
+fun-decl $store.mem 4 0
+    type-con $memory_t 0
+    type-con $ptr 0
+    int
+    type-con $memory_t 0
+fun-decl $select.tm 3 0
+    type-con $typemap_t 0
+    type-con $ptr 0
+    type-con $type_state 0
+fun-decl $store.tm 4 0
+    type-con $typemap_t 0
+    type-con $ptr 0
+    type-con $type_state 0
+    type-con $typemap_t 0
+fun-decl $select.sm 3 0
+    type-con $statusmap_t 0
+    type-con $ptr 0
+    type-con $status 0
+fun-decl $store.sm 4 0
+    type-con $statusmap_t 0
+    type-con $ptr 0
+    type-con $status 0
+    type-con $statusmap_t 0
+fun-decl $memory 2 0
+    type-con $state 0
+    type-con $memory_t 0
+fun-decl $typemap 2 0
+    type-con $state 0
+    type-con $typemap_t 0
+fun-decl $statusmap 2 0
+    type-con $state 0
+    type-con $statusmap_t 0
+fun-decl $mem 3 1
+    type-con $state 0
+    type-con $ptr 0
+    int
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $read_any 3 1
+    type-con $state 0
+    type-con $ptr 0
+    int
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $mem_eq 4 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $st_eq 4 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $ts_eq 4 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $extent_hint 3 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+fun-decl $nesting_level 2 0
+    type-con $ctype 0
+    int
+fun-decl $is_nested 3 0
+    type-con $ctype 0
+    type-con $ctype 0
+    bool
+fun-decl $nesting_min 3 0
+    type-con $ctype 0
+    type-con $ctype 0
+    int
+fun-decl $nesting_max 3 0
+    type-con $ctype 0
+    type-con $ctype 0
+    int
+fun-decl $is_nested_range 5 0
+    type-con $ctype 0
+    type-con $ctype 0
+    int
+    int
+    bool
+fun-decl $typ 2 0
+    type-con $ptr 0
+    type-con $ctype 0
+fun-decl $ref 2 0
+    type-con $ptr 0
+    int
+fun-decl $ptr 3 0
+    type-con $ctype 0
+    int
+    type-con $ptr 0
+fun-decl $ghost_ref 3 0
+    type-con $ptr 0
+    type-con $field 0
+    int
+fun-decl $ghost_emb 2 0
+    int
+    type-con $ptr 0
+fun-decl $ghost_path 2 0
+    int
+    type-con $field 0
+fun-decl $physical_ref 3 0
+    type-con $ptr 0
+    type-con $field 0
+    int
+fun-decl $array_path 3 0
+    type-con $field 0
+    int
+    type-con $field 0
+fun-decl $is_base_field 2 0
+    type-con $field 0
+    bool
+fun-decl $array_path_1 2 0
+    type-con $field 0
+    type-con $field 0
+fun-decl $array_path_2 2 0
+    type-con $field 0
+    int
+fun-decl $null 1 0
+    type-con $ptr 0
+fun-decl $is 3 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+fun-decl $ptr_cast 3 1
+    type-con $ptr 0
+    type-con $ctype 0
+    type-con $ptr 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $read_ptr 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    type-con $ptr 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $dot 3 0
+    type-con $ptr 0
+    type-con $field 0
+    type-con $ptr 0
+fun-decl $emb 3 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $path 3 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $field 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $containing_struct 3 0
+    type-con $ptr 0
+    type-con $field 0
+    type-con $ptr 0
+fun-decl $containing_struct_ref 3 0
+    type-con $ptr 0
+    type-con $field 0
+    int
+fun-decl $is_primitive_non_volatile_field 2 0
+    type-con $field 0
+    bool
+fun-decl $is_primitive_volatile_field 2 0
+    type-con $field 0
+    bool
+fun-decl $is_primitive_embedded_array 3 0
+    type-con $field 0
+    int
+    bool
+fun-decl $is_primitive_embedded_volatile_array 4 0
+    type-con $field 0
+    int
+    type-con $ctype 0
+    bool
+fun-decl $static_field_properties 3 1
+    type-con $field 0
+    type-con $ctype 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $field_properties 6 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $field 0
+    type-con $ctype 0
+    bool
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $ts_typed 2 0
+    type-con $type_state 0
+    bool
+fun-decl $ts_emb 2 0
+    type-con $type_state 0
+    type-con $ptr 0
+fun-decl $ts_path 2 0
+    type-con $type_state 0
+    type-con $field 0
+fun-decl $ts_is_array_elt 2 0
+    type-con $type_state 0
+    bool
+fun-decl $ts_is_volatile 2 0
+    type-con $type_state 0
+    bool
+fun-decl $is_object_root 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_volatile 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_malloc_root 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $current_timestamp 2 0
+    type-con $state 0
+    int
+fun-decl $is_fresh 4 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_writes_at 3 0
+    int
+    type-con $ptr 0
+    bool
+fun-decl $writable 4 1
+    type-con $state 0
+    int
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $top_writable 4 1
+    type-con $state 0
+    int
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $struct_zero 1 0
+    type-con $struct 0
+fun-decl $vs_base 3 1
+    type-con $struct 0
+    type-con $ctype 0
+    type-con $ptr 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $vs_base_ref 2 0
+    type-con $struct 0
+    int
+fun-decl $vs_state 2 0
+    type-con $struct 0
+    type-con $state 0
+fun-decl $vs_ctor 3 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $struct 0
+fun-decl $rec_zero 1 0
+    type-con $record 0
+fun-decl $rec_update 4 0
+    type-con $record 0
+    type-con $field 0
+    int
+    type-con $record 0
+fun-decl $rec_fetch 3 0
+    type-con $record 0
+    type-con $field 0
+    int
+fun-decl $rec_update_bv 7 0
+    type-con $record 0
+    type-con $field 0
+    int
+    int
+    int
+    int
+    type-con $record 0
+fun-decl $is_record_type 2 0
+    type-con $ctype 0
+    bool
+fun-decl $is_record_field 4 0
+    type-con $ctype 0
+    type-con $field 0
+    type-con $ctype 0
+    bool
+fun-decl $as_record_record_field 2 0
+    type-con $field 0
+    type-con $field 0
+fun-decl $rec_eq 3 0
+    type-con $record 0
+    type-con $record 0
+    bool
+fun-decl $rec_base_eq 3 0
+    int
+    int
+    bool
+fun-decl $int_to_record 2 0
+    int
+    type-con $record 0
+fun-decl $record_to_int 2 0
+    type-con $record 0
+    int
+fun-decl $good_state 2 0
+    type-con $state 0
+    bool
+fun-decl $invok_state 2 0
+    type-con $state 0
+    bool
+fun-decl $has_volatile_owns_set 2 0
+    type-con $ctype 0
+    bool
+fun-decl $owns_set_field 2 0
+    type-con $ctype 0
+    type-con $field 0
+fun-decl $st_owner 2 0
+    type-con $status 0
+    type-con $ptr 0
+fun-decl $st_closed 2 0
+    type-con $status 0
+    bool
+fun-decl $st_timestamp 2 0
+    type-con $status 0
+    int
+fun-decl $st_ref_cnt 2 0
+    type-con $status 0
+    int
+fun-decl $owner 3 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+fun-decl $closed 3 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+fun-decl $timestamp 3 0
+    type-con $state 0
+    type-con $ptr 0
+    int
+fun-decl $position_marker 1 0
+    bool
+fun-decl $st 3 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $status 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $ts 3 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $type_state 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $owns 3 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptrset 0
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $nested 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $nested_in 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $wrapped 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $irrelevant 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $mutable 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $thread_owned 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $thread_owned_or_even_mutable 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $typed 3 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+fun-decl $typed2 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $ptr_eq 3 1
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $ptr_neq 3 1
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_primitive_field_of 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $instantiate_st 2 0
+    type-con $status 0
+    bool
+fun-decl $is_domain_root 3 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+fun-decl $in_wrapped_domain 3 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+fun-decl $thread_local_np 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $thread_local 3 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+fun-decl $thread_local2 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $dont_instantiate 2 0
+    type-con $ptr 0
+    bool
+fun-decl $dont_instantiate_int 2 0
+    int
+    bool
+fun-decl $dont_instantiate_state 2 0
+    type-con $state 0
+    bool
+fun-decl $instantiate_int 2 0
+    int
+    bool
+fun-decl $instantiate_bool 2 0
+    bool
+    bool
+fun-decl $instantiate_ptr 2 0
+    type-con $ptr 0
+    bool
+fun-decl $instantiate_ptrset 2 0
+    type-con $ptrset 0
+    bool
+fun-decl $inv 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $inv2nt 4 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $imply_inv 4 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+fun-decl $inv2 5 0
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+fun-decl $inv2_when_closed 5 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $sequential 5 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $depends 5 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $spans_the_same 5 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $state_spans_the_same 5 0
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+fun-decl $nonvolatile_spans_the_same 5 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $state_nonvolatile_spans_the_same 5 0
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+fun-decl $in_extent_of 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_full_extent_of 3 1
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $extent_mutable 3 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+fun-decl $extent_is_fresh 4 0
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+fun-decl $forall_inv2_when_closed 3 1
+    type-con $state 0
+    type-con $state 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $function_entry 2 0
+    type-con $state 0
+    bool
+fun-decl $full_stop 2 0
+    type-con $state 0
+    bool
+fun-decl $full_stop_ext 3 1
+    type-con $token 0
+    type-con $state 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $file_name_is 3 0
+    int
+    type-con $token 0
+    bool
+fun-decl $closed_is_transitive 2 1
+    type-con $state 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $call_transition 3 0
+    type-con $state 0
+    type-con $state 0
+    bool
+fun-decl $good_state_ext 3 0
+    type-con $token 0
+    type-con $state 0
+    bool
+fun-decl $local_value_is 6 0
+    type-con $state 0
+    type-con $token 0
+    type-con $token 0
+    int
+    type-con $ctype 0
+    bool
+fun-decl $local_value_is_ptr 6 0
+    type-con $state 0
+    type-con $token 0
+    type-con $token 0
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+fun-decl $read_ptr_m 4 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    type-con $ptr 0
+fun-decl $type_code_is 3 0
+    int
+    type-con $ctype 0
+    bool
+fun-decl $function_arg_type 4 0
+    type-con $pure_function 0
+    int
+    type-con $ctype 0
+    bool
+fun-decl $ver_domain 2 0
+    type-con $version 0
+    type-con $ptrset 0
+fun-decl $read_version 3 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $version 0
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $domain 3 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptrset 0
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $in_domain 4 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+fun-decl $in_vdomain 4 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+fun-decl $in_domain_lab 5 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $label 0
+    bool
+fun-decl $in_vdomain_lab 5 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $label 0
+    bool
+fun-decl $inv_lab 4 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $label 0
+    bool
+fun-decl $dom_thread_local 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $fetch_from_domain 3 0
+    type-con $version 0
+    type-con $ptr 0
+    int
+fun-decl $in_claim_domain 3 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+fun-decl $by_claim 5 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $ptr 0
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $claim_version 2 0
+    type-con $ptr 0
+    type-con $version 0
+fun-decl $read_vol_version 3 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $vol_version 0
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $fetch_from_vv 3 0
+    type-con $vol_version 0
+    type-con $ptr 0
+    int
+fun-decl $fetch_vol_field 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $field 0
+    int
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_approved_by 4 0
+    type-con $ctype 0
+    type-con $field 0
+    type-con $field 0
+    bool
+fun-decl $inv_is_approved_by_ptr 6 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $field 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $inv_is_approved_by 6 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $field 0
+    type-con $field 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_owner_approved 3 0
+    type-con $ctype 0
+    type-con $field 0
+    bool
+fun-decl $inv_is_owner_approved 5 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $field 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $good_for_admissibility 2 0
+    type-con $state 0
+    bool
+fun-decl $good_for_post_admissibility 2 0
+    type-con $state 0
+    bool
+fun-decl $stuttering_pre 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $admissibility_pre 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $mutable_increases 3 1
+    type-con $state 0
+    type-con $state 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $meta_eq 3 1
+    type-con $state 0
+    type-con $state 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_stuttering_check 1 0
+    bool
+fun-decl $is_unwrap_check 1 0
+    bool
+fun-decl $is_admissibility_check 1 1
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $good_for_pre_can_unwrap 2 0
+    type-con $state 0
+    bool
+fun-decl $good_for_post_can_unwrap 2 0
+    type-con $state 0
+    bool
+fun-decl $unwrap_check_pre 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $update_int 4 0
+    type-con $state 0
+    type-con $ptr 0
+    int
+    type-con $state 0
+fun-decl $timestamp_is_now 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $now_writable 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $timestamp_post 3 1
+    type-con $state 0
+    type-con $state 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $timestamp_post_strict 3 1
+    type-con $state 0
+    type-con $state 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $pre_wrap 2 0
+    type-con $state 0
+    bool
+fun-decl $pre_unwrap 2 0
+    type-con $state 0
+    bool
+fun-decl $pre_static_wrap 2 0
+    type-con $state 0
+    bool
+fun-decl $pre_static_unwrap 2 0
+    type-con $state 0
+    bool
+fun-decl $unwrap_post 5 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $unwrap_post_claimable 5 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $keeps 4 2
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+  attribute expand 1
+    expr-attr
+      true
+fun-decl $expect_unreachable 1 0
+    bool
+fun-decl $taken_over 4 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $status 0
+fun-decl $take_over 4 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $state 0
+fun-decl $released 4 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $status 0
+fun-decl $release 5 0
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $state 0
+fun-decl $post_unwrap 3 0
+    type-con $state 0
+    type-con $state 0
+    bool
+fun-decl $new_ownees 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $get_memory_allocator 1 0
+    type-con $ptr 0
+fun-decl $memory_allocator_type 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl $memory_allocator_ref 1 0
+    int
+fun-decl $program_entry_point 2 0
+    type-con $state 0
+    bool
+fun-decl $program_entry_point_ch 2 0
+    type-con $state 0
+    bool
+fun-decl $is_global 3 1
+    type-con $ptr 0
+    type-con $ctype 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_global_array 4 1
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $active_option 3 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $field 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $ts_active_option 2 0
+    type-con $type_state 0
+    type-con $field 0
+fun-decl $union_active 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $field 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_union_field 3 0
+    type-con $ctype 0
+    type-con $field 0
+    bool
+fun-decl $union_havoced 4 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $full_extent 2 0
+    type-con $ptr 0
+    type-con $ptrset 0
+fun-decl $extent 3 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptrset 0
+fun-decl $span 2 0
+    type-con $ptr 0
+    type-con $ptrset 0
+fun-decl $in_span_of 3 1
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $first_option_typed 3 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+fun-decl $struct_extent 2 1
+    type-con $ptr 0
+    type-con $ptrset 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_struct_extent_of 3 1
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $volatile_span 3 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptrset 0
+fun-decl $left_split 3 0
+    type-con $ptr 0
+    int
+    type-con $ptr 0
+fun-decl $right_split 3 0
+    type-con $ptr 0
+    int
+    type-con $ptr 0
+fun-decl $joined_array 3 0
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $ptr 0
+fun-decl $mutable_root 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $set_in 3 0
+    type-con $ptr 0
+    type-con $ptrset 0
+    bool
+fun-decl $set_empty 1 0
+    type-con $ptrset 0
+fun-decl $set_singleton 2 0
+    type-con $ptr 0
+    type-con $ptrset 0
+fun-decl $non_null_set_singleton 2 0
+    type-con $ptr 0
+    type-con $ptrset 0
+fun-decl $set_union 3 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+fun-decl $set_difference 3 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+fun-decl $set_intersection 3 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+fun-decl $set_subset 3 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+    bool
+fun-decl $set_eq 3 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+    bool
+fun-decl $set_cardinality 2 0
+    type-con $ptrset 0
+    int
+fun-decl $set_universe 1 0
+    type-con $ptrset 0
+fun-decl $set_disjoint 3 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+    bool
+fun-decl $id_set_disjoint 4 0
+    type-con $ptr 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+    int
+fun-decl $set_in3 3 0
+    type-con $ptr 0
+    type-con $ptrset 0
+    bool
+fun-decl $set_in2 3 0
+    type-con $ptr 0
+    type-con $ptrset 0
+    bool
+fun-decl $in_some_owns 2 0
+    type-con $ptr 0
+    bool
+fun-decl $set_in0 3 0
+    type-con $ptr 0
+    type-con $ptrset 0
+    bool
+fun-decl sk_hack 2 0
+    bool
+    bool
+fun-decl $writes_nothing 3 1
+    type-con $state 0
+    type-con $state 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $array 3 0
+    type-con $ctype 0
+    int
+    type-con $ctype 0
+fun-decl $element_type 2 0
+    type-con $ctype 0
+    type-con $ctype 0
+fun-decl $array_length 2 0
+    type-con $ctype 0
+    int
+fun-decl $is_array_elt 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $inlined_array 3 1
+    type-con $ptr 0
+    type-con $ctype 0
+    type-con $ptr 0
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $idx 4 0
+    type-con $ptr 0
+    int
+    type-con $ctype 0
+    type-con $ptr 0
+fun-decl $add.mul 4 2
+    int
+    int
+    int
+    int
+  attribute inline 1
+    expr-attr
+      true
+  attribute expand 1
+    expr-attr
+      true
+fun-decl $add 3 2
+    int
+    int
+    int
+  attribute inline 1
+    expr-attr
+      true
+  attribute expand 1
+    expr-attr
+      true
+fun-decl $is_array_vol_or_nonvol 6 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    bool
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $is_array 5 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $is_thread_local_array 5 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_mutable_array 5 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_array_emb 6 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $is_array_emb_path 8 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    type-con $ptr 0
+    type-con $field 0
+    bool
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $array_field_properties 6 1
+    type-con $field 0
+    type-con $ctype 0
+    int
+    bool
+    bool
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $no_inline_array_field_properties 6 1
+    type-con $field 0
+    type-con $ctype 0
+    int
+    bool
+    bool
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $array_elt_emb 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $array_members 4 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    type-con $ptrset 0
+fun-decl $array_range 4 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    type-con $ptrset 0
+fun-decl $non_null_array_range 4 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    type-con $ptrset 0
+fun-decl $non_null_extent 3 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptrset 0
+fun-decl $as_array 4 1
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    type-con $ptr 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $array_eq 6 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $index_within 3 0
+    type-con $ptr 0
+    type-con $ptr 0
+    int
+fun-decl $in_array 5 1
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_array_full_extent_of 5 1
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_array_extent_of 6 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $ctype 0
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range 4 1
+    int
+    int
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $bool_to_int 2 1
+    bool
+    int
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $int_to_bool 2 1
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $read_bool 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $ite.int 4 3
+    bool
+    int
+    int
+    int
+  attribute external 1
+    string-attr ITE
+  attribute bvz 1
+    string-attr ITE
+  attribute bvint 1
+    string-attr ITE
+fun-decl $ite.bool 4 3
+    bool
+    bool
+    bool
+    bool
+  attribute external 1
+    string-attr ITE
+  attribute bvz 1
+    string-attr ITE
+  attribute bvint 1
+    string-attr ITE
+fun-decl $ite.ptr 4 3
+    bool
+    type-con $ptr 0
+    type-con $ptr 0
+    type-con $ptr 0
+  attribute external 1
+    string-attr ITE
+  attribute bvz 1
+    string-attr ITE
+  attribute bvint 1
+    string-attr ITE
+fun-decl $ite.struct 4 3
+    bool
+    type-con $struct 0
+    type-con $struct 0
+    type-con $struct 0
+  attribute external 1
+    string-attr ITE
+  attribute bvz 1
+    string-attr ITE
+  attribute bvint 1
+    string-attr ITE
+fun-decl $ite.ptrset 4 3
+    bool
+    type-con $ptrset 0
+    type-con $ptrset 0
+    type-con $ptrset 0
+  attribute external 1
+    string-attr ITE
+  attribute bvz 1
+    string-attr ITE
+  attribute bvint 1
+    string-attr ITE
+fun-decl $ite.primitive 4 3
+    bool
+    type-con $primitive 0
+    type-con $primitive 0
+    type-con $primitive 0
+  attribute external 1
+    string-attr ITE
+  attribute bvz 1
+    string-attr ITE
+  attribute bvint 1
+    string-attr ITE
+fun-decl $ite.record 4 3
+    bool
+    type-con $record 0
+    type-con $record 0
+    type-con $record 0
+  attribute external 1
+    string-attr ITE
+  attribute bvz 1
+    string-attr ITE
+  attribute bvint 1
+    string-attr ITE
+fun-decl $bool_id 2 1
+    bool
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $min.i1 1 0
+    int
+fun-decl $max.i1 1 0
+    int
+fun-decl $min.i2 1 0
+    int
+fun-decl $max.i2 1 0
+    int
+fun-decl $min.i4 1 0
+    int
+fun-decl $max.i4 1 0
+    int
+fun-decl $min.i8 1 0
+    int
+fun-decl $max.i8 1 0
+    int
+fun-decl $max.u1 1 0
+    int
+fun-decl $max.u2 1 0
+    int
+fun-decl $max.u4 1 0
+    int
+fun-decl $max.u8 1 0
+    int
+fun-decl $in_range_i1 2 1
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range_i2 2 1
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range_i4 2 1
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range_i8 2 1
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range_u1 2 1
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range_u2 2 1
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range_u4 2 1
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range_u8 2 1
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range_div_i1 3 1
+    int
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range_div_i2 3 1
+    int
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range_div_i4 3 1
+    int
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $in_range_div_i8 3 1
+    int
+    int
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $read_i1 3 1
+    type-con $state 0
+    type-con $ptr 0
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $read_i2 3 1
+    type-con $state 0
+    type-con $ptr 0
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $read_i4 3 1
+    type-con $state 0
+    type-con $ptr 0
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $read_i8 3 1
+    type-con $state 0
+    type-con $ptr 0
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $read_u1 3 1
+    type-con $state 0
+    type-con $ptr 0
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $read_u2 3 1
+    type-con $state 0
+    type-con $ptr 0
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $read_u4 3 1
+    type-con $state 0
+    type-con $ptr 0
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $read_u8 3 1
+    type-con $state 0
+    type-con $ptr 0
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $ptr_to_u8 2 0
+    type-con $ptr 0
+    int
+fun-decl $ptr_to_i8 2 0
+    type-con $ptr 0
+    int
+fun-decl $ptr_to_u4 2 0
+    type-con $ptr 0
+    int
+fun-decl $ptr_to_i4 2 0
+    type-con $ptr 0
+    int
+fun-decl $u8_to_ptr 2 1
+    int
+    type-con $ptr 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $i8_to_ptr 2 1
+    int
+    type-con $ptr 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $u4_to_ptr 2 1
+    int
+    type-con $ptr 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $i4_to_ptr 2 1
+    int
+    type-con $ptr 0
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $byte_ptr_subtraction 3 1
+    type-con $ptr 0
+    type-con $ptr 0
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $_pow2 2 0
+    int
+    int
+fun-decl $_or 4 0
+    type-con $ctype 0
+    int
+    int
+    int
+fun-decl $_xor 4 0
+    type-con $ctype 0
+    int
+    int
+    int
+fun-decl $_and 4 0
+    type-con $ctype 0
+    int
+    int
+    int
+fun-decl $_not 3 0
+    type-con $ctype 0
+    int
+    int
+fun-decl $unchk_add 4 1
+    type-con $ctype 0
+    int
+    int
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $unchk_sub 4 1
+    type-con $ctype 0
+    int
+    int
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $unchk_mul 4 1
+    type-con $ctype 0
+    int
+    int
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $unchk_div 4 1
+    type-con $ctype 0
+    int
+    int
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $unchk_mod 4 1
+    type-con $ctype 0
+    int
+    int
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $_shl 4 1
+    type-con $ctype 0
+    int
+    int
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $_shr 3 1
+    int
+    int
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $bv_extract_signed 5 0
+    int
+    int
+    int
+    int
+    int
+fun-decl $bv_extract_unsigned 5 0
+    int
+    int
+    int
+    int
+    int
+fun-decl $bv_update 6 0
+    int
+    int
+    int
+    int
+    int
+    int
+fun-decl $unchecked 3 0
+    type-con $ctype 0
+    int
+    int
+fun-decl $in_range_t 3 0
+    type-con $ctype 0
+    int
+    bool
+fun-decl $_mul 3 1
+    int
+    int
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $get_string_literal 3 0
+    int
+    int
+    type-con $ptr 0
+fun-decl $get_fnptr 3 0
+    int
+    type-con $ctype 0
+    type-con $ptr 0
+fun-decl $get_fnptr_ref 2 0
+    int
+    int
+fun-decl $get_fnptr_inv 2 0
+    int
+    int
+fun-decl $is_fnptr_type 2 0
+    type-con $ctype 0
+    bool
+fun-decl $is_math_type 2 0
+    type-con $ctype 0
+    bool
+fun-decl $claims_obj 3 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+fun-decl $valid_claim 3 0
+    type-con $state 0
+    type-con $ptr 0
+    bool
+fun-decl $claim_initial_assumptions 4 1
+    type-con $state 0
+    type-con $ptr 0
+    type-con $token 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $claim_transitivity_assumptions 5 1
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $token 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $valid_claim_impl 3 1
+    type-con $state 0
+    type-con $state 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $claims_claim 3 0
+    type-con $ptr 0
+    type-con $ptr 0
+    bool
+fun-decl $not_shared 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $claimed_closed 3 1
+    type-con $state 0
+    type-con $ptr 0
+    bool
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $no_claim 1 1
+    type-con $ptr 0
+  attribute unique 0
+fun-decl $ref_cnt 3 1
+    type-con $state 0
+    type-con $ptr 0
+    int
+  attribute weight 1
+    expr-attr
+      int-num 0
+fun-decl $is_claimable 2 0
+    type-con $ctype 0
+    bool
+fun-decl $is_thread_local_storage 2 0
+    type-con $ctype 0
+    bool
+fun-decl $frame_level 2 0
+    type-con $pure_function 0
+    int
+fun-decl $current_frame_level 1 0
+    int
+fun-decl $can_use_all_frame_axioms 2 1
+    type-con $state 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $can_use_frame_axiom_of 2 1
+    type-con $pure_function 0
+    bool
+  attribute inline 1
+    expr-attr
+      true
+fun-decl $reads_check_pre 2 0
+    type-con $state 0
+    bool
+fun-decl $reads_check_post 2 0
+    type-con $state 0
+    bool
+fun-decl $start_here 1 0
+    bool
+fun-decl $ptrset_to_int 2 0
+    type-con $ptrset 0
+    int
+fun-decl $int_to_ptrset 2 0
+    int
+    type-con $ptrset 0
+fun-decl $version_to_int 2 0
+    type-con $version 0
+    int
+fun-decl $int_to_version 2 0
+    int
+    type-con $version 0
+fun-decl $vol_version_to_int 2 0
+    type-con $vol_version 0
+    int
+fun-decl $int_to_vol_version 2 0
+    int
+    type-con $vol_version 0
+fun-decl $ptr_to_int 2 0
+    type-con $ptr 0
+    int
+fun-decl $int_to_ptr 2 0
+    int
+    type-con $ptr 0
+fun-decl $precise_test 2 0
+    type-con $ptr 0
+    bool
+fun-decl $updated_only_values 4 0
+    type-con $state 0
+    type-con $state 0
+    type-con $ptrset 0
+    bool
+fun-decl $updated_only_domains 4 0
+    type-con $state 0
+    type-con $state 0
+    type-con $ptrset 0
+    bool
+fun-decl $domain_updated_at 5 0
+    type-con $state 0
+    type-con $state 0
+    type-con $ptr 0
+    type-con $ptrset 0
+    bool
+fun-decl l#public 1 1
+    type-con $label 0
+  attribute unique 0
+fun-decl #tok$1^16.24 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #tok$1^24.47 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #tok$1^23.7 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #tok$1^16.3 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #loc.p 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #tok$1^16.8 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #loc.witness 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #tok$1^14.3 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #loc.max 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #tok$1^12.3 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #loc.len 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #distTp1 1 1
+    type-con $ctype 0
+  attribute unique 0
+fun-decl #loc.arr 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #tok$1^6.1 1 1
+    type-con $token 0
+  attribute unique 0
+fun-decl #file^Z?3A?5CC?5Cmax.c 1 1
+    type-con $token 0
+  attribute unique 0
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^^i1 0
+    int-num 1
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^^i2 0
+    int-num 2
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^^i4 0
+    int-num 4
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^^i8 0
+    int-num 8
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^^u1 0
+    int-num 1
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^^u2 0
+    int-num 2
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^^u4 0
+    int-num 4
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^^u8 0
+    int-num 8
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^^f4 0
+    int-num 4
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^^f8 0
+    int-num 8
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^$#thread_id_t 0
+    int-num 1
+axiom 0
+    =
+    fun $sizeof 1
+    fun ^$#ptrset 0
+    int-num 1
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^i1 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^i2 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^i4 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^i8 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^u1 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^u2 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^u4 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^u8 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^f4 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^f8 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^mathint 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^bool 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^void 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^claim 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^^root_emb 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^$#ptrset 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^$#thread_id_t 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^$#state_t 0
+    int-num 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun ^$#struct 0
+    int-num 0
+axiom 0
+    fun $is_composite 1
+    fun ^^claim 0
+axiom 0
+    fun $is_composite 1
+    fun ^^root_emb 0
+axiom 0
+    forall 1 1 3
+      var #n
+        type-con $ctype 0
+      pat 1
+        fun $ptr_to 1
+        var #n
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.145:15
+      attribute uniqueId 1
+        string-attr 4
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $unptr_to 1
+    fun $ptr_to 1
+    var #n
+      type-con $ctype 0
+    var #n
+      type-con $ctype 0
+axiom 0
+    forall 1 1 3
+      var #n
+        type-con $ctype 0
+      pat 1
+        fun $ptr_to 1
+        var #n
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.146:15
+      attribute uniqueId 1
+        string-attr 5
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $sizeof 1
+    fun $ptr_to 1
+    var #n
+      type-con $ctype 0
+    int-num 8
+axiom 0
+    forall 2 1 3
+      var #r
+        type-con $ctype 0
+      var #d
+        type-con $ctype 0
+      pat 1
+        fun $map_t 2
+        var #r
+          type-con $ctype 0
+        var #d
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.152:15
+      attribute uniqueId 1
+        string-attr 6
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $map_domain 1
+    fun $map_t 2
+    var #r
+      type-con $ctype 0
+    var #d
+      type-con $ctype 0
+    var #d
+      type-con $ctype 0
+axiom 0
+    forall 2 1 3
+      var #r
+        type-con $ctype 0
+      var #d
+        type-con $ctype 0
+      pat 1
+        fun $map_t 2
+        var #r
+          type-con $ctype 0
+        var #d
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.153:15
+      attribute uniqueId 1
+        string-attr 7
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $map_range 1
+    fun $map_t 2
+    var #r
+      type-con $ctype 0
+    var #d
+      type-con $ctype 0
+    var #r
+      type-con $ctype 0
+axiom 0
+    forall 1 1 3
+      var #n
+        type-con $ctype 0
+      pat 1
+        fun $ptr_to 1
+        var #n
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.158:15
+      attribute uniqueId 1
+        string-attr 8
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $ptr_level 1
+    fun $ptr_to 1
+    var #n
+      type-con $ctype 0
+    +
+    fun $ptr_level 1
+    var #n
+      type-con $ctype 0
+    int-num 17
+axiom 0
+    forall 2 1 3
+      var #r
+        type-con $ctype 0
+      var #d
+        type-con $ctype 0
+      pat 1
+        fun $map_t 2
+        var #r
+          type-con $ctype 0
+        var #d
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.159:15
+      attribute uniqueId 1
+        string-attr 9
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $ptr_level 1
+    fun $map_t 2
+    var #r
+      type-con $ctype 0
+    var #d
+      type-con $ctype 0
+    +
+    fun $ptr_level 1
+    var #r
+      type-con $ctype 0
+    int-num 23
+axiom 0
+    forall 1 1 4
+      var t
+        type-con $ctype 0
+      pat 1
+        fun $is_primitive 1
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.167:36
+      attribute uniqueId 1
+        string-attr 10
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $is_primitive 1
+    var t
+      type-con $ctype 0
+    =
+    fun $kind_of 1
+    var t
+      type-con $ctype 0
+    fun $kind_primitive 0
+axiom 0
+    forall 1 1 4
+      var t
+        type-con $ctype 0
+      pat 1
+        fun $is_composite 1
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.173:36
+      attribute uniqueId 1
+        string-attr 11
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $is_composite 1
+    var t
+      type-con $ctype 0
+    =
+    fun $kind_of 1
+    var t
+      type-con $ctype 0
+    fun $kind_composite 0
+axiom 0
+    forall 1 1 4
+      var t
+        type-con $ctype 0
+      pat 1
+        fun $is_arraytype 1
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.179:36
+      attribute uniqueId 1
+        string-attr 12
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $is_arraytype 1
+    var t
+      type-con $ctype 0
+    =
+    fun $kind_of 1
+    var t
+      type-con $ctype 0
+    fun $kind_array 0
+axiom 0
+    forall 1 1 4
+      var t
+        type-con $ctype 0
+      pat 1
+        fun $is_threadtype 1
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.185:37
+      attribute uniqueId 1
+        string-attr 13
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $is_threadtype 1
+    var t
+      type-con $ctype 0
+    =
+    fun $kind_of 1
+    var t
+      type-con $ctype 0
+    fun $kind_thread 0
+axiom 0
+    forall 1 1 4
+      var t
+        type-con $ctype 0
+      pat 1
+        fun $is_composite 1
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.198:15
+      attribute uniqueId 1
+        string-attr 14
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $is_composite 1
+    var t
+      type-con $ctype 0
+    fun $is_non_primitive 1
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 1 1 4
+      var t
+        type-con $ctype 0
+      pat 1
+        fun $is_arraytype 1
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.199:15
+      attribute uniqueId 1
+        string-attr 15
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $is_arraytype 1
+    var t
+      type-con $ctype 0
+    fun $is_non_primitive 1
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 1 1 4
+      var t
+        type-con $ctype 0
+      pat 1
+        fun $is_threadtype 1
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.200:15
+      attribute uniqueId 1
+        string-attr 16
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $is_threadtype 1
+    var t
+      type-con $ctype 0
+    fun $is_non_primitive 1
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 2 1 3
+      var #r
+        type-con $ctype 0
+      var #d
+        type-con $ctype 0
+      pat 1
+        fun $map_t 2
+        var #r
+          type-con $ctype 0
+        var #d
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.208:15
+      attribute uniqueId 1
+        string-attr 17
+      attribute bvZ3Native 1
+        string-attr False
+    fun $is_primitive 1
+    fun $map_t 2
+    var #r
+      type-con $ctype 0
+    var #d
+      type-con $ctype 0
+axiom 0
+    forall 1 1 3
+      var #n
+        type-con $ctype 0
+      pat 1
+        fun $ptr_to 1
+        var #n
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.209:15
+      attribute uniqueId 1
+        string-attr 18
+      attribute bvZ3Native 1
+        string-attr False
+    fun $is_primitive 1
+    fun $ptr_to 1
+    var #n
+      type-con $ctype 0
+axiom 0
+    forall 1 1 3
+      var #n
+        type-con $ctype 0
+      pat 1
+        fun $is_primitive 1
+        var #n
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.210:15
+      attribute uniqueId 1
+        string-attr 19
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $is_primitive 1
+    var #n
+      type-con $ctype 0
+    not
+    fun $is_claimable 1
+    var #n
+      type-con $ctype 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^void 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^bool 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^mathint 0
+axiom 0
+    fun $is_primitive 1
+    fun ^$#ptrset 0
+axiom 0
+    fun $is_primitive 1
+    fun ^$#state_t 0
+axiom 0
+    fun $is_threadtype 1
+    fun ^$#thread_id_t 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^i1 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^i2 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^i4 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^i8 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^u1 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^u2 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^u4 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^u8 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^f4 0
+axiom 0
+    fun $is_primitive 1
+    fun ^^f8 0
+axiom 0
+    =
+    fun $me 0
+    fun $ptr 2
+    fun ^$#thread_id_t 0
+    fun $me_ref 0
+axiom 0
+    forall 3 0 4
+      var M
+        type-con $memory_t 0
+      var p
+        type-con $ptr 0
+      var v
+        int
+      attribute qid 1
+        string-attr VccPrelu.238:15
+      attribute uniqueId 1
+        string-attr 20
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $select.mem 2
+    fun $store.mem 3
+    var M
+      type-con $memory_t 0
+    var p
+      type-con $ptr 0
+    var v
+      int
+    var p
+      type-con $ptr 0
+    var v
+      int
+axiom 0
+    forall 4 0 4
+      var M
+        type-con $memory_t 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      var v
+        int
+      attribute qid 1
+        string-attr VccPrelu.240:15
+      attribute uniqueId 1
+        string-attr 21
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    or 2
+    =
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+    =
+    fun $select.mem 2
+    fun $store.mem 3
+    var M
+      type-con $memory_t 0
+    var p
+      type-con $ptr 0
+    var v
+      int
+    var q
+      type-con $ptr 0
+    fun $select.mem 2
+    var M
+      type-con $memory_t 0
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 3 0 4
+      var M
+        type-con $typemap_t 0
+      var p
+        type-con $ptr 0
+      var v
+        type-con $type_state 0
+      attribute qid 1
+        string-attr VccPrelu.249:15
+      attribute uniqueId 1
+        string-attr 22
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $select.tm 2
+    fun $store.tm 3
+    var M
+      type-con $typemap_t 0
+    var p
+      type-con $ptr 0
+    var v
+      type-con $type_state 0
+    var p
+      type-con $ptr 0
+    var v
+      type-con $type_state 0
+axiom 0
+    forall 4 0 4
+      var M
+        type-con $typemap_t 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      var v
+        type-con $type_state 0
+      attribute qid 1
+        string-attr VccPrelu.251:15
+      attribute uniqueId 1
+        string-attr 23
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    or 2
+    =
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+    =
+    fun $select.tm 2
+    fun $store.tm 3
+    var M
+      type-con $typemap_t 0
+    var p
+      type-con $ptr 0
+    var v
+      type-con $type_state 0
+    var q
+      type-con $ptr 0
+    fun $select.tm 2
+    var M
+      type-con $typemap_t 0
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 3 0 4
+      var M
+        type-con $statusmap_t 0
+      var p
+        type-con $ptr 0
+      var v
+        type-con $status 0
+      attribute qid 1
+        string-attr VccPrelu.260:15
+      attribute uniqueId 1
+        string-attr 24
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $select.sm 2
+    fun $store.sm 3
+    var M
+      type-con $statusmap_t 0
+    var p
+      type-con $ptr 0
+    var v
+      type-con $status 0
+    var p
+      type-con $ptr 0
+    var v
+      type-con $status 0
+axiom 0
+    forall 4 0 4
+      var M
+        type-con $statusmap_t 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      var v
+        type-con $status 0
+      attribute qid 1
+        string-attr VccPrelu.262:15
+      attribute uniqueId 1
+        string-attr 25
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    or 2
+    =
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+    =
+    fun $select.sm 2
+    fun $store.sm 3
+    var M
+      type-con $statusmap_t 0
+    var p
+      type-con $ptr 0
+    var v
+      type-con $status 0
+    var q
+      type-con $ptr 0
+    fun $select.sm 2
+    var M
+      type-con $statusmap_t 0
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 3 1 3
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      var r
+        type-con $ptr 0
+      pat 2
+        fun $extent_hint 2
+        var p
+          type-con $ptr 0
+        var q
+          type-con $ptr 0
+        fun $extent_hint 2
+        var q
+          type-con $ptr 0
+        var r
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.288:15
+      attribute uniqueId 1
+        string-attr 26
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    fun $extent_hint 2
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+    fun $extent_hint 2
+    var q
+      type-con $ptr 0
+    var r
+      type-con $ptr 0
+    fun $extent_hint 2
+    var p
+      type-con $ptr 0
+    var r
+      type-con $ptr 0
+axiom 0
+    forall 1 1 3
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $typ 1
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.290:15
+      attribute uniqueId 1
+        string-attr 27
+      attribute bvZ3Native 1
+        string-attr False
+    fun $extent_hint 2
+    var p
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 4 1 3
+      var t
+        type-con $ctype 0
+      var s
+        type-con $ctype 0
+      var min
+        int
+      var max
+        int
+      pat 1
+        fun $is_nested_range 4
+        var t
+          type-con $ctype 0
+        var s
+          type-con $ctype 0
+        var min
+          int
+        var max
+          int
+      attribute qid 1
+        string-attr VccPrelu.297:27
+      attribute uniqueId 1
+        string-attr 28
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $is_nested_range 4
+    var t
+      type-con $ctype 0
+    var s
+      type-con $ctype 0
+    var min
+      int
+    var max
+      int
+    and 3
+    fun $is_nested 2
+    var t
+      type-con $ctype 0
+    var s
+      type-con $ctype 0
+    =
+    fun $nesting_min 2
+    var t
+      type-con $ctype 0
+    var s
+      type-con $ctype 0
+    var min
+      int
+    =
+    fun $nesting_max 2
+    var t
+      type-con $ctype 0
+    var s
+      type-con $ctype 0
+    var max
+      int
+axiom 0
+    forall 2 0 4
+      var #t
+        type-con $ctype 0
+      var #b
+        int
+      attribute qid 1
+        string-attr VccPrelu.334:15
+      attribute uniqueId 1
+        string-attr 29
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $typ 1
+    fun $ptr 2
+    var #t
+      type-con $ctype 0
+    var #b
+      int
+    var #t
+      type-con $ctype 0
+axiom 0
+    forall 2 0 4
+      var #t
+        type-con $ctype 0
+      var #b
+        int
+      attribute qid 1
+        string-attr VccPrelu.335:15
+      attribute uniqueId 1
+        string-attr 30
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $ref 1
+    fun $ptr 2
+    var #t
+      type-con $ctype 0
+    var #b
+      int
+    var #b
+      int
+axiom 0
+    forall 2 1 4
+      var p
+        type-con $ptr 0
+      var f
+        type-con $field 0
+      pat 1
+        fun $ghost_ref 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.344:15
+      attribute uniqueId 1
+        string-attr 31
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    and 2
+    =
+    fun $ghost_emb 1
+    fun $ghost_ref 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    var p
+      type-con $ptr 0
+    =
+    fun $ghost_path 1
+    fun $ghost_ref 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    var f
+      type-con $field 0
+axiom 0
+    forall 2 1 4
+      var fld
+        type-con $field 0
+      var off
+        int
+      pat 1
+        fun $array_path 2
+        var fld
+          type-con $field 0
+        var off
+          int
+      attribute qid 1
+        string-attr VccPrelu.355:15
+      attribute uniqueId 1
+        string-attr 32
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    and 3
+    not
+    fun $is_base_field 1
+    fun $array_path 2
+    var fld
+      type-con $field 0
+    var off
+      int
+    =
+    fun $array_path_1 1
+    fun $array_path 2
+    var fld
+      type-con $field 0
+    var off
+      int
+    var fld
+      type-con $field 0
+    =
+    fun $array_path_2 1
+    fun $array_path 2
+    var fld
+      type-con $field 0
+    var off
+      int
+    var off
+      int
+axiom 0
+    =
+    fun $null 0
+    fun $ptr 2
+    fun ^^void 0
+    int-num 0
+axiom 0
+    forall 2 0 4
+      var #p
+        type-con $ptr 0
+      var #t
+        type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.368:15
+      attribute uniqueId 1
+        string-attr 33
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $is 2
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+    =
+    fun $typ 1
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+axiom 0
+    forall 2 1 3
+      var #p
+        type-con $ptr 0
+      var #t
+        type-con $ctype 0
+      pat 1
+        fun $is 2
+        var #p
+          type-con $ptr 0
+        var #t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.370:15
+      attribute uniqueId 1
+        string-attr 34
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $is 2
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+    =
+    var #p
+      type-con $ptr 0
+    fun $ptr 2
+    var #t
+      type-con $ctype 0
+    fun $ref 1
+    var #p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 3
+      var r
+        int
+      var f
+        type-con $field 0
+      pat 1
+        fun $containing_struct 2
+        fun $dot 2
+        fun $ptr 2
+        fun $field_parent_type 1
+        var f
+          type-con $field 0
+        var r
+          int
+        var f
+          type-con $field 0
+        var f
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.388:15
+      attribute uniqueId 1
+        string-attr 35
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $containing_struct 2
+    fun $dot 2
+    fun $ptr 2
+    fun $field_parent_type 1
+    var f
+      type-con $field 0
+    var r
+      int
+    var f
+      type-con $field 0
+    var f
+      type-con $field 0
+    fun $ptr 2
+    fun $field_parent_type 1
+    var f
+      type-con $field 0
+    var r
+      int
+axiom 0
+    forall 2 1 3
+      var p
+        type-con $ptr 0
+      var f
+        type-con $field 0
+      pat 1
+        fun $containing_struct 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.392:15
+      attribute uniqueId 1
+        string-attr 36
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $containing_struct 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    fun $ptr 2
+    fun $field_parent_type 1
+    var f
+      type-con $field 0
+    fun $containing_struct_ref 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+axiom 0
+    forall 2 1 3
+      var p
+        type-con $ptr 0
+      var f
+        type-con $field 0
+      pat 1
+        fun $dot 2
+        fun $containing_struct 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+        var f
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.396:15
+      attribute uniqueId 1
+        string-attr 37
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    >=
+    fun $field_offset 1
+    var f
+      type-con $field 0
+    int-num 0
+    =
+    fun $ref 1
+    fun $dot 2
+    fun $containing_struct 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    var f
+      type-con $field 0
+    fun $ref 1
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 1 1 3
+      var ts
+        type-con $type_state 0
+      pat 1
+        fun $ts_emb 1
+        var ts
+          type-con $type_state 0
+      attribute qid 1
+        string-attr VccPrelu.427:15
+      attribute uniqueId 1
+        string-attr 38
+      attribute bvZ3Native 1
+        string-attr False
+    and 2
+    not
+    =
+    fun $kind_of 1
+    fun $typ 1
+    fun $ts_emb 1
+    var ts
+      type-con $type_state 0
+    fun $kind_primitive 0
+    fun $is_non_primitive 1
+    fun $typ 1
+    fun $ts_emb 1
+    var ts
+      type-con $type_state 0
+axiom 0
+    forall 2 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 2
+        fun $typed 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        fun $select.tm 2
+        fun $typemap 1
+        var S
+          type-con $state 0
+        fun $ts_emb 1
+        fun $select.tm 2
+        fun $typemap 1
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.430:15
+      attribute uniqueId 1
+        string-attr 39
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $typed 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $typed 2
+    var S
+      type-con $state 0
+    fun $ts_emb 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $ts_is_volatile 1
+        fun $select.tm 2
+        fun $typemap 1
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.440:15
+      attribute uniqueId 1
+        string-attr 40
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    fun $good_state 1
+    var S
+      type-con $state 0
+    fun $ts_is_volatile 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    =
+    fun $kind_of 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    fun $kind_primitive 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $select.sm 2
+        fun $statusmap 1
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.456:15
+      attribute uniqueId 1
+        string-attr 41
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    or 2
+    <=
+    fun $timestamp 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $current_timestamp 1
+    var S
+      type-con $state 0
+    not
+    fun $ts_typed 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    fun $good_state 1
+    fun $vs_state 1
+    fun $struct_zero 0
+axiom 0
+    forall 1 0 3
+      var s
+        type-con $struct 0
+      attribute qid 1
+        string-attr VccPrelu.486:15
+      attribute uniqueId 1
+        string-attr 42
+      attribute bvZ3Native 1
+        string-attr False
+    fun $good_state 1
+    fun $vs_state 1
+    var s
+      type-con $struct 0
+axiom 0
+    forall 2 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $vs_ctor 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.489:15
+      attribute uniqueId 1
+        string-attr 43
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $good_state 1
+    var S
+      type-con $state 0
+    and 2
+    =
+    fun $vs_base_ref 1
+    fun $vs_ctor 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $ref 1
+    var p
+      type-con $ptr 0
+    =
+    fun $vs_state 1
+    fun $vs_ctor 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var S
+      type-con $state 0
+axiom 0
+    forall 6 1 3
+      var r
+        type-con $record 0
+      var f
+        type-con $field 0
+      var val_bitsize
+        int
+      var from
+        int
+      var to
+        int
+      var repl
+        int
+      pat 1
+        fun $rec_update_bv 6
+        var r
+          type-con $record 0
+        var f
+          type-con $field 0
+        var val_bitsize
+          int
+        var from
+          int
+        var to
+          int
+        var repl
+          int
+      attribute qid 1
+        string-attr VccPrelu.502:25
+      attribute uniqueId 1
+        string-attr 44
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $rec_update_bv 6
+    var r
+      type-con $record 0
+    var f
+      type-con $field 0
+    var val_bitsize
+      int
+    var from
+      int
+    var to
+      int
+    var repl
+      int
+    fun $rec_update 3
+    var r
+      type-con $record 0
+    var f
+      type-con $field 0
+    fun $bv_update 5
+    fun $rec_fetch 2
+    var r
+      type-con $record 0
+    var f
+      type-con $field 0
+    var val_bitsize
+      int
+    var from
+      int
+    var to
+      int
+    var repl
+      int
+axiom 0
+    forall 1 0 3
+      var f
+        type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.505:15
+      attribute uniqueId 1
+        string-attr 45
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $rec_fetch 2
+    fun $rec_zero 0
+    var f
+      type-con $field 0
+    int-num 0
+axiom 0
+    forall 3 1 3
+      var r
+        type-con $record 0
+      var f
+        type-con $field 0
+      var v
+        int
+      pat 1
+        fun $rec_fetch 2
+        fun $rec_update 3
+        var r
+          type-con $record 0
+        var f
+          type-con $field 0
+        var v
+          int
+        var f
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.507:15
+      attribute uniqueId 1
+        string-attr 46
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $rec_fetch 2
+    fun $rec_update 3
+    var r
+      type-con $record 0
+    var f
+      type-con $field 0
+    var v
+      int
+    var f
+      type-con $field 0
+    var v
+      int
+axiom 0
+    forall 4 1 3
+      var r
+        type-con $record 0
+      var f1
+        type-con $field 0
+      var f2
+        type-con $field 0
+      var v
+        int
+      pat 1
+        fun $rec_fetch 2
+        fun $rec_update 3
+        var r
+          type-con $record 0
+        var f1
+          type-con $field 0
+        var v
+          int
+        var f2
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.510:15
+      attribute uniqueId 1
+        string-attr 47
+      attribute bvZ3Native 1
+        string-attr False
+    or 2
+    =
+    fun $rec_fetch 2
+    fun $rec_update 3
+    var r
+      type-con $record 0
+    var f1
+      type-con $field 0
+    var v
+      int
+    var f2
+      type-con $field 0
+    fun $rec_fetch 2
+    var r
+      type-con $record 0
+    var f2
+      type-con $field 0
+    =
+    var f1
+      type-con $field 0
+    var f2
+      type-con $field 0
+axiom 0
+    forall 1 1 3
+      var t
+        type-con $ctype 0
+      pat 1
+        fun $is_record_type 1
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.516:15
+      attribute uniqueId 1
+        string-attr 48
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $is_record_type 1
+    var t
+      type-con $ctype 0
+    fun $is_primitive 1
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 3 1 3
+      var p
+        type-con $ctype 0
+      var f
+        type-con $field 0
+      var ft
+        type-con $ctype 0
+      pat 2
+        fun $is_record_field 3
+        var p
+          type-con $ctype 0
+        var f
+          type-con $field 0
+        var ft
+          type-con $ctype 0
+        fun $is_record_type 1
+        var ft
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.519:15
+      attribute uniqueId 1
+        string-attr 49
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    fun $is_record_field 3
+    var p
+      type-con $ctype 0
+    var f
+      type-con $field 0
+    var ft
+      type-con $ctype 0
+    fun $is_record_type 1
+    var ft
+      type-con $ctype 0
+    =
+    fun $as_record_record_field 1
+    var f
+      type-con $field 0
+    var f
+      type-con $field 0
+axiom 0
+    forall 2 1 3
+      var r1
+        type-con $record 0
+      var r2
+        type-con $record 0
+      pat 1
+        fun $rec_eq 2
+        var r1
+          type-con $record 0
+        var r2
+          type-con $record 0
+      attribute qid 1
+        string-attr VccPrelu.522:18
+      attribute uniqueId 1
+        string-attr 50
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $rec_eq 2
+    var r1
+      type-con $record 0
+    var r2
+      type-con $record 0
+    =
+    var r1
+      type-con $record 0
+    var r2
+      type-con $record 0
+axiom 0
+    forall 2 1 3
+      var x
+        int
+      var y
+        int
+      pat 1
+        fun $rec_base_eq 2
+        var x
+          int
+        var y
+          int
+      attribute qid 1
+        string-attr VccPrelu.524:23
+      attribute uniqueId 1
+        string-attr 51
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $rec_base_eq 2
+    var x
+      int
+    var y
+      int
+    =
+    var x
+      int
+    var y
+      int
+axiom 0
+    forall 1 0 3
+      var r
+        type-con $record 0
+      attribute qid 1
+        string-attr VccPrelu.530:15
+      attribute uniqueId 1
+        string-attr 52
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $int_to_record 1
+    fun $record_to_int 1
+    var r
+      type-con $record 0
+    var r
+      type-con $record 0
+axiom 0
+    forall 2 1 3
+      var r1
+        type-con $record 0
+      var r2
+        type-con $record 0
+      pat 1
+        fun $rec_eq 2
+        var r1
+          type-con $record 0
+        var r2
+          type-con $record 0
+      attribute qid 1
+        string-attr VccPrelu.532:15
+      attribute uniqueId 1
+        string-attr 54
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    forall 1 0 3
+      var f
+        type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.534:11
+      attribute uniqueId 1
+        string-attr 53
+      attribute bvZ3Native 1
+        string-attr False
+    fun $rec_base_eq 2
+    fun $rec_fetch 2
+    var r1
+      type-con $record 0
+    var f
+      type-con $field 0
+    fun $rec_fetch 2
+    var r2
+      type-con $record 0
+    var f
+      type-con $field 0
+    fun $rec_eq 2
+    var r1
+      type-con $record 0
+    var r2
+      type-con $record 0
+axiom 0
+    forall 3 1 3
+      var r1
+        type-con $record 0
+      var r2
+        type-con $record 0
+      var f
+        type-con $field 0
+      pat 1
+        fun $rec_base_eq 2
+        fun $rec_fetch 2
+        var r1
+          type-con $record 0
+        var f
+          type-con $field 0
+        fun $rec_fetch 2
+        var r2
+          type-con $record 0
+        fun $as_record_record_field 1
+        var f
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.536:15
+      attribute uniqueId 1
+        string-attr 55
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $rec_eq 2
+    fun $int_to_record 1
+    fun $rec_fetch 2
+    var r1
+      type-con $record 0
+    var f
+      type-con $field 0
+    fun $int_to_record 1
+    fun $rec_fetch 2
+    var r2
+      type-con $record 0
+    var f
+      type-con $field 0
+    fun $rec_base_eq 2
+    fun $rec_fetch 2
+    var r1
+      type-con $record 0
+    var f
+      type-con $field 0
+    fun $rec_fetch 2
+    var r2
+      type-con $record 0
+    var f
+      type-con $field 0
+axiom 0
+    fun $has_volatile_owns_set 1
+    fun ^^claim 0
+axiom 0
+    forall 2 1 3
+      var #p
+        type-con $ptr 0
+      var t
+        type-con $ctype 0
+      pat 1
+        fun $dot 2
+        var #p
+          type-con $ptr 0
+        fun $owns_set_field 1
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.555:15
+      attribute uniqueId 1
+        string-attr 56
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $dot 2
+    var #p
+      type-con $ptr 0
+    fun $owns_set_field 1
+    var t
+      type-con $ctype 0
+    fun $ptr 2
+    fun ^$#ptrset 0
+    fun $ghost_ref 2
+    var #p
+      type-con $ptr 0
+    fun $owns_set_field 1
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 2
+        fun $is_primitive 1
+        fun $typ 1
+        var p
+          type-con $ptr 0
+        fun $owner 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.567:15
+      attribute uniqueId 1
+        string-attr 57
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $is_primitive 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    =
+    fun $owner 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $owner 2
+    var S
+      type-con $state 0
+    fun $ts_emb 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 2
+        fun $is_non_primitive 1
+        fun $typ 1
+        var p
+          type-con $ptr 0
+        fun $owner 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.569:15
+      attribute uniqueId 1
+        string-attr 58
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $is_non_primitive 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    =
+    fun $owner 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $st_owner 1
+    fun $select.sm 2
+    fun $statusmap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 2
+        fun $is_primitive 1
+        fun $typ 1
+        var p
+          type-con $ptr 0
+        fun $closed 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.572:15
+      attribute uniqueId 1
+        string-attr 59
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $is_primitive 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    =
+    fun $closed 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $st_closed 1
+    fun $select.sm 2
+    fun $statusmap 1
+    var S
+      type-con $state 0
+    fun $ts_emb 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 2
+        fun $is_non_primitive 1
+        fun $typ 1
+        var p
+          type-con $ptr 0
+        fun $closed 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.574:15
+      attribute uniqueId 1
+        string-attr 60
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $is_non_primitive 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    =
+    fun $closed 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $st_closed 1
+    fun $select.sm 2
+    fun $statusmap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 2
+        fun $is_primitive 1
+        fun $typ 1
+        var p
+          type-con $ptr 0
+        fun $timestamp 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.577:15
+      attribute uniqueId 1
+        string-attr 61
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $is_primitive 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    =
+    fun $timestamp 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $st_timestamp 1
+    fun $select.sm 2
+    fun $statusmap 1
+    var S
+      type-con $state 0
+    fun $ts_emb 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 2
+        fun $is_non_primitive 1
+        fun $typ 1
+        var p
+          type-con $ptr 0
+        fun $timestamp 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.579:15
+      attribute uniqueId 1
+        string-attr 62
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $is_non_primitive 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    =
+    fun $timestamp 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $st_timestamp 1
+    fun $select.sm 2
+    fun $statusmap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    fun $position_marker 0
+axiom 0
+    forall 1 1 3
+      var s
+        type-con $status 0
+      pat 1
+        fun $st_owner 1
+        var s
+          type-con $status 0
+      attribute qid 1
+        string-attr VccPrelu.585:15
+      attribute uniqueId 1
+        string-attr 63
+      attribute bvZ3Native 1
+        string-attr False
+    and 2
+    not
+    =
+    fun $kind_of 1
+    fun $typ 1
+    fun $st_owner 1
+    var s
+      type-con $status 0
+    fun $kind_primitive 0
+    fun $is_non_primitive 1
+    fun $typ 1
+    fun $st_owner 1
+    var s
+      type-con $status 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var #p
+        type-con $ptr 0
+      pat 1
+        fun $owns 2
+        var S
+          type-con $state 0
+        var #p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.593:28
+      attribute uniqueId 1
+        string-attr 64
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $owns 2
+    var S
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $int_to_ptrset 1
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    fun $dot 2
+    var #p
+      type-con $ptr 0
+    fun $owns_set_field 1
+    fun $typ 1
+    var #p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $mutable 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.608:31
+      attribute uniqueId 1
+        string-attr 65
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $mutable 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    and 3
+    fun $typed 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    =
+    fun $owner 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $me 0
+    not
+    fun $closed 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var #p
+        type-con $ptr 0
+      pat 1
+        fun $typed 2
+        var S
+          type-con $state 0
+        var #p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.619:11
+      attribute uniqueId 1
+        string-attr 66
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $good_state 1
+    var S
+      type-con $state 0
+    =
+    fun $typed 2
+    var S
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $ts_typed 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 3
+      var S
+        type-con $state 0
+      var #p
+        type-con $ptr 0
+      pat 1
+        fun $typed 2
+        var S
+          type-con $state 0
+        var #p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.621:11
+      attribute uniqueId 1
+        string-attr 67
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    fun $good_state 1
+    var S
+      type-con $state 0
+    fun $typed 2
+    var S
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    >
+    fun $ref 1
+    var #p
+      type-con $ptr 0
+    int-num 0
+axiom 0
+    forall 3 1 3
+      var S1
+        type-con $state 0
+      var S2
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 2
+        fun $select.sm 2
+        fun $statusmap 1
+        var S2
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        fun $call_transition 2
+        var S1
+          type-con $state 0
+        var S2
+          type-con $state 0
+      attribute qid 1
+        string-attr VccPrelu.685:15
+      attribute uniqueId 1
+        string-attr 68
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $call_transition 2
+    var S1
+      type-con $state 0
+    var S2
+      type-con $state 0
+    fun $instantiate_st 1
+    fun $select.sm 2
+    fun $statusmap 1
+    var S1
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $is_domain_root 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.711:26
+      attribute uniqueId 1
+        string-attr 69
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $is_domain_root 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    true
+axiom 0
+    forall 2 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $in_wrapped_domain 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.714:29
+      attribute uniqueId 1
+        string-attr 71
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $in_wrapped_domain 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    exists 1 1 3
+      var q
+        type-con $ptr 0
+      pat 1
+        fun $set_in2 2
+        var p
+          type-con $ptr 0
+        fun $ver_domain 1
+        fun $read_version 2
+        var S
+          type-con $state 0
+        var q
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.715:13
+      attribute uniqueId 1
+        string-attr 70
+      attribute bvZ3Native 1
+        string-attr False
+    and 8
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $ver_domain 1
+    fun $read_version 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    fun $closed 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    =
+    fun $owner 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    fun $me 0
+    fun $is 2
+    var q
+      type-con $ptr 0
+    fun $typ 1
+    var q
+      type-con $ptr 0
+    fun $typed 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    not
+    =
+    fun $kind_of 1
+    fun $typ 1
+    var q
+      type-con $ptr 0
+    fun $kind_primitive 0
+    fun $is_non_primitive 1
+    fun $typ 1
+    var q
+      type-con $ptr 0
+    fun $is_domain_root 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 2 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $thread_local 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.728:24
+      attribute uniqueId 1
+        string-attr 72
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $thread_local 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    and 2
+    fun $typed 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    or 2
+    and 4
+    =
+    fun $kind_of 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    fun $kind_primitive 0
+    or 2
+    not
+    fun $ts_is_volatile 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    not
+    fun $closed 2
+    var S
+      type-con $state 0
+    fun $ts_emb 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    not
+    =
+    fun $kind_of 1
+    fun $typ 1
+    fun $ts_emb 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $kind_primitive 0
+    or 2
+    =
+    fun $owner 2
+    var S
+      type-con $state 0
+    fun $ts_emb 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $me 0
+    fun $in_wrapped_domain 2
+    var S
+      type-con $state 0
+    fun $ts_emb 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    and 2
+    not
+    =
+    fun $kind_of 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    fun $kind_primitive 0
+    or 2
+    =
+    fun $owner 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $me 0
+    fun $in_wrapped_domain 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 3 1 3
+      var #s1
+        type-con $state 0
+      var #p
+        type-con $ptr 0
+      var typ
+        type-con $ctype 0
+      pat 1
+        fun $inv2 4
+        var #s1
+          type-con $state 0
+        var #s1
+          type-con $state 0
+        var #p
+          type-con $ptr 0
+        var typ
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.766:15
+      attribute uniqueId 1
+        string-attr 73
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $imply_inv 3
+    var #s1
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    var typ
+      type-con $ctype 0
+    fun $inv2 4
+    var #s1
+      type-con $state 0
+    var #s1
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    var typ
+      type-con $ctype 0
+axiom 0
+    forall 4 1 4
+      var #s1
+        type-con $state 0
+      var #s2
+        type-con $state 0
+      var #p
+        type-con $ptr 0
+      var #t
+        type-con $ctype 0
+      pat 1
+        fun $sequential 4
+        var #s1
+          type-con $state 0
+        var #s2
+          type-con $state 0
+        var #p
+          type-con $ptr 0
+        var #t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.778:34
+      attribute uniqueId 1
+        string-attr 74
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $sequential 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+    implies
+    and 2
+    fun $closed 2
+    var #s1
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $closed 2
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $spans_the_same 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+axiom 0
+    forall 4 1 4
+      var #s1
+        type-con $state 0
+      var #s2
+        type-con $state 0
+      var #dependant
+        type-con $ptr 0
+      var #this
+        type-con $ptr 0
+      pat 1
+        fun $depends 4
+        var #s1
+          type-con $state 0
+        var #s2
+          type-con $state 0
+        var #dependant
+          type-con $ptr 0
+        var #this
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.781:31
+      attribute uniqueId 1
+        string-attr 75
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $depends 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #dependant
+      type-con $ptr 0
+    var #this
+      type-con $ptr 0
+    or 4
+    fun $spans_the_same 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #this
+      type-con $ptr 0
+    fun $typ 1
+    var #this
+      type-con $ptr 0
+    and 2
+    not
+    fun $closed 2
+    var #s1
+      type-con $state 0
+    var #dependant
+      type-con $ptr 0
+    not
+    fun $closed 2
+    var #s2
+      type-con $state 0
+    var #dependant
+      type-con $ptr 0
+    and 2
+    fun $inv2 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #dependant
+      type-con $ptr 0
+    fun $typ 1
+    var #dependant
+      type-con $ptr 0
+    fun $nonvolatile_spans_the_same 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #dependant
+      type-con $ptr 0
+    fun $typ 1
+    var #dependant
+      type-con $ptr 0
+    fun $is_threadtype 1
+    fun $typ 1
+    var #dependant
+      type-con $ptr 0
+axiom 0
+    forall 4 1 4
+      var #s1
+        type-con $state 0
+      var #s2
+        type-con $state 0
+      var #p
+        type-con $ptr 0
+      var #t
+        type-con $ctype 0
+      pat 1
+        fun $spans_the_same 4
+        var #s1
+          type-con $state 0
+        var #s2
+          type-con $state 0
+        var #p
+          type-con $ptr 0
+        var #t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.786:38
+      attribute uniqueId 1
+        string-attr 76
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $spans_the_same 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+    and 4
+    =
+    fun $read_version 2
+    var #s1
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $read_version 2
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    =
+    fun $owns 2
+    var #s1
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $owns 2
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    =
+    fun $select.tm 2
+    fun $typemap 1
+    var #s1
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $select.tm 2
+    fun $typemap 1
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $state_spans_the_same 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+axiom 0
+    forall 4 1 4
+      var #s1
+        type-con $state 0
+      var #s2
+        type-con $state 0
+      var #p
+        type-con $ptr 0
+      var #t
+        type-con $ctype 0
+      pat 1
+        fun $nonvolatile_spans_the_same 4
+        var #s1
+          type-con $state 0
+        var #s2
+          type-con $state 0
+        var #p
+          type-con $ptr 0
+        var #t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.795:50
+      attribute uniqueId 1
+        string-attr 77
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $nonvolatile_spans_the_same 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+    and 3
+    =
+    fun $read_version 2
+    var #s1
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $read_version 2
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    =
+    fun $select.tm 2
+    fun $typemap 1
+    var #s1
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $select.tm 2
+    fun $typemap 1
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $state_nonvolatile_spans_the_same 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+axiom 0
+    forall 1 1 3
+      var T
+        type-con $ctype 0
+      pat 1
+        fun $is_primitive 1
+        var T
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.813:15
+      attribute uniqueId 1
+        string-attr 79
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $is_primitive 1
+    var T
+      type-con $ctype 0
+    forall 2 1 3
+      var r
+        int
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $full_extent 1
+        fun $ptr 2
+        var T
+          type-con $ctype 0
+        var r
+          int
+      attribute qid 1
+        string-attr VccPrelu.815:13
+      attribute uniqueId 1
+        string-attr 78
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $full_extent 1
+    fun $ptr 2
+    var T
+      type-con $ctype 0
+    var r
+      int
+    =
+    var p
+      type-con $ptr 0
+    fun $ptr 2
+    var T
+      type-con $ctype 0
+    var r
+      int
+axiom 0
+    forall 1 1 3
+      var T
+        type-con $ctype 0
+      pat 1
+        fun $is_primitive 1
+        var T
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.818:15
+      attribute uniqueId 1
+        string-attr 81
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $is_primitive 1
+    var T
+      type-con $ctype 0
+    forall 3 1 3
+      var S
+        type-con $state 0
+      var r
+        int
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $extent 2
+        var S
+          type-con $state 0
+        fun $ptr 2
+        var T
+          type-con $ctype 0
+        var r
+          int
+      attribute qid 1
+        string-attr VccPrelu.820:13
+      attribute uniqueId 1
+        string-attr 80
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $extent 2
+    var S
+      type-con $state 0
+    fun $ptr 2
+    var T
+      type-con $ctype 0
+    var r
+      int
+    =
+    var p
+      type-con $ptr 0
+    fun $ptr 2
+    var T
+      type-con $ctype 0
+    var r
+      int
+axiom 0
+    forall 1 1 3
+      var S
+        type-con $state 0
+      pat 1
+        fun $function_entry 1
+        var S
+          type-con $state 0
+      attribute qid 1
+        string-attr VccPrelu.835:15
+      attribute uniqueId 1
+        string-attr 83
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $function_entry 1
+    var S
+      type-con $state 0
+    and 2
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    >=
+    fun $current_timestamp 1
+    var S
+      type-con $state 0
+    int-num 0
+axiom 0
+    forall 1 1 3
+      var S
+        type-con $state 0
+      pat 1
+        fun $full_stop 1
+        var S
+          type-con $state 0
+      attribute qid 1
+        string-attr VccPrelu.838:15
+      attribute uniqueId 1
+        string-attr 84
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    and 2
+    fun $good_state 1
+    var S
+      type-con $state 0
+    fun $invok_state 1
+    var S
+      type-con $state 0
+axiom 0
+    forall 1 1 3
+      var S
+        type-con $state 0
+      pat 1
+        fun $invok_state 1
+        var S
+          type-con $state 0
+      attribute qid 1
+        string-attr VccPrelu.841:15
+      attribute uniqueId 1
+        string-attr 85
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $invok_state 1
+    var S
+      type-con $state 0
+    fun $good_state 1
+    var S
+      type-con $state 0
+axiom 0
+    forall 2 1 3
+      var id
+        type-con $token 0
+      var S
+        type-con $state 0
+      pat 1
+        fun $good_state_ext 2
+        var id
+          type-con $token 0
+        var S
+          type-con $state 0
+      attribute qid 1
+        string-attr VccPrelu.860:15
+      attribute uniqueId 1
+        string-attr 87
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $good_state_ext 2
+    var id
+      type-con $token 0
+    var S
+      type-con $state 0
+    fun $good_state 1
+    var S
+      type-con $state 0
+axiom 0
+    forall 3 1 3
+      var S
+        type-con $state 0
+      var r
+        int
+      var t
+        type-con $ctype 0
+      pat 1
+        fun $ptr 2
+        var t
+          type-con $ctype 0
+        fun $select.mem 2
+        fun $memory 1
+        var S
+          type-con $state 0
+        fun $ptr 2
+        fun $ptr_to 1
+        var t
+          type-con $ctype 0
+        var r
+          int
+      attribute qid 1
+        string-attr VccPrelu.872:15
+      attribute uniqueId 1
+        string-attr 88
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    fun $ptr 2
+    fun $ptr_to 1
+    var t
+      type-con $ctype 0
+    var r
+      int
+    fun $read_ptr_m 3
+    var S
+      type-con $state 0
+    fun $ptr 2
+    fun $ptr_to 1
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $read_version 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.886:36
+      attribute uniqueId 1
+        string-attr 89
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $read_version 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $int_to_version 1
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $domain 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.889:30
+      attribute uniqueId 1
+        string-attr 90
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $domain 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $ver_domain 1
+    fun $read_version 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 4 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      var l
+        type-con $label 0
+      pat 1
+        fun $in_domain_lab 4
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        var q
+          type-con $ptr 0
+        var l
+          type-con $label 0
+      attribute qid 1
+        string-attr VccPrelu.899:15
+      attribute uniqueId 1
+        string-attr 91
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $in_domain_lab 4
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+    var l
+      type-con $label 0
+    fun $inv_lab 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var l
+      type-con $label 0
+axiom 0
+    forall 4 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      var l
+        type-con $label 0
+      pat 1
+        fun $in_domain_lab 4
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        var q
+          type-con $ptr 0
+        var l
+          type-con $label 0
+      attribute qid 1
+        string-attr VccPrelu.902:15
+      attribute uniqueId 1
+        string-attr 92
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $in_domain_lab 4
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+    var l
+      type-con $label 0
+    fun $in_domain 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 4 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      var l
+        type-con $label 0
+      pat 1
+        fun $in_vdomain_lab 4
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        var q
+          type-con $ptr 0
+        var l
+          type-con $label 0
+      attribute qid 1
+        string-attr VccPrelu.905:15
+      attribute uniqueId 1
+        string-attr 93
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $in_vdomain_lab 4
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+    var l
+      type-con $label 0
+    fun $inv_lab 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var l
+      type-con $label 0
+axiom 0
+    forall 4 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      var l
+        type-con $label 0
+      pat 1
+        fun $in_vdomain_lab 4
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        var q
+          type-con $ptr 0
+        var l
+          type-con $label 0
+      attribute qid 1
+        string-attr VccPrelu.908:15
+      attribute uniqueId 1
+        string-attr 94
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $in_vdomain_lab 4
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+    var l
+      type-con $label 0
+    fun $in_vdomain 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 3 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      pat 1
+        fun $in_domain 3
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        var q
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.914:15
+      attribute uniqueId 1
+        string-attr 96
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $in_domain 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+    and 3
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $domain 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    fun $closed 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    forall 1 1 3
+      var r
+        type-con $ptr 0
+      pat 1
+        fun $set_in 2
+        var r
+          type-con $ptr 0
+        fun $owns 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.918:16
+      attribute uniqueId 1
+        string-attr 95
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    not
+    fun $has_volatile_owns_set 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    fun $set_in 2
+    var r
+      type-con $ptr 0
+    fun $owns 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $set_in2 2
+    var r
+      type-con $ptr 0
+    fun $ver_domain 1
+    fun $read_version 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 2 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $in_domain 3
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.923:15
+      attribute uniqueId 1
+        string-attr 97
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 7
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    fun $closed 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    =
+    fun $owner 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $me 0
+    fun $is 2
+    var p
+      type-con $ptr 0
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    fun $typed 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    not
+    =
+    fun $kind_of 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    fun $kind_primitive 0
+    fun $is_non_primitive 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    fun $in_domain 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 3 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      pat 1
+        fun $in_domain 3
+        var S
+          type-con $state 0
+        var q
+          type-con $ptr 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.932:15
+      attribute uniqueId 1
+        string-attr 98
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    and 2
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    fun $set_in 2
+    var q
+      type-con $ptr 0
+    fun $domain 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $in_domain 3
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 4 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      var r
+        type-con $ptr 0
+      pat 2
+        fun $set_in 2
+        var q
+          type-con $ptr 0
+        fun $domain 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        fun $in_domain 3
+        var S
+          type-con $state 0
+        var r
+          type-con $ptr 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.936:15
+      attribute uniqueId 1
+        string-attr 99
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    and 3
+    not
+    fun $has_volatile_owns_set 1
+    fun $typ 1
+    var q
+      type-con $ptr 0
+    fun $set_in 2
+    var q
+      type-con $ptr 0
+    fun $domain 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $set_in0 2
+    var r
+      type-con $ptr 0
+    fun $owns 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    and 2
+    fun $in_domain 3
+    var S
+      type-con $state 0
+    var r
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    fun $set_in0 2
+    var r
+      type-con $ptr 0
+    fun $owns 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 4 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      var r
+        type-con $ptr 0
+      pat 2
+        fun $set_in 2
+        var q
+          type-con $ptr 0
+        fun $domain 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        fun $in_vdomain 3
+        var S
+          type-con $state 0
+        var r
+          type-con $ptr 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.941:15
+      attribute uniqueId 1
+        string-attr 101
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    and 3
+    fun $has_volatile_owns_set 1
+    fun $typ 1
+    var q
+      type-con $ptr 0
+    fun $set_in 2
+    var q
+      type-con $ptr 0
+    fun $domain 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    forall 1 0 3
+      var S1
+        type-con $state 0
+      attribute qid 1
+        string-attr VccPrelu.945:11
+      attribute uniqueId 1
+        string-attr 100
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 3
+    fun $inv2 4
+    var S1
+      type-con $state 0
+    var S1
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    fun $typ 1
+    var q
+      type-con $ptr 0
+    =
+    fun $read_version 2
+    var S1
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $read_version 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    =
+    fun $domain 2
+    var S1
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $domain 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $set_in0 2
+    var r
+      type-con $ptr 0
+    fun $owns 2
+    var S1
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    and 2
+    fun $in_vdomain 3
+    var S
+      type-con $state 0
+    var r
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    fun $set_in0 2
+    var r
+      type-con $ptr 0
+    fun $owns 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 3 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      pat 1
+        fun $in_vdomain 3
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        var q
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.952:15
+      attribute uniqueId 1
+        string-attr 102
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    implies
+    fun $in_vdomain 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+    fun $in_domain 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 4 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var d
+        type-con $ptr 0
+      var f
+        type-con $field 0
+      pat 3
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $domain 2
+        var S
+          type-con $state 0
+        var d
+          type-con $ptr 0
+        fun $is_primitive_non_volatile_field 1
+        var f
+          type-con $field 0
+        fun $select.mem 2
+        fun $memory 1
+        var S
+          type-con $state 0
+        fun $dot 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.957:15
+      attribute uniqueId 1
+        string-attr 103
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $domain 2
+    var S
+      type-con $state 0
+    var d
+      type-con $ptr 0
+    fun $is_primitive_non_volatile_field 1
+    var f
+      type-con $field 0
+    =
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    fun $fetch_from_domain 2
+    fun $read_version 2
+    var S
+      type-con $state 0
+    var d
+      type-con $ptr 0
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+axiom 0
+    forall 3 2 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var d
+        type-con $ptr 0
+      pat 3
+        fun $full_stop 1
+        var S
+          type-con $state 0
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $domain 2
+        var S
+          type-con $state 0
+        var d
+          type-con $ptr 0
+        fun $select.sm 2
+        fun $statusmap 1
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      pat 3
+        fun $full_stop 1
+        var S
+          type-con $state 0
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $domain 2
+        var S
+          type-con $state 0
+        var d
+          type-con $ptr 0
+        fun $select.tm 2
+        fun $typemap 1
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.962:15
+      attribute uniqueId 1
+        string-attr 104
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $domain 2
+    var S
+      type-con $state 0
+    var d
+      type-con $ptr 0
+    and 2
+    fun $typed 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    not
+    fun $ts_is_volatile 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 4 2 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var d
+        type-con $ptr 0
+      var f
+        type-con $field 0
+      pat 3
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $domain 2
+        var S
+          type-con $state 0
+        var d
+          type-con $ptr 0
+        fun $is_primitive_non_volatile_field 1
+        var f
+          type-con $field 0
+        fun $owner 2
+        var S
+          type-con $state 0
+        fun $dot 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+      pat 3
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $domain 2
+        var S
+          type-con $state 0
+        var d
+          type-con $ptr 0
+        fun $is_primitive_non_volatile_field 1
+        var f
+          type-con $field 0
+        fun $select.tm 2
+        fun $typemap 1
+        var S
+          type-con $state 0
+        fun $dot 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.968:15
+      attribute uniqueId 1
+        string-attr 105
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 3
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $domain 2
+    var S
+      type-con $state 0
+    var d
+      type-con $ptr 0
+    fun $is_primitive_non_volatile_field 1
+    var f
+      type-con $field 0
+    and 2
+    fun $typed 2
+    var S
+      type-con $state 0
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    not
+    fun $ts_is_volatile 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+axiom 0
+    forall 7 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var d
+        type-con $ptr 0
+      var f
+        type-con $field 0
+      var sz
+        int
+      var i
+        int
+      var t
+        type-con $ctype 0
+      pat 3
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $domain 2
+        var S
+          type-con $state 0
+        var d
+          type-con $ptr 0
+        fun $is_primitive_embedded_array 2
+        var f
+          type-con $field 0
+        var sz
+          int
+        fun $select.mem 2
+        fun $memory 1
+        var S
+          type-con $state 0
+        fun $idx 3
+        fun $dot 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+        var i
+          int
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.974:15
+      attribute uniqueId 1
+        string-attr 106
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 5
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $domain 2
+    var S
+      type-con $state 0
+    var d
+      type-con $ptr 0
+    fun $is_primitive_embedded_array 2
+    var f
+      type-con $field 0
+    var sz
+      int
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var sz
+      int
+    =
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    fun $idx 3
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    var i
+      int
+    var t
+      type-con $ctype 0
+    fun $fetch_from_domain 2
+    fun $read_version 2
+    var S
+      type-con $state 0
+    var d
+      type-con $ptr 0
+    fun $idx 3
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    var i
+      int
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 7 2 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var d
+        type-con $ptr 0
+      var f
+        type-con $field 0
+      var sz
+        int
+      var i
+        int
+      var t
+        type-con $ctype 0
+      pat 3
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $domain 2
+        var S
+          type-con $state 0
+        var d
+          type-con $ptr 0
+        fun $is_primitive_embedded_array 2
+        var f
+          type-con $field 0
+        var sz
+          int
+        fun $select.tm 2
+        fun $typemap 1
+        var S
+          type-con $state 0
+        fun $idx 3
+        fun $dot 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+        var i
+          int
+        var t
+          type-con $ctype 0
+      pat 3
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $domain 2
+        var S
+          type-con $state 0
+        var d
+          type-con $ptr 0
+        fun $is_primitive_embedded_array 2
+        var f
+          type-con $field 0
+        var sz
+          int
+        fun $owner 2
+        var S
+          type-con $state 0
+        fun $idx 3
+        fun $dot 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+        var i
+          int
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.979:15
+      attribute uniqueId 1
+        string-attr 107
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 5
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $domain 2
+    var S
+      type-con $state 0
+    var d
+      type-con $ptr 0
+    fun $is_primitive_embedded_array 2
+    var f
+      type-con $field 0
+    var sz
+      int
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var sz
+      int
+    and 2
+    fun $typed 2
+    var S
+      type-con $state 0
+    fun $idx 3
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    var i
+      int
+    var t
+      type-con $ctype 0
+    not
+    fun $ts_is_volatile 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    fun $idx 3
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    var i
+      int
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 6 2 3
+      var S
+        type-con $state 0
+      var r
+        int
+      var d
+        type-con $ptr 0
+      var sz
+        int
+      var i
+        int
+      var t
+        type-con $ctype 0
+      pat 3
+        fun $set_in 2
+        fun $ptr 2
+        fun $array 2
+        var t
+          type-con $ctype 0
+        var sz
+          int
+        var r
+          int
+        fun $domain 2
+        var S
+          type-con $state 0
+        var d
+          type-con $ptr 0
+        fun $select.tm 2
+        fun $typemap 1
+        var S
+          type-con $state 0
+        fun $idx 3
+        fun $ptr 2
+        var t
+          type-con $ctype 0
+        var r
+          int
+        var i
+          int
+        var t
+          type-con $ctype 0
+        fun $is_primitive 1
+        var t
+          type-con $ctype 0
+      pat 3
+        fun $set_in 2
+        fun $ptr 2
+        fun $array 2
+        var t
+          type-con $ctype 0
+        var sz
+          int
+        var r
+          int
+        fun $domain 2
+        var S
+          type-con $state 0
+        var d
+          type-con $ptr 0
+        fun $owner 2
+        var S
+          type-con $state 0
+        fun $idx 3
+        fun $ptr 2
+        var t
+          type-con $ctype 0
+        var r
+          int
+        var i
+          int
+        var t
+          type-con $ctype 0
+        fun $is_primitive 1
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.985:15
+      attribute uniqueId 1
+        string-attr 108
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 5
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    fun $is_primitive 1
+    var t
+      type-con $ctype 0
+    fun $set_in 2
+    fun $ptr 2
+    fun $array 2
+    var t
+      type-con $ctype 0
+    var sz
+      int
+    var r
+      int
+    fun $domain 2
+    var S
+      type-con $state 0
+    var d
+      type-con $ptr 0
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var sz
+      int
+    and 2
+    fun $typed 2
+    var S
+      type-con $state 0
+    fun $idx 3
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var i
+      int
+    var t
+      type-con $ctype 0
+    not
+    fun $ts_is_volatile 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    fun $idx 3
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var i
+      int
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 6 1 3
+      var S
+        type-con $state 0
+      var r
+        int
+      var d
+        type-con $ptr 0
+      var sz
+        int
+      var i
+        int
+      var t
+        type-con $ctype 0
+      pat 3
+        fun $set_in 2
+        fun $ptr 2
+        fun $array 2
+        var t
+          type-con $ctype 0
+        var sz
+          int
+        var r
+          int
+        fun $domain 2
+        var S
+          type-con $state 0
+        var d
+          type-con $ptr 0
+        fun $select.mem 2
+        fun $memory 1
+        var S
+          type-con $state 0
+        fun $idx 3
+        fun $ptr 2
+        var t
+          type-con $ctype 0
+        var r
+          int
+        var i
+          int
+        var t
+          type-con $ctype 0
+        fun $is_primitive 1
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.994:15
+      attribute uniqueId 1
+        string-attr 109
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 5
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    fun $is_primitive 1
+    var t
+      type-con $ctype 0
+    fun $set_in 2
+    fun $ptr 2
+    fun $array 2
+    var t
+      type-con $ctype 0
+    var sz
+      int
+    var r
+      int
+    fun $domain 2
+    var S
+      type-con $state 0
+    var d
+      type-con $ptr 0
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var sz
+      int
+    =
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    fun $idx 3
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var i
+      int
+    var t
+      type-con $ctype 0
+    fun $fetch_from_domain 2
+    fun $read_version 2
+    var S
+      type-con $state 0
+    var d
+      type-con $ptr 0
+    fun $idx 3
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var i
+      int
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 6 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var f
+        type-con $field 0
+      var sz
+        int
+      var i
+        int
+      var t
+        type-con $ctype 0
+      pat 2
+        fun $is_primitive_embedded_volatile_array 3
+        var f
+          type-con $field 0
+        var sz
+          int
+        var t
+          type-con $ctype 0
+        fun $ts_is_volatile 1
+        fun $select.tm 2
+        fun $typemap 1
+        var S
+          type-con $state 0
+        fun $idx 3
+        fun $dot 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+        var i
+          int
+        var t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.1002:15
+      attribute uniqueId 1
+        string-attr 110
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 4
+    fun $good_state 1
+    var S
+      type-con $state 0
+    fun $is_primitive_embedded_volatile_array 3
+    var f
+      type-con $field 0
+    var sz
+      int
+    var t
+      type-con $ctype 0
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var sz
+      int
+    fun $ts_is_volatile 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    fun $idx 3
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    var i
+      int
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 4 1 4
+      var p
+        type-con $ptr 0
+      var S1
+        type-con $state 0
+      var S2
+        type-con $state 0
+      var q
+        type-con $ptr 0
+      pat 2
+        fun $set_in 2
+        var q
+          type-con $ptr 0
+        fun $domain 2
+        var S1
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        fun $call_transition 2
+        var S1
+          type-con $state 0
+        var S2
+          type-con $state 0
+      attribute qid 1
+        string-attr VccPrelu.1013:15
+      attribute uniqueId 1
+        string-attr 111
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    fun $instantiate_bool 1
+    fun $set_in 2
+    var q
+      type-con $ptr 0
+    fun $domain 2
+    var S2
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 4 1 4
+      var p
+        type-con $ptr 0
+      var S1
+        type-con $state 0
+      var S2
+        type-con $state 0
+      var q
+        type-con $ptr 0
+      pat 2
+        fun $set_in 2
+        var q
+          type-con $ptr 0
+        fun $ver_domain 1
+        fun $read_version 2
+        var S1
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        fun $call_transition 2
+        var S1
+          type-con $state 0
+        var S2
+          type-con $state 0
+      attribute qid 1
+        string-attr VccPrelu.1017:15
+      attribute uniqueId 1
+        string-attr 112
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    fun $instantiate_bool 1
+    fun $set_in 2
+    var q
+      type-con $ptr 0
+    fun $ver_domain 1
+    fun $read_version 2
+    var S2
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 2 1 3
+      var p
+        type-con $ptr 0
+      var c
+        type-con $ptr 0
+      pat 1
+        fun $in_claim_domain 2
+        var p
+          type-con $ptr 0
+        var c
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.1022:15
+      attribute uniqueId 1
+        string-attr 114
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    forall 1 1 3
+      var s
+        type-con $state 0
+      pat 1
+        fun $dont_instantiate_state 1
+        var s
+          type-con $state 0
+      attribute qid 1
+        string-attr VccPrelu.1023:11
+      attribute uniqueId 1
+        string-attr 113
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $valid_claim 2
+    var s
+      type-con $state 0
+    var c
+      type-con $ptr 0
+    fun $closed 2
+    var s
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $in_claim_domain 2
+    var p
+      type-con $ptr 0
+    var c
+      type-con $ptr 0
+axiom 0
+    forall 4 1 4
+      var S
+        type-con $state 0
+      var c
+        type-con $ptr 0
+      var obj
+        type-con $ptr 0
+      var ptr
+        type-con $ptr 0
+      pat 1
+        fun $by_claim 4
+        var S
+          type-con $state 0
+        var c
+          type-con $ptr 0
+        var obj
+          type-con $ptr 0
+        var ptr
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.1026:32
+      attribute uniqueId 1
+        string-attr 115
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $by_claim 4
+    var S
+      type-con $state 0
+    var c
+      type-con $ptr 0
+    var obj
+      type-con $ptr 0
+    var ptr
+      type-con $ptr 0
+    var ptr
+      type-con $ptr 0
+axiom 0
+    forall 4 2 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var c
+        type-con $ptr 0
+      var f
+        type-con $field 0
+      pat 2
+        fun $in_claim_domain 2
+        var p
+          type-con $ptr 0
+        var c
+          type-con $ptr 0
+        fun $select.mem 2
+        fun $memory 1
+        var S
+          type-con $state 0
+        fun $dot 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+      pat 1
+        fun $by_claim 4
+        var S
+          type-con $state 0
+        var c
+          type-con $ptr 0
+        var p
+          type-con $ptr 0
+        fun $dot 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.1031:15
+      attribute uniqueId 1
+        string-attr 116
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 4
+    fun $good_state 1
+    var S
+      type-con $state 0
+    fun $closed 2
+    var S
+      type-con $state 0
+    var c
+      type-con $ptr 0
+    fun $in_claim_domain 2
+    var p
+      type-con $ptr 0
+    var c
+      type-con $ptr 0
+    fun $is_primitive_non_volatile_field 1
+    var f
+      type-con $field 0
+    and 2
+    fun $in_claim_domain 2
+    var p
+      type-con $ptr 0
+    var c
+      type-con $ptr 0
+    =
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    fun $fetch_from_domain 2
+    fun $claim_version 1
+    var c
+      type-con $ptr 0
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+axiom 0
+    forall 7 2 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var c
+        type-con $ptr 0
+      var f
+        type-con $field 0
+      var i
+        int
+      var sz
+        int
+      var t
+        type-con $ctype 0
+      pat 4
+        fun $valid_claim 2
+        var S
+          type-con $state 0
+        var c
+          type-con $ptr 0
+        fun $in_claim_domain 2
+        var p
+          type-con $ptr 0
+        var c
+          type-con $ptr 0
+        fun $select.mem 2
+        fun $memory 1
+        var S
+          type-con $state 0
+        fun $idx 3
+        fun $dot 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+        var i
+          int
+        var t
+          type-con $ctype 0
+        fun $is_primitive_embedded_array 2
+        var f
+          type-con $field 0
+        var sz
+          int
+      pat 2
+        fun $by_claim 4
+        var S
+          type-con $state 0
+        var c
+          type-con $ptr 0
+        var p
+          type-con $ptr 0
+        fun $idx 3
+        fun $dot 2
+        var p
+          type-con $ptr 0
+        var f
+          type-con $field 0
+        var i
+          int
+        var t
+          type-con $ctype 0
+        fun $is_primitive_embedded_array 2
+        var f
+          type-con $field 0
+        var sz
+          int
+      attribute qid 1
+        string-attr VccPrelu.1040:15
+      attribute uniqueId 1
+        string-attr 117
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 6
+    fun $good_state 1
+    var S
+      type-con $state 0
+    fun $closed 2
+    var S
+      type-con $state 0
+    var c
+      type-con $ptr 0
+    fun $in_claim_domain 2
+    var p
+      type-con $ptr 0
+    var c
+      type-con $ptr 0
+    fun $is_primitive_embedded_array 2
+    var f
+      type-con $field 0
+    var sz
+      int
+    <=
+    int-num 0
+    var i
+      int
+    <
+    var i
+      int
+    var sz
+      int
+    =
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    fun $idx 3
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    var i
+      int
+    var t
+      type-con $ctype 0
+    fun $fetch_from_domain 2
+    fun $claim_version 1
+    var c
+      type-con $ptr 0
+    fun $idx 3
+    fun $dot 2
+    var p
+      type-con $ptr 0
+    var f
+      type-con $field 0
+    var i
+      int
+    var t
+      type-con $ctype 0
+axiom 0
+    forall 2 1 4
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $read_vol_version 2
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.1067:40
+      attribute uniqueId 1
+        string-attr 119
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $read_vol_version 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $int_to_vol_version 1
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+axiom 0
+    forall 5 1 3
+      var S
+        type-con $state 0
+      var r
+        int
+      var t
+        type-con $ctype 0
+      var approver
+        type-con $field 0
+      var subject
+        type-con $field 0
+      pat 2
+        fun $is_approved_by 3
+        var t
+          type-con $ctype 0
+        var approver
+          type-con $field 0
+        var subject
+          type-con $field 0
+        fun $select.mem 2
+        fun $memory 1
+        var S
+          type-con $state 0
+        fun $dot 2
+        fun $ptr 2
+        var t
+          type-con $ctype 0
+        var r
+          int
+        var subject
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.1078:15
+      attribute uniqueId 1
+        string-attr 120
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 4
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    fun $is_approved_by 3
+    var t
+      type-con $ctype 0
+    var approver
+      type-con $field 0
+    var subject
+      type-con $field 0
+    fun $closed 2
+    var S
+      type-con $state 0
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    or 2
+    =
+    fun $int_to_ptr 1
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    fun $dot 2
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var approver
+      type-con $field 0
+    fun $me 0
+    =
+    fun $int_to_ptr 1
+    fun $fetch_from_vv 2
+    fun $read_vol_version 2
+    var S
+      type-con $state 0
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    fun $dot 2
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var approver
+      type-con $field 0
+    fun $me 0
+    =
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    fun $dot 2
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var subject
+      type-con $field 0
+    fun $fetch_from_vv 2
+    fun $read_vol_version 2
+    var S
+      type-con $state 0
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    fun $dot 2
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var subject
+      type-con $field 0
+axiom 0
+    forall 4 1 3
+      var S
+        type-con $state 0
+      var r
+        int
+      var t
+        type-con $ctype 0
+      var subject
+        type-con $field 0
+      pat 2
+        fun $is_owner_approved 2
+        var t
+          type-con $ctype 0
+        var subject
+          type-con $field 0
+        fun $select.mem 2
+        fun $memory 1
+        var S
+          type-con $state 0
+        fun $dot 2
+        fun $ptr 2
+        var t
+          type-con $ctype 0
+        var r
+          int
+        var subject
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.1103:15
+      attribute uniqueId 1
+        string-attr 121
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 4
+    fun $full_stop 1
+    var S
+      type-con $state 0
+    fun $closed 2
+    var S
+      type-con $state 0
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    fun $is_owner_approved 2
+    var t
+      type-con $ctype 0
+    var subject
+      type-con $field 0
+    =
+    fun $owner 2
+    var S
+      type-con $state 0
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    fun $me 0
+    =
+    fun $select.mem 2
+    fun $memory 1
+    var S
+      type-con $state 0
+    fun $dot 2
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var subject
+      type-con $field 0
+    fun $fetch_from_vv 2
+    fun $read_vol_version 2
+    var S
+      type-con $state 0
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    fun $dot 2
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var subject
+      type-con $field 0
+axiom 0
+    forall 5 1 3
+      var S1
+        type-con $state 0
+      var S2
+        type-con $state 0
+      var r
+        int
+      var t
+        type-con $ctype 0
+      var subject
+        type-con $field 0
+      pat 3
+        fun $is_owner_approved 2
+        var t
+          type-con $ctype 0
+        var subject
+          type-con $field 0
+        fun $post_unwrap 2
+        var S1
+          type-con $state 0
+        var S2
+          type-con $state 0
+        fun $select.mem 2
+        fun $memory 1
+        var S1
+          type-con $state 0
+        fun $dot 2
+        fun $ptr 2
+        var t
+          type-con $ctype 0
+        var r
+          int
+        var subject
+          type-con $field 0
+      attribute qid 1
+        string-attr VccPrelu.1111:15
+      attribute uniqueId 1
+        string-attr 122
+      attribute bvZ3Native 1
+        string-attr False
+    fun $instantiate_int 1
+    fun $select.mem 2
+    fun $memory 1
+    var S2
+      type-con $state 0
+    fun $dot 2
+    fun $ptr 2
+    var t
+      type-con $ctype 0
+    var r
+      int
+    var subject
+      type-con $field 0
+axiom 0
+    forall 3 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      pat 2
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $owns 2
+        var S
+          type-con $state 0
+        var q
+          type-con $ptr 0
+        fun $is_non_primitive 1
+        fun $typ 1
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.1133:15
+      attribute uniqueId 1
+        string-attr 124
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 3
+    fun $good_state 1
+    var S
+      type-con $state 0
+    fun $closed 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    fun $is_non_primitive 1
+    fun $typ 1
+    var p
+      type-con $ptr 0
+    =
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $owns 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    =
+    fun $owner 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 4 1 3
+      var #s1
+        type-con $state 0
+      var #s2
+        type-con $state 0
+      var #p
+        type-con $ptr 0
+      var #t
+        type-con $ctype 0
+      pat 2
+        fun $is_arraytype 1
+        var #t
+          type-con $ctype 0
+        fun $inv2 4
+        var #s1
+          type-con $state 0
+        var #s2
+          type-con $state 0
+        var #p
+          type-con $ptr 0
+        var #t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.1140:15
+      attribute uniqueId 1
+        string-attr 125
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    fun $is_arraytype 1
+    var #t
+      type-con $ctype 0
+    =
+    fun $typ 1
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+    and 2
+    =
+    fun $inv2 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+    fun $typed 2
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $sequential 4
+    var #s1
+      type-con $state 0
+    var #s2
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+axiom 0
+    forall 3 1 3
+      var S
+        type-con $state 0
+      var #r
+        int
+      var #t
+        type-con $ctype 0
+      pat 2
+        fun $owns 2
+        var S
+          type-con $state 0
+        fun $ptr 2
+        var #t
+          type-con $ctype 0
+        var #r
+          int
+        fun $is_arraytype 1
+        var #t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.1145:15
+      attribute uniqueId 1
+        string-attr 126
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $good_state 1
+    var S
+      type-con $state 0
+    implies
+    fun $is_arraytype 1
+    var #t
+      type-con $ctype 0
+    =
+    fun $owns 2
+    var S
+      type-con $state 0
+    fun $ptr 2
+    var #t
+      type-con $ctype 0
+    var #r
+      int
+    fun $set_empty 0
+axiom 0
+    forall 3 1 3
+      var S
+        type-con $state 0
+      var #p
+        type-con $ptr 0
+      var #t
+        type-con $ctype 0
+      pat 1
+        fun $inv2 4
+        var S
+          type-con $state 0
+        var S
+          type-con $state 0
+        var #p
+          type-con $ptr 0
+        var #t
+          type-con $ctype 0
+      attribute qid 1
+        string-attr VccPrelu.1149:15
+      attribute uniqueId 1
+        string-attr 127
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 2
+    fun $invok_state 1
+    var S
+      type-con $state 0
+    fun $closed 2
+    var S
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    fun $inv2 4
+    var S
+      type-con $state 0
+    var S
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    var #t
+      type-con $ctype 0
+axiom 0
+    forall 1 1 3
+      var S
+        type-con $state 0
+      pat 1
+        fun $good_state 1
+        var S
+          type-con $state 0
+      attribute qid 1
+        string-attr VccPrelu.1152:15
+      attribute uniqueId 1
+        string-attr 128
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $good_state 1
+    var S
+      type-con $state 0
+    forall 2 1 3
+      var #p
+        type-con $ptr 0
+      var #q
+        type-con $ptr 0
+      pat 1
+        fun $set_in 2
+        var #p
+          type-con $ptr 0
+        fun $owns 2
+        var S
+          type-con $state 0
+        var #q
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.846:13
+      attribute uniqueId 1
+        string-attr 86
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    and 3
+    fun $good_state 1
+    var S
+      type-con $state 0
+    fun $set_in 2
+    var #p
+      type-con $ptr 0
+    fun $owns 2
+    var S
+      type-con $state 0
+    var #q
+      type-con $ptr 0
+    fun $closed 2
+    var S
+      type-con $state 0
+    var #q
+      type-con $ptr 0
+    and 2
+    fun $closed 2
+    var S
+      type-con $state 0
+    var #p
+      type-con $ptr 0
+    not
+    =
+    fun $ref 1
+    var #p
+      type-con $ptr 0
+    int-num 0
+axiom 0
+    forall 3 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var v
+        int
+      pat 1
+        fun $update_int 3
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        var v
+          int
+      attribute qid 1
+        string-attr VccPrelu.1260:15
+      attribute uniqueId 1
+        string-attr 138
+      attribute bvZ3Native 1
+        string-attr False
+    and 6
+    =
+    fun $typemap 1
+    fun $update_int 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var v
+      int
+    fun $typemap 1
+    var S
+      type-con $state 0
+    =
+    fun $statusmap 1
+    fun $update_int 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var v
+      int
+    fun $statusmap 1
+    var S
+      type-con $state 0
+    =
+    fun $memory 1
+    fun $update_int 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var v
+      int
+    fun $store.mem 3
+    fun $memory 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var v
+      int
+    <
+    fun $current_timestamp 1
+    var S
+      type-con $state 0
+    fun $current_timestamp 1
+    fun $update_int 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var v
+      int
+    forall 1 1 4
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $timestamp 2
+        fun $update_int 3
+        var S
+          type-con $state 0
+        var p
+          type-con $ptr 0
+        var v
+          int
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.1280:13
+      attribute uniqueId 1
+        string-attr 140
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    <=
+    fun $timestamp 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $timestamp 2
+    fun $update_int 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var v
+      int
+    var p
+      type-con $ptr 0
+    fun $call_transition 2
+    var S
+      type-con $state 0
+    fun $update_int 3
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    var v
+      int
+axiom 0
+    forall 3 1 3
+      var S
+        type-con $state 0
+      var l
+        type-con $ptr 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $take_over 3
+        var S
+          type-con $state 0
+        var l
+          type-con $ptr 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.1309:15
+      attribute uniqueId 1
+        string-attr 141
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    not
+    =
+    fun $kind_of 1
+    fun $typ 1
+    var l
+      type-con $ptr 0
+    fun $kind_primitive 0
+    and 5
+    =
+    fun $statusmap 1
+    fun $take_over 3
+    var S
+      type-con $state 0
+    var l
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    fun $store.sm 3
+    fun $statusmap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $taken_over 3
+    var S
+      type-con $state 0
+    var l
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    fun $closed 2
+    fun $take_over 3
+    var S
+      type-con $state 0
+    var l
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    =
+    fun $owner 2
+    fun $take_over 3
+    var S
+      type-con $state 0
+    var l
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    var l
+      type-con $ptr 0
+    =
+    fun $ref_cnt 2
+    fun $take_over 3
+    var S
+      type-con $state 0
+    var l
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    fun $ref_cnt 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    true
+axiom 0
+    forall 4 1 3
+      var S0
+        type-con $state 0
+      var S
+        type-con $state 0
+      var l
+        type-con $ptr 0
+      var p
+        type-con $ptr 0
+      pat 1
+        fun $release 4
+        var S0
+          type-con $state 0
+        var S
+          type-con $state 0
+        var l
+          type-con $ptr 0
+        var p
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.1325:15
+      attribute uniqueId 1
+        string-attr 142
+      attribute bvZ3Native 1
+        string-attr False
+    and 6
+    =
+    fun $statusmap 1
+    fun $release 4
+    var S0
+      type-con $state 0
+    var S
+      type-con $state 0
+    var l
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    fun $store.sm 3
+    fun $statusmap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $released 3
+    var S
+      type-con $state 0
+    var l
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    fun $closed 2
+    fun $release 4
+    var S0
+      type-con $state 0
+    var S
+      type-con $state 0
+    var l
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    =
+    fun $owner 2
+    fun $release 4
+    var S0
+      type-con $state 0
+    var S
+      type-con $state 0
+    var l
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    fun $me 0
+    =
+    fun $ref_cnt 2
+    fun $release 4
+    var S0
+      type-con $state 0
+    var S
+      type-con $state 0
+    var l
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    fun $ref_cnt 2
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    =
+    fun $timestamp 2
+    fun $release 4
+    var S0
+      type-con $state 0
+    var S
+      type-con $state 0
+    var l
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    var p
+      type-con $ptr 0
+    fun $current_timestamp 1
+    var S0
+      type-con $state 0
+    true
+axiom 0
+    =
+    fun $get_memory_allocator 0
+    fun $ptr 2
+    fun $memory_allocator_type 0
+    fun $memory_allocator_ref 0
+axiom 0
+    =
+    fun $ptr_level 1
+    fun $memory_allocator_type 0
+    int-num 0
+axiom 0
+    forall 1 1 3
+      var S
+        type-con $state 0
+      pat 1
+        fun $program_entry_point 1
+        var S
+          type-con $state 0
+      attribute qid 1
+        string-attr VccPrelu.1661:15
+      attribute uniqueId 1
+        string-attr 175
+      attribute bvZ3Native 1
+        string-attr False
+    implies
+    fun $program_entry_point 1
+    var S
+      type-con $state 0
+    fun $program_entry_point_ch 1
+    var S
+      type-con $state 0
+axiom 0
+    forall 3 1 3
+      var S
+        type-con $state 0
+      var p
+        type-con $ptr 0
+      var q
+        type-con $ptr 0
+      pat 1
+        fun $set_in 2
+        var p
+          type-con $ptr 0
+        fun $volatile_span 2
+        var S
+          type-con $state 0
+        var q
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.1745:15
+      attribute uniqueId 1
+        string-attr 186
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $volatile_span 2
+    var S
+      type-con $state 0
+    var q
+      type-con $ptr 0
+    or 2
+    =
+    var p
+      type-con $ptr 0
+    var q
+      type-con $ptr 0
+    and 2
+    fun $ts_is_volatile 1
+    fun $select.tm 2
+    fun $typemap 1
+    var S
+      type-con $state 0
+    var p
+      type-con $ptr 0
+    fun $set_in 2
+    var p
+      type-con $ptr 0
+    fun $span 1
+    var q
+      type-con $ptr 0
+axiom 0
+    forall 2 1 3
+      var a
+        type-con $ptr 0
+      var i
+        int
+      pat 1
+        fun $left_split 2
+        var a
+          type-con $ptr 0
+        var i
+          int
+      attribute qid 1
+        string-attr VccPrelu.1752:22
+      attribute uniqueId 1
+        string-attr 187
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $left_split 2
+    var a
+      type-con $ptr 0
+    var i
+      int
+    fun $ptr 2
+    fun $array 2
+    fun $element_type 1
+    fun $typ 1
+    var a
+      type-con $ptr 0
+    var i
+      int
+    fun $ref 1
+    var a
+      type-con $ptr 0
+axiom 0
+    forall 2 1 3
+      var a
+        type-con $ptr 0
+      var i
+        int
+      pat 1
+        fun $right_split 2
+        var a
+          type-con $ptr 0
+        var i
+          int
+      attribute qid 1
+        string-attr VccPrelu.1754:23
+      attribute uniqueId 1
+        string-attr 188
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $right_split 2
+    var a
+      type-con $ptr 0
+    var i
+      int
+    fun $ptr 2
+    fun $array 2
+    fun $element_type 1
+    fun $typ 1
+    var a
+      type-con $ptr 0
+    -
+    fun $array_length 1
+    fun $typ 1
+    var a
+      type-con $ptr 0
+    var i
+      int
+    fun $ref 1
+    fun $idx 3
+    fun $ptr 2
+    fun $element_type 1
+    fun $typ 1
+    var a
+      type-con $ptr 0
+    fun $ref 1
+    var a
+      type-con $ptr 0
+    var i
+      int
+    fun $element_type 1
+    fun $typ 1
+    var a
+      type-con $ptr 0
+axiom 0
+    forall 2 1 3
+      var a1
+        type-con $ptr 0
+      var a2
+        type-con $ptr 0
+      pat 1
+        fun $joined_array 2
+        var a1
+          type-con $ptr 0
+        var a2
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.1757:24
+      attribute uniqueId 1
+        string-attr 189
+      attribute bvZ3Native 1
+        string-attr False
+    =
+    fun $joined_array 2
+    var a1
+      type-con $ptr 0
+    var a2
+      type-con $ptr 0
+    fun $ptr 2
+    fun $array 2
+    fun $element_type 1
+    fun $typ 1
+    var a1
+      type-con $ptr 0
+    +
+    fun $array_length 1
+    fun $typ 1
+    var a1
+      type-con $ptr 0
+    fun $array_length 1
+    fun $typ 1
+    var a2
+      type-con $ptr 0
+    fun $ref 1
+    var a1
+      type-con $ptr 0
+axiom 0
+    forall 1 1 4
+      var #o
+        type-con $ptr 0
+      pat 1
+        fun $set_in 2
+        var #o
+          type-con $ptr 0
+        fun $set_empty 0
+      attribute qid 1
+        string-attr VccPrelu.1854:15
+      attribute uniqueId 1
+        string-attr 198
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    not
+    fun $set_in 2
+    var #o
+      type-con $ptr 0
+    fun $set_empty 0
+axiom 0
+    forall 2 1 4
+      var #r
+        type-con $ptr 0
+      var #o
+        type-con $ptr 0
+      pat 1
+        fun $set_in 2
+        var #o
+          type-con $ptr 0
+        fun $set_singleton 1
+        var #r
+          type-con $ptr 0
+      attribute qid 1
+        string-attr VccPrelu.1857:15
+      attribute uniqueId 1
+        string-attr 199
+      attribute bvZ3Native 1
+        string-attr False
+      attribute weight 1
+        expr-attr
+          int-num 0
+    =
+    fun $set_in 2
+    var #o
+      type-con $ptr 0
+    fun $set_singleton 1
+    var #r
+      type-con $ptr 0
+    =
+    var #r
+      type-con $ptr 0
+    var #o
+      type-con $ptr 0
<