/*
 * Author: heizmann@informatik.uni-freiburg.de
 * Date: 7.8.2010
 *
 * Unstructured Version of the three_times example.
 * (Output of BoogiePreprocessor and BoogiePrinter)
 */


type $ctype;
type $ptr;
type $field;
type $kind;
type $type_state;
type $status;
type $primitive;
type $struct;
type $token;
type $state;
type $pure_function;
type $label;
function $kind_of($ctype) returns ($kind);
const $kind_composite : $kind;
const $kind_primitive : $kind;
const $kind_array : $kind;
const $kind_thread : $kind;
function $sizeof($ctype) returns (int);
const ^^i1 : $ctype;
const ^^i2 : $ctype;
const ^^i4 : $ctype;
const ^^i8 : $ctype;
const ^^u1 : $ctype;
const ^^u2 : $ctype;
const ^^u4 : $ctype;
const ^^u8 : $ctype;
const ^^void : $ctype;
const ^^bool : $ctype;
const ^^f4 : $ctype;
const ^^f8 : $ctype;
const ^^claim : $ctype;
const ^^root_emb : $ctype;
const ^^mathint : $ctype;
axiom $sizeof(^^i1) == 1;
axiom $sizeof(^^i2) == 2;
axiom $sizeof(^^i4) == 4;
axiom $sizeof(^^i8) == 8;
axiom $sizeof(^^u1) == 1;
axiom $sizeof(^^u2) == 2;
axiom $sizeof(^^u4) == 4;
axiom $sizeof(^^u8) == 8;
axiom $sizeof(^^f4) == 4;
axiom $sizeof(^^f8) == 8;
function $as_in_range_t($ctype) returns ($ctype);
axiom $as_in_range_t(^^i1) == ^^i1;
axiom $as_in_range_t(^^i2) == ^^i2;
axiom $as_in_range_t(^^i4) == ^^i4;
axiom $as_in_range_t(^^i8) == ^^i8;
axiom $as_in_range_t(^^u1) == ^^u1;
axiom $as_in_range_t(^^u2) == ^^u2;
axiom $as_in_range_t(^^u4) == ^^u4;
axiom $as_in_range_t(^^u8) == ^^u8;
axiom $as_in_range_t(^^f4) == ^^f4;
axiom $as_in_range_t(^^f8) == ^^f8;
const ^$#thread_id_t : $ctype;
const ^$#ptrset : $ctype;
const ^$#state_t : $ctype;
const ^$#struct : $ctype;
axiom $sizeof(^$#thread_id_t) == 1;
axiom $sizeof(^$#ptrset) == 1;
axiom $ptr_level(^^i1) == 0;
axiom $ptr_level(^^i2) == 0;
axiom $ptr_level(^^i4) == 0;
axiom $ptr_level(^^i8) == 0;
axiom $ptr_level(^^u1) == 0;
axiom $ptr_level(^^u2) == 0;
axiom $ptr_level(^^u4) == 0;
axiom $ptr_level(^^u8) == 0;
axiom $ptr_level(^^f4) == 0;
axiom $ptr_level(^^f8) == 0;
axiom $ptr_level(^^mathint) == 0;
axiom $ptr_level(^^bool) == 0;
axiom $ptr_level(^^void) == 0;
axiom $ptr_level(^^claim) == 0;
axiom $ptr_level(^^root_emb) == 0;
axiom $ptr_level(^$#ptrset) == 0;
axiom $ptr_level(^$#thread_id_t) == 0;
axiom $ptr_level(^$#state_t) == 0;
axiom $ptr_level(^$#struct) == 0;
axiom $is_composite(^^claim);
axiom $is_composite(^^root_emb);
function $ptr_to($ctype) returns ($ctype);
function $spec_ptr_to($ctype) returns ($ctype);
function $unptr_to($ctype) returns ($ctype);
function $ptr_level($ctype) returns (int);
const $arch_ptr_size : int;
axiom (forall #n : $ctype :: { $ptr_to(#n) } $unptr_to($ptr_to(#n)) == #n);
axiom (forall #n : $ctype :: { $spec_ptr_to(#n) } $unptr_to($spec_ptr_to(#n)) == #n);
axiom (forall #n : $ctype :: { $ptr_to(#n) } $sizeof($ptr_to(#n)) == $arch_ptr_size);
axiom (forall #n : $ctype :: { $spec_ptr_to(#n) } $sizeof($ptr_to(#n)) == $arch_ptr_size);
function $map_t($ctype, $ctype) returns ($ctype);
function $map_domain($ctype) returns ($ctype);
function $map_range($ctype) returns ($ctype);
axiom (forall #r : $ctype, #d : $ctype :: { $map_t(#r, #d) } $map_domain($map_t(#r, #d)) == #d);
axiom (forall #r : $ctype, #d : $ctype :: { $map_t(#r, #d) } $map_range($map_t(#r, #d)) == #r);
axiom (forall #n : $ctype :: { $ptr_to(#n) } $ptr_level($ptr_to(#n)) == $ptr_level(#n) + 17);
axiom (forall #n : $ctype :: { $spec_ptr_to(#n) } $ptr_level($spec_ptr_to(#n)) == $ptr_level(#n) + 31);
axiom (forall #r : $ctype, #d : $ctype :: { $map_t(#r, #d) } $ptr_level($map_t(#r, #d)) == $ptr_level(#r) + 23);
function { :weight 0 } $is_primitive(t:$ctype) returns (bool);
axiom (forall t : $ctype :: { $is_primitive(t) } $is_primitive(t) == ($kind_of(t) == $kind_primitive));
function { :weight 0 } $is_composite(t:$ctype) returns (bool);
axiom (forall t : $ctype :: { $is_composite(t) } $is_composite(t) == ($kind_of(t) == $kind_composite));
function { :weight 0 } $is_arraytype(t:$ctype) returns (bool);
axiom (forall t : $ctype :: { $is_arraytype(t) } $is_arraytype(t) == ($kind_of(t) == $kind_array));
function { :weight 0 } $is_threadtype(t:$ctype) returns (bool);
axiom (forall t : $ctype :: { $is_threadtype(t) } $is_threadtype(t) == ($kind_of(t) == $kind_thread));
function $field_offset($field) returns (int);
function $field_parent_type($field) returns ($ctype);
function $is_non_primitive(t:$ctype) returns (bool);
axiom (forall t : $ctype :: { :weight 0 } { $is_composite(t) } $is_composite(t) ==> $is_non_primitive(t));
axiom (forall t : $ctype :: { :weight 0 } { $is_arraytype(t) } $is_arraytype(t) ==> $is_non_primitive(t));
axiom (forall t : $ctype :: { :weight 0 } { $is_threadtype(t) } $is_threadtype(t) ==> $is_non_primitive(t));
axiom (forall #r : $ctype, #d : $ctype :: { $map_t(#r, #d) } $is_primitive($map_t(#r, #d)));
axiom (forall #n : $ctype :: { $ptr_to(#n) } $is_primitive($ptr_to(#n)));
axiom (forall #n : $ctype :: { $spec_ptr_to(#n) } $is_primitive($spec_ptr_to(#n)));
axiom (forall #n : $ctype :: { $is_primitive(#n) } $is_primitive(#n) ==> !$is_claimable(#n));
axiom (forall #n : $ctype :: { $is_claimable(#n) } $is_claimable(#n) ==> $is_composite(#n));
axiom $is_primitive(^^void);
axiom $is_primitive(^^bool);
axiom $is_primitive(^^mathint);
axiom $is_primitive(^$#ptrset);
axiom $is_primitive(^$#state_t);
axiom $is_threadtype(^$#thread_id_t);
axiom $is_primitive(^^i1);
axiom $is_primitive(^^i2);
axiom $is_primitive(^^i4);
axiom $is_primitive(^^i8);
axiom $is_primitive(^^u1);
axiom $is_primitive(^^u2);
axiom $is_primitive(^^u4);
axiom $is_primitive(^^u8);
axiom $is_primitive(^^f4);
axiom $is_primitive(^^f8);
const $me_ref : int;
function $me() returns ($ptr);
axiom $in_range_spec_ptr($me_ref);
axiom $me() == $ptr(^$#thread_id_t, $me_ref);
type $memory_t;
function $select.mem($memory_t, $ptr) returns (int);
function $store.mem($memory_t, $ptr, int) returns ($memory_t);
axiom (forall M : $memory_t, p : $ptr, v : int :: { :weight 0 } $select.mem($store.mem(M, p, v), p) == v);
axiom (forall M : $memory_t, p : $ptr, q : $ptr, v : int :: { :weight 0 } p == q || $select.mem($store.mem(M, p, v), q) == $select.mem(M, q));
type $typemap_t;
function $select.tm($typemap_t, $ptr) returns ($type_state);
function $store.tm($typemap_t, $ptr, $type_state) returns ($typemap_t);
axiom (forall M : $typemap_t, p : $ptr, v : $type_state :: { :weight 0 } $select.tm($store.tm(M, p, v), p) == v);
axiom (forall M : $typemap_t, p : $ptr, q : $ptr, v : $type_state :: { :weight 0 } p == q || $select.tm($store.tm(M, p, v), q) == $select.tm(M, q));
type $statusmap_t;
function $select.sm($statusmap_t, $ptr) returns ($status);
function $store.sm($statusmap_t, $ptr, $status) returns ($statusmap_t);
axiom (forall M : $statusmap_t, p : $ptr, v : $status :: { :weight 0 } $select.sm($store.sm(M, p, v), p) == v);
axiom (forall M : $statusmap_t, p : $ptr, q : $ptr, v : $status :: { :weight 0 } p == q || $select.sm($store.sm(M, p, v), q) == $select.sm(M, q));
function $memory(s:$state) returns ($memory_t);
function $typemap(s:$state) returns ($typemap_t);
function $statusmap(s:$state) returns ($statusmap_t);
function $extent_hint(p:$ptr, q:$ptr) returns (bool);
axiom (forall p : $ptr, q : $ptr, r : $ptr :: { $extent_hint(p, q),$extent_hint(q, r) } $extent_hint(p, q) && $extent_hint(q, r) ==> $extent_hint(p, r));
axiom (forall p : $ptr :: { $typ(p) } $extent_hint(p, p));
function $nesting_level($ctype) returns (int);
function $is_nested($ctype, $ctype) returns (bool);
function $nesting_min($ctype, $ctype) returns (int);
function $nesting_max($ctype, $ctype) returns (int);
function $is_nested_range(t:$ctype, s:$ctype, min:int, max:int) returns (bool);
axiom (forall t : $ctype, s : $ctype, min : int, max : int :: { $is_nested_range(t, s, min, max) } $is_nested_range(t, s, min, max) == ($is_nested(t, s) && $nesting_min(t, s) == min && $nesting_max(t, s) == max));
function $typ($ptr) returns ($ctype);
function $ref($ptr) returns (int);
function $ptr($ctype, int) returns ($ptr);
axiom (forall #t : $ctype, #b : int :: { :weight 0 } $typ($ptr(#t, #b)) == #t);
axiom (forall #t : $ctype, #b : int :: { :weight 0 } $ref($ptr(#t, #b)) == #b);
function $ghost_ref($ptr, $field) returns (int);
function $ghost_emb(int) returns ($ptr);
function $ghost_path(int) returns ($field);
axiom (forall p : $ptr, f : $field :: { :weight 0 } { $ghost_ref(p, f) } $ghost_emb($ghost_ref(p, f)) == p && $ghost_path($ghost_ref(p, f)) == f);
axiom (forall p : $ptr, f : $field :: { $ghost_ref(p, f) } $in_range_spec_ptr($ghost_ref(p, f)));
function $physical_ref(p:$ptr, f:$field) returns (int);
function $array_path(basefield:$field, off:int) returns ($field);
function $is_base_field($field) returns (bool);
function $array_path_1($field) returns ($field);
function $array_path_2($field) returns (int);
axiom (forall fld : $field, off : int :: { :weight 0 } { $array_path(fld, off) } !$is_base_field($array_path(fld, off)) && $array_path_1($array_path(fld, off)) == fld && $array_path_2($array_path(fld, off)) == off);
const $null : $ptr;
axiom $null == $ptr(^^void, 0);
function $is($ptr, $ctype) returns (bool);
axiom (forall #p : $ptr, #t : $ctype :: { :weight 0 } $is(#p, #t) == ($typ(#p) == #t));
axiom (forall #p : $ptr, #t : $ctype :: { $is(#p, #t) } $is(#p, #t) ==> #p == $ptr(#t, $ref(#p)));
function $dot($ptr, $field) returns ($ptr);
function $containing_struct(p:$ptr, f:$field) returns ($ptr);
function $containing_struct_ref(p:$ptr, f:$field) returns (int);
axiom (forall r : int, f : $field :: { $containing_struct($dot($ptr($field_parent_type(f), r), f), f) } $containing_struct($dot($ptr($field_parent_type(f), r), f), f) == $ptr($field_parent_type(f), r));
axiom (forall p : $ptr, f : $field :: { $containing_struct(p, f) } $containing_struct(p, f) == $ptr($field_parent_type(f), $containing_struct_ref(p, f)));
axiom (forall p : $ptr, f : $field :: { $dot($containing_struct(p, f), f) } $field_offset(f) >= 0 ==> $ref($dot($containing_struct(p, f), f)) == $ref(p));
function $is_primitive_non_volatile_field($field) returns (bool);
function $is_primitive_volatile_field($field) returns (bool);
function $is_primitive_embedded_array(f:$field, sz:int) returns (bool);
function $is_primitive_embedded_volatile_array(f:$field, sz:int, t:$ctype) returns (bool);
function $embedded_array_size(f:$field, t:$ctype) returns (int);
function $ts_typed($type_state) returns (bool);
function $ts_emb($type_state) returns ($ptr);
function $ts_path($type_state) returns ($field);
function $ts_is_volatile($type_state) returns (bool);
axiom (forall ts : $type_state :: { $ts_emb(ts) } $kind_of($typ($ts_emb(ts))) != $kind_primitive && $is_non_primitive($typ($ts_emb(ts))));
axiom (forall S : $state, p : $ptr :: { $typed(S, p),$select.tm($typemap(S), $ts_emb($select.tm($typemap(S), p))) } $typed(S, p) ==> $typed(S, $ts_emb($select.tm($typemap(S), p))));
axiom (forall S : $state, p : $ptr :: { $ts_is_volatile($select.tm($typemap(S), p)) } $good_state(S) && $ts_is_volatile($select.tm($typemap(S), p)) ==> $kind_of($typ(p)) == $kind_primitive);
function $current_timestamp(S:$state) returns (int);
axiom (forall S : $state, p : $ptr :: { :weight 0 } { $select.sm($statusmap(S), p) } $timestamp(S, p) <= $current_timestamp(S) || !$ts_typed($select.tm($typemap(S), p)));
function $in_writes_at(time:int, p:$ptr) returns (bool);
const $struct_zero : $struct;
axiom $good_state($vs_state($struct_zero));
function $vs_base_ref($struct) returns (int);
function $vs_state($struct) returns ($state);
axiom (forall s : $struct :: $good_state($vs_state(s)));
function $vs_ctor(S:$state, p:$ptr) returns ($struct);
axiom (forall S : $state, p : $ptr :: { $vs_ctor(S, p) } $good_state(S) ==> $vs_base_ref($vs_ctor(S, p)) == $ref(p) && $vs_state($vs_ctor(S, p)) == S);
axiom (forall f : $field, t : $ctype :: { $select.mem($memory($vs_state($struct_zero)), $dot($ptr(t, $vs_base_ref($struct_zero)), f)) } $select.mem($memory($vs_state($struct_zero)), $dot($ptr(t, $vs_base_ref($struct_zero)), f)) == 0);
type $record;
const $rec_zero : $record;
function $rec_update(r:$record, f:$field, v:int) returns ($record);
function $rec_fetch(r:$record, f:$field) returns (int);
function $rec_update_bv(r:$record, f:$field, val_bitsize:int, from:int, to:int, repl:int) returns ($record);
axiom (forall r : $record, f : $field, val_bitsize : int, from : int, to : int, repl : int :: { $rec_update_bv(r, f, val_bitsize, from, to, repl) } $rec_update_bv(r, f, val_bitsize, from, to, repl) == $rec_update(r, f, $bv_update($rec_fetch(r, f), val_bitsize, from, to, repl)));
axiom (forall f : $field :: $rec_fetch($rec_zero, f) == 0);
axiom (forall r : $record, f : $field, v : int :: { $rec_fetch($rec_update(r, f, v), f) } $rec_fetch($rec_update(r, f, v), f) == $unchecked($record_field_int_kind(f), v));
axiom (forall r : $record, f : $field :: { $rec_fetch(r, f) } $in_range_t($record_field_int_kind(f), $rec_fetch(r, f)));
axiom (forall r : $record, f1 : $field, f2 : $field, v : int :: { $rec_fetch($rec_update(r, f1, v), f2) } $rec_fetch($rec_update(r, f1, v), f2) == $rec_fetch(r, f2) || f1 == f2);
function $is_record_type(t:$ctype) returns (bool);
function $is_record_field(parent:$ctype, field:$field, field_type:$ctype) returns (bool);
axiom (forall t : $ctype :: { $is_record_type(t) } $is_record_type(t) ==> $is_primitive(t));
function $as_record_record_field($field) returns ($field);
axiom (forall p : $ctype, f : $field, ft : $ctype :: { $is_record_field(p, f, ft),$is_record_type(ft) } $is_record_field(p, f, ft) && $is_record_type(ft) ==> $as_record_record_field(f) == f);
function $record_field_int_kind(f:$field) returns ($ctype);
function $rec_eq(r1:$record, r2:$record) returns (bool);
axiom (forall r1 : $record, r2 : $record :: { $rec_eq(r1, r2) } $rec_eq(r1, r2) == (r1 == r2));
function $rec_base_eq(x:int, y:int) returns (bool);
axiom (forall x : int, y : int :: { $rec_base_eq(x, y) } $rec_base_eq(x, y) == (x == y));
function $int_to_record(x:int) returns ($record);
function $record_to_int(r:$record) returns (int);
axiom (forall r : $record :: $int_to_record($record_to_int(r)) == r);
axiom (forall r1 : $record, r2 : $record :: { $rec_eq(r1, r2) } (forall f : $field :: $rec_base_eq($rec_fetch(r1, f), $rec_fetch(r2, f))) ==> $rec_eq(r1, r2));
axiom (forall r1 : $record, r2 : $record, f : $field :: { $rec_base_eq($rec_fetch(r1, f), $rec_fetch(r2, $as_record_record_field(f))) } $rec_eq($int_to_record($rec_fetch(r1, f)), $int_to_record($rec_fetch(r2, f))) ==> $rec_base_eq($rec_fetch(r1, f), $rec_fetch(r2, f)));
var $s : $state;
function $good_state($state) returns (bool);
function $invok_state($state) returns (bool);
const $state_zero : $state;
function $has_volatile_owns_set(t:$ctype) returns (bool);
axiom $has_volatile_owns_set(^^claim);
function $owns_set_field(t:$ctype) returns ($field);
axiom (forall #p : $ptr, t : $ctype :: { $dot(#p, $owns_set_field(t)) } $dot(#p, $owns_set_field(t)) == $ptr(^$#ptrset, $ghost_ref(#p, $owns_set_field(t))));
function $st_owner($status) returns ($ptr);
function $st_closed($status) returns (bool);
function $st_timestamp($status) returns (int);
function $st_ref_cnt(s:$status) returns (int);
function $owner(S:$state, p:$ptr) returns ($ptr);
function $closed(S:$state, p:$ptr) returns (bool);
function $timestamp(S:$state, p:$ptr) returns (int);
axiom (forall S : $state, p : $ptr :: { :weight 0 } { $is_primitive($typ(p)),$owner(S, p) } $is_primitive($typ(p)) ==> $owner(S, p) == $owner(S, $ts_emb($select.tm($typemap(S), p))));
axiom (forall S : $state, p : $ptr :: { :weight 0 } { $is_non_primitive($typ(p)),$owner(S, p) } $is_non_primitive($typ(p)) ==> $owner(S, p) == $st_owner($select.sm($statusmap(S), p)));
axiom (forall S : $state, p : $ptr :: { :weight 0 } { $is_primitive($typ(p)),$closed(S, p) } $is_primitive($typ(p)) ==> $closed(S, p) == $st_closed($select.sm($statusmap(S), $ts_emb($select.tm($typemap(S), p)))));
axiom (forall S : $state, p : $ptr :: { :weight 0 } { $is_non_primitive($typ(p)),$closed(S, p) } $is_non_primitive($typ(p)) ==> $closed(S, p) == $st_closed($select.sm($statusmap(S), p)));
axiom (forall S : $state, p : $ptr :: { :weight 0 } { $is_primitive($typ(p)),$timestamp(S, p) } $is_primitive($typ(p)) ==> $timestamp(S, p) == $st_timestamp($select.sm($statusmap(S), $ts_emb($select.tm($typemap(S), p)))));
axiom (forall S : $state, p : $ptr :: { :weight 0 } { $is_non_primitive($typ(p)),$timestamp(S, p) } $is_non_primitive($typ(p)) ==> $timestamp(S, p) == $st_timestamp($select.sm($statusmap(S), p)));
function $position_marker() returns (bool);
axiom $position_marker();
axiom (forall s : $status :: { $st_owner(s) } $kind_of($typ($st_owner(s))) != $kind_primitive && $is_non_primitive($typ($st_owner(s))));
function { :weight 0 } $owns(S:$state, #p:$ptr) returns ($ptrset);
axiom (forall S : $state, #p : $ptr :: { $owns(S, #p) } $owns(S, #p) == $int_to_ptrset($select.mem($memory(S), $dot(#p, $owns_set_field($typ(#p))))));
function { :weight 0 } $mutable(S:$state, p:$ptr) returns (bool);
axiom (forall S : $state, p : $ptr :: { $mutable(S, p) } $mutable(S, p) == ($typed(S, p) && $owner(S, p) == $me() && !$closed(S, p)));
function $typed(S:$state, p:$ptr) returns (bool);
axiom (forall S : $state, #p : $ptr :: { :weight 0 } { $typed(S, #p) } $good_state(S) ==> $typed(S, #p) == $ts_typed($select.tm($typemap(S), #p)));
axiom (forall S : $state, #p : $ptr :: { $typed(S, #p) } $good_state(S) && $typed(S, #p) ==> $ref(#p) > 0);
function $in_range_phys_ptr(#r:int) returns (bool);
axiom (forall #r : int :: { $in_range_phys_ptr(#r) } $in_range_phys_ptr(#r) == (0 <= #r && #r <= $arch_spec_ptr_start));
function $in_range_spec_ptr(#r:int) returns (bool);
axiom (forall #r : int :: { $in_range_spec_ptr(#r) } $in_range_spec_ptr(#r) == (0 == #r || #r > $arch_spec_ptr_start));
const $arch_spec_ptr_start : int;
axiom (forall S : $state, #r : int, #t : $ctype :: { $typed(S, $ptr(#t, #r)) } $typed(S, $ptr(#t, #r)) && $in_range_phys_ptr(#r) ==> $in_range_phys_ptr(#r + $sizeof(#t) - 1));
function $instantiate_st(s:$status) returns (bool);
axiom (forall S1 : $state, S2 : $state, p : $ptr :: { $select.sm($statusmap(S2), p),$call_transition(S1, S2) } $call_transition(S1, S2) ==> $instantiate_st($select.sm($statusmap(S1), p)));
axiom (forall S1 : $state, S2 : $state, p : $ptr :: { $select.mem($memory(S2), p),$call_transition(S1, S2) } $call_transition(S1, S2) ==> $instantiate_int($select.mem($memory(S1), p)));
function $is_domain_root(S:$state, p:$ptr) returns (bool);
axiom (forall S : $state, p : $ptr :: { $is_domain_root(S, p) } $is_domain_root(S, p) == true);
function $in_wrapped_domain(S:$state, p:$ptr) returns (bool);
axiom (forall S : $state, p : $ptr :: { $in_wrapped_domain(S, p) } $in_wrapped_domain(S, p) == (exists q : $ptr :: { $set_in2(p, $ver_domain($read_version(S, q))) } $set_in(p, $ver_domain($read_version(S, q))) && ($closed(S, q) && $owner(S, q) == $me() && ($is(q, $typ(q)) && $typed(S, q)) && $kind_of($typ(q)) != $kind_primitive && $is_non_primitive($typ(q))) && $is_domain_root(S, q)));
function $thread_local(S:$state, p:$ptr) returns (bool);
axiom (forall S : $state, p : $ptr :: { $thread_local(S, p) } $thread_local(S, p) == ($typed(S, p) && (($kind_of($typ(p)) == $kind_primitive && (!$ts_is_volatile($select.tm($typemap(S), p)) || !$closed(S, $ts_emb($select.tm($typemap(S), p)))) && !($kind_of($typ($ts_emb($select.tm($typemap(S), p)))) == $kind_primitive) && ($owner(S, $ts_emb($select.tm($typemap(S), p))) == $me() || $in_wrapped_domain(S, $ts_emb($select.tm($typemap(S), p))))) || (!($kind_of($typ(p)) == $kind_primitive) && ($owner(S, p) == $me() || $in_wrapped_domain(S, p))))));
function $dont_instantiate($ptr) returns (bool);
function $dont_instantiate_int(int) returns (bool);
function $dont_instantiate_state($state) returns (bool);
function $instantiate_int(int) returns (bool);
function $instantiate_bool(bool) returns (bool);
function $instantiate_ptr($ptr) returns (bool);
function $instantiate_ptrset($ptrset) returns (bool);
function $imply_inv(#s1:$state, #p:$ptr, typ:$ctype) returns (bool);
axiom (forall #s1 : $state, #p : $ptr, typ : $ctype :: { $inv2(#s1, #s1, #p, typ) } $imply_inv(#s1, #p, typ) ==> $inv2(#s1, #s1, #p, typ));
function $inv2(#s1:$state, #s2:$state, #p:$ptr, typ:$ctype) returns (bool);
function { :weight 0 } $sequential(#s1:$state, #s2:$state, #p:$ptr, #t:$ctype) returns (bool);
axiom (forall #s1 : $state, #s2 : $state, #p : $ptr, #t : $ctype :: { $sequential(#s1, #s2, #p, #t) } $sequential(#s1, #s2, #p, #t) == ($closed(#s1, #p) && $closed(#s2, #p) ==> $spans_the_same(#s1, #s2, #p, #t)));
function { :weight 0 } $depends(#s1:$state, #s2:$state, #dependant:$ptr, #this:$ptr) returns (bool);
axiom (forall #s1 : $state, #s2 : $state, #dependant : $ptr, #this : $ptr :: { $depends(#s1, #s2, #dependant, #this) } $depends(#s1, #s2, #dependant, #this) == ($spans_the_same(#s1, #s2, #this, $typ(#this)) || ((!$closed(#s1, #dependant) && !$closed(#s2, #dependant)) || ($inv2(#s1, #s2, #dependant, $typ(#dependant)) && $nonvolatile_spans_the_same(#s1, #s2, #dependant, $typ(#dependant)))) || $is_threadtype($typ(#dependant))));
function { :weight 0 } $spans_the_same(#s1:$state, #s2:$state, #p:$ptr, #t:$ctype) returns (bool);
axiom (forall #s1 : $state, #s2 : $state, #p : $ptr, #t : $ctype :: { $spans_the_same(#s1, #s2, #p, #t) } $spans_the_same(#s1, #s2, #p, #t) == ($read_version(#s1, #p) == $read_version(#s2, #p) && $owns(#s1, #p) == $owns(#s2, #p) && $select.tm($typemap(#s1), #p) == $select.tm($typemap(#s2), #p) && $state_spans_the_same(#s1, #s2, #p, #t)));
function $state_spans_the_same(#s1:$state, #s2:$state, #p:$ptr, #t:$ctype) returns (bool);
function { :weight 0 } $nonvolatile_spans_the_same(#s1:$state, #s2:$state, #p:$ptr, #t:$ctype) returns (bool);
axiom (forall #s1 : $state, #s2 : $state, #p : $ptr, #t : $ctype :: { $nonvolatile_spans_the_same(#s1, #s2, #p, #t) } $nonvolatile_spans_the_same(#s1, #s2, #p, #t) == ($read_version(#s1, #p) == $read_version(#s2, #p) && $select.tm($typemap(#s1), #p) == $select.tm($typemap(#s2), #p) && $state_nonvolatile_spans_the_same(#s1, #s2, #p, #t)));
function $state_nonvolatile_spans_the_same(#s1:$state, #s2:$state, #p:$ptr, #t:$ctype) returns (bool);
function $extent_mutable(S:$state, p:$ptr) returns (bool);
function $extent_is_fresh(S1:$state, S2:$state, p:$ptr) returns (bool);
function $extent_zero(S:$state, p:$ptr) returns (bool);
axiom (forall T : $ctype :: { $is_primitive(T) } $is_primitive(T) ==> (forall r : int, p : $ptr :: { $set_in(p, $full_extent($ptr(T, r))) } $set_in(p, $full_extent($ptr(T, r))) <==> p == $ptr(T, r)) && (forall r : int, S : $state :: { $extent_mutable(S, $ptr(T, r)) } $extent_mutable(S, $ptr(T, r)) <==> $mutable(S, $ptr(T, r))));
axiom (forall T : $ctype :: { $is_primitive(T) } $is_primitive(T) ==> (forall S : $state, r : int, p : $ptr :: { $set_in(p, $extent(S, $ptr(T, r))) } $set_in(p, $extent(S, $ptr(T, r))) <==> p == $ptr(T, r)));
axiom (forall S : $state, T : $ctype, sz : int, r : int :: { $extent_mutable(S, $ptr($array(T, sz), r)) } $extent_mutable(S, $ptr($array(T, sz), r)) <==> $mutable(S, $ptr($array(T, sz), r)) && (forall i : int :: { $extent_mutable(S, $idx($ptr(T, r), i, T)) } 0 <= i && i < sz ==> $extent_mutable(S, $idx($ptr(T, r), i, T))));
axiom (forall T : $ctype :: { $is_primitive(T) } $is_primitive(T) ==> (forall S : $state, r : int :: { $extent_zero(S, $ptr(T, r)) } $extent_zero(S, $ptr(T, r)) <==> $select.mem($memory(S), $ptr(T, r)) == 0));
axiom (forall S : $state, T : $ctype, sz : int, r : int :: { $extent_zero(S, $ptr($array(T, sz), r)) } $extent_zero(S, $ptr($array(T, sz), r)) <==> (forall i : int :: { $idx($ptr(T, r), i, T) } 0 <= i && i < sz ==> $extent_zero(S, $idx($ptr(T, r), i, T))));
function $function_entry($state) returns (bool);
function $full_stop($state) returns (bool);
function $file_name_is(id:int, tok:$token) returns (bool);
axiom (forall S : $state :: { $function_entry(S) } $function_entry(S) ==> $full_stop(S) && $current_timestamp(S) >= 0);
axiom (forall S : $state :: { $full_stop(S) } $full_stop(S) ==> $good_state(S) && $invok_state(S));
axiom (forall S : $state :: { $invok_state(S) } $invok_state(S) ==> $good_state(S));
function $call_transition(S1:$state, S2:$state) returns (bool);
function $good_state_ext(id:$token, S:$state) returns (bool);
axiom (forall id : $token, S : $state :: { $good_state_ext(id, S) } $good_state_ext(id, S) ==> $good_state(S));
function $local_value_is(S1:$state, pos:$token, local_name:$token, val:int, t:$ctype) returns (bool);
function $local_value_is_ptr(S1:$state, pos:$token, local_name:$token, val:$ptr, t:$ctype) returns (bool);
function $read_ptr_m(S:$state, p:$ptr, t:$ctype) returns ($ptr);
axiom (forall S : $state, r : int, t : $ctype :: { $ptr(t, $select.mem($memory(S), $ptr($ptr_to(t), r))) } $ptr(t, $select.mem($memory(S), $ptr($ptr_to(t), r))) == $read_ptr_m(S, $ptr($ptr_to(t), r), t));
axiom (forall S : $state, r : int, t : $ctype :: { $ptr(t, $select.mem($memory(S), $ptr($spec_ptr_to(t), r))) } $ptr(t, $select.mem($memory(S), $ptr($spec_ptr_to(t), r))) == $read_ptr_m(S, $ptr($spec_ptr_to(t), r), t));
function $type_code_is(x:int, tp:$ctype) returns (bool);
function $function_arg_type(fnname:$pure_function, idx:int, tp:$ctype) returns (bool);
type $version;
function $ver_domain($version) returns ($ptrset);
function { :weight 0 } $read_version(S:$state, p:$ptr) returns ($version);
axiom (forall S : $state, p : $ptr :: { $read_version(S, p) } $read_version(S, p) == $int_to_version($select.mem($memory(S), p)));
function { :weight 0 } $domain(S:$state, p:$ptr) returns ($ptrset);
axiom (forall S : $state, p : $ptr :: { $domain(S, p) } $domain(S, p) == $ver_domain($read_version(S, p)));
function $in_domain(S:$state, p:$ptr, q:$ptr) returns (bool);
function $in_vdomain(S:$state, p:$ptr, q:$ptr) returns (bool);
function $in_domain_lab(S:$state, p:$ptr, q:$ptr, l:$label) returns (bool);
function $in_vdomain_lab(S:$state, p:$ptr, q:$ptr, l:$label) returns (bool);
function $inv_lab(S:$state, p:$ptr, l:$label) returns (bool);
axiom (forall S : $state, p : $ptr, q : $ptr, l : $label :: { :weight 0 } { $in_domain_lab(S, p, q, l) } $in_domain_lab(S, p, q, l) ==> $inv_lab(S, p, l));
axiom (forall S : $state, p : $ptr, q : $ptr, l : $label :: { :weight 0 } { $in_domain_lab(S, p, q, l) } $in_domain_lab(S, p, q, l) <==> $in_domain(S, p, q));
axiom (forall S : $state, p : $ptr, q : $ptr, l : $label :: { :weight 0 } { $in_vdomain_lab(S, p, q, l) } $in_vdomain_lab(S, p, q, l) ==> $inv_lab(S, p, l));
axiom (forall S : $state, p : $ptr, q : $ptr, l : $label :: { :weight 0 } { $in_vdomain_lab(S, p, q, l) } $in_vdomain_lab(S, p, q, l) <==> $in_vdomain(S, p, q));
axiom (forall S : $state, p : $ptr, q : $ptr :: { :weight 0 } { $in_domain(S, p, q) } $in_domain(S, p, q) ==> $set_in(p, $domain(S, q)) && $closed(S, p) && (forall r : $ptr :: { $set_in(r, $owns(S, p)) } !$has_volatile_owns_set($typ(p)) && $set_in(r, $owns(S, p)) ==> $set_in2(r, $ver_domain($read_version(S, q)))));
axiom (forall S : $state, p : $ptr :: { $in_domain(S, p, p) } $full_stop(S) && $closed(S, p) && $owner(S, p) == $me() && ($is(p, $typ(p)) && $typed(S, p)) && $kind_of($typ(p)) != $kind_primitive && $is_non_primitive($typ(p)) ==> $in_domain(S, p, p));
axiom (forall S : $state, p : $ptr, q : $ptr :: { :weight 0 } { $in_domain(S, q, p) } $full_stop(S) && $set_in(q, $domain(S, p)) ==> $in_domain(S, q, p));
axiom (forall S : $state, p : $ptr, q : $ptr, r : $ptr :: { :weight 0 } { $set_in(q, $domain(S, p)),$in_domain(S, r, p) } !$has_volatile_owns_set($typ(q)) && $set_in(q, $domain(S, p)) && $set_in0(r, $owns(S, q)) ==> $in_domain(S, r, p) && $set_in0(r, $owns(S, q)));
axiom (forall S : $state, p : $ptr, q : $ptr, r : $ptr :: { :weight 0 } { $set_in(q, $domain(S, p)),$in_vdomain(S, r, p) } $has_volatile_owns_set($typ(q)) && $set_in(q, $domain(S, p)) && (forall S1 : $state :: $inv2(S1, S1, q, $typ(q)) && $read_version(S1, p) == $read_version(S, p) && $domain(S1, p) == $domain(S, p) ==> $set_in0(r, $owns(S1, q))) ==> $in_vdomain(S, r, p) && $set_in0(r, $owns(S, q)));
axiom (forall S : $state, p : $ptr, q : $ptr :: { :weight 0 } { $in_vdomain(S, p, q) } $in_vdomain(S, p, q) ==> $in_domain(S, p, q));
function $fetch_from_domain(v:$version, p:$ptr) returns (int);
axiom (forall S : $state, p : $ptr, d : $ptr, f : $field :: { $set_in(p, $domain(S, d)),$is_primitive_non_volatile_field(f),$select.mem($memory(S), $dot(p, f)) } $set_in(p, $domain(S, d)) && $is_primitive_non_volatile_field(f) ==> $select.mem($memory(S), $dot(p, f)) == $fetch_from_domain($read_version(S, d), $dot(p, f)));
axiom (forall S : $state, p : $ptr, d : $ptr :: { $full_stop(S),$set_in(p, $domain(S, d)),$select.sm($statusmap(S), p) } { $full_stop(S),$set_in(p, $domain(S, d)),$select.tm($typemap(S), p) } $full_stop(S) && $set_in(p, $domain(S, d)) ==> $typed(S, p) && !$ts_is_volatile($select.tm($typemap(S), p)));
axiom (forall S : $state, p : $ptr, d : $ptr, f : $field :: { $set_in(p, $domain(S, d)),$is_primitive_non_volatile_field(f),$owner(S, $dot(p, f)) } { $set_in(p, $domain(S, d)),$is_primitive_non_volatile_field(f),$select.tm($typemap(S), $dot(p, f)) } $full_stop(S) && $set_in(p, $domain(S, d)) && $is_primitive_non_volatile_field(f) ==> $typed(S, $dot(p, f)) && !$ts_is_volatile($select.tm($typemap(S), $dot(p, f))));
axiom (forall S : $state, p : $ptr, d : $ptr, f : $field, sz : int, i : int, t : $ctype :: { $set_in(p, $domain(S, d)),$is_primitive_embedded_array(f, sz),$select.mem($memory(S), $idx($dot(p, f), i, t)) } $full_stop(S) && $set_in(p, $domain(S, d)) && $is_primitive_embedded_array(f, sz) && 0 <= i && i < sz ==> $select.mem($memory(S), $idx($dot(p, f), i, t)) == $fetch_from_domain($read_version(S, d), $idx($dot(p, f), i, t)));
axiom (forall S : $state, p : $ptr, d : $ptr, f : $field, sz : int, i : int, t : $ctype :: { $set_in(p, $domain(S, d)),$is_primitive_embedded_array(f, sz),$select.tm($typemap(S), $idx($dot(p, f), i, t)) } { $set_in(p, $domain(S, d)),$is_primitive_embedded_array(f, sz),$owner(S, $idx($dot(p, f), i, t)) } $full_stop(S) && $set_in(p, $domain(S, d)) && $is_primitive_embedded_array(f, sz) && 0 <= i && i < sz ==> $typed(S, $idx($dot(p, f), i, t)) && !$ts_is_volatile($select.tm($typemap(S), $idx($dot(p, f), i, t))));
axiom (forall S : $state, r : int, d : $ptr, sz : int, i : int, t : $ctype :: { $set_in($ptr($array(t, sz), r), $domain(S, d)),$select.tm($typemap(S), $idx($ptr(t, r), i, t)),$is_primitive(t) } { $set_in($ptr($array(t, sz), r), $domain(S, d)),$owner(S, $idx($ptr(t, r), i, t)),$is_primitive(t) } $full_stop(S) && $is_primitive(t) && $set_in($ptr($array(t, sz), r), $domain(S, d)) && 0 <= i && i < sz ==> $typed(S, $idx($ptr(t, r), i, t)) && !$ts_is_volatile($select.tm($typemap(S), $idx($ptr(t, r), i, t))));
axiom (forall S : $state, r : int, d : $ptr, sz : int, i : int, t : $ctype :: { $set_in($ptr($array(t, sz), r), $domain(S, d)),$select.mem($memory(S), $idx($ptr(t, r), i, t)),$is_primitive(t) } $full_stop(S) && $is_primitive(t) && $set_in($ptr($array(t, sz), r), $domain(S, d)) && 0 <= i && i < sz ==> $select.mem($memory(S), $idx($ptr(t, r), i, t)) == $fetch_from_domain($read_version(S, d), $idx($ptr(t, r), i, t)));
axiom (forall S : $state, p : $ptr, f : $field, sz : int, i : int, t : $ctype :: { $is_primitive_embedded_volatile_array(f, sz, t),$ts_is_volatile($select.tm($typemap(S), $idx($dot(p, f), i, t))) } $good_state(S) && $is_primitive_embedded_volatile_array(f, sz, t) && 0 <= i && i < sz ==> $ts_is_volatile($select.tm($typemap(S), $idx($dot(p, f), i, t))));
axiom (forall p : $ptr, S1 : $state, S2 : $state, q : $ptr :: { :weight 0 } { $set_in(q, $domain(S1, p)),$call_transition(S1, S2) } $instantiate_bool($set_in(q, $domain(S2, p))));
axiom (forall p : $ptr, S1 : $state, S2 : $state, q : $ptr :: { :weight 0 } { $set_in(q, $ver_domain($read_version(S1, p))),$call_transition(S1, S2) } $instantiate_bool($set_in(q, $ver_domain($read_version(S2, p)))));
function $in_claim_domain(p:$ptr, c:$ptr) returns (bool);
axiom (forall p : $ptr, c : $ptr :: { $in_claim_domain(p, c) } (forall s : $state :: { $dont_instantiate_state(s) } $valid_claim(s, c) ==> $closed(s, p)) ==> $in_claim_domain(p, c));
function { :weight 0 } $by_claim(S:$state, c:$ptr, obj:$ptr, ptr:$ptr) returns ($ptr);
axiom (forall S : $state, c : $ptr, obj : $ptr, ptr : $ptr :: { $by_claim(S, c, obj, ptr) } $by_claim(S, c, obj, ptr) == ptr);
function $claim_version($ptr) returns ($version);
axiom (forall S : $state, p : $ptr, c : $ptr, f : $field :: { $in_claim_domain(p, c),$select.mem($memory(S), $dot(p, f)) } { $by_claim(S, c, p, $dot(p, f)) } $good_state(S) && $closed(S, c) && $in_claim_domain(p, c) && $is_primitive_non_volatile_field(f) ==> $in_claim_domain(p, c) && $select.mem($memory(S), $dot(p, f)) == $fetch_from_domain($claim_version(c), $dot(p, f)));
axiom (forall S : $state, p : $ptr, c : $ptr, f : $field, i : int, sz : int, t : $ctype :: { $valid_claim(S, c),$in_claim_domain(p, c),$select.mem($memory(S), $idx($dot(p, f), i, t)),$is_primitive_embedded_array(f, sz) } { $by_claim(S, c, p, $idx($dot(p, f), i, t)),$is_primitive_embedded_array(f, sz) } $good_state(S) && $closed(S, c) && $in_claim_domain(p, c) && $is_primitive_embedded_array(f, sz) && 0 <= i && i < sz ==> $select.mem($memory(S), $idx($dot(p, f), i, t)) == $fetch_from_domain($claim_version(c), $idx($dot(p, f), i, t)));
axiom (forall S : $state, p : $ptr, c : $ptr, i : int, sz : int, t : $ctype :: { $valid_claim(S, c),$in_claim_domain($ptr($array(t, sz), $ref(p)), c),$select.mem($memory(S), $idx(p, i, t)),$is_primitive(t) } { $by_claim(S, c, p, $idx(p, i, t)),$is_primitive(t),$is_array(S, p, t, sz) } $good_state(S) && $closed(S, c) && $in_claim_domain($ptr($array(t, sz), $ref(p)), c) && $is_primitive(t) && 0 <= i && i < sz ==> $select.mem($memory(S), $idx(p, i, t)) == $fetch_from_domain($claim_version(c), $idx(p, i, t)));
procedure $write_ref_cnt(p:$ptr, v:int) returns ();
    modifies $s;
    ensures old($typemap($s)) == $typemap($s);
    ensures old($memory($s)) == $memory($s);
    ensures (forall q : $ptr :: { $select.sm($statusmap($s), q) } q == p || $select.sm($statusmap(old($s)), q) == $select.sm($statusmap($s), q));
    ensures old($owner($s, p)) == $owner($s, p);
    ensures old($owns($s, p)) == $owns($s, p);
    ensures old($closed($s, p)) == $closed($s, p);
    ensures old($timestamp($s, p)) == $timestamp($s, p);
    ensures $ref_cnt($s, p) == v;
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p$0 : $ptr :: { :weight 0 } { $timestamp($s, p$0) } $timestamp(old($s), p$0) <= $timestamp($s, p$0)) && $call_transition(old($s), $s);
    ensures $good_state($s);

type $vol_version;
function { :weight 0 } $read_vol_version(S:$state, p:$ptr) returns ($vol_version);
axiom (forall S : $state, p : $ptr :: { $read_vol_version(S, p) } $read_vol_version(S, p) == $int_to_vol_version($select.mem($memory(S), p)));
function $fetch_from_vv(v:$vol_version, p:$ptr) returns (int);
function $is_approved_by(t:$ctype, approver:$field, subject:$field) returns (bool);
axiom (forall S : $state, r : int, t : $ctype, approver : $field, subject : $field :: { $is_approved_by(t, approver, subject),$select.mem($memory(S), $dot($ptr(t, r), subject)) } $full_stop(S) && $is_approved_by(t, approver, subject) && $closed(S, $ptr(t, r)) && ($int_to_ptr($select.mem($memory(S), $dot($ptr(t, r), approver))) == $me() || $int_to_ptr($fetch_from_vv($read_vol_version(S, $ptr(t, r)), $dot($ptr(t, r), approver))) == $me()) ==> $select.mem($memory(S), $dot($ptr(t, r), subject)) == $fetch_from_vv($read_vol_version(S, $ptr(t, r)), $dot($ptr(t, r), subject)));
function $is_owner_approved(t:$ctype, subject:$field) returns (bool);
axiom (forall S : $state, r : int, t : $ctype, subject : $field :: { $is_owner_approved(t, subject),$select.mem($memory(S), $dot($ptr(t, r), subject)) } $full_stop(S) && $closed(S, $ptr(t, r)) && $is_owner_approved(t, subject) && $owner(S, $ptr(t, r)) == $me() ==> $select.mem($memory(S), $dot($ptr(t, r), subject)) == $fetch_from_vv($read_vol_version(S, $ptr(t, r)), $dot($ptr(t, r), subject)));
axiom (forall S1 : $state, S2 : $state, r : int, t : $ctype, subject : $field :: { $is_owner_approved(t, subject),$post_unwrap(S1, S2),$select.mem($memory(S1), $dot($ptr(t, r), subject)) } $instantiate_int($select.mem($memory(S2), $dot($ptr(t, r), subject))));
procedure $bump_volatile_version(p:$ptr) returns ();
    modifies $s;
    ensures $typemap($s) == $typemap(old($s));
    ensures $statusmap($s) == $statusmap(old($s));
    ensures (forall q : $ptr :: { $select.mem($memory($s), q) } q == p || $select.mem($memory(old($s)), q) == $select.mem($memory($s), q));
    ensures $read_version(old($s), p) == $read_version($s, p);
    ensures $read_vol_version(old($s), p) != $read_vol_version($s, p);
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p$0 : $ptr :: { :weight 0 } { $timestamp($s, p$0) } $timestamp(old($s), p$0) <= $timestamp($s, p$0)) && $call_transition(old($s), $s);

axiom (forall S : $state, p : $ptr, q : $ptr :: { $set_in(p, $owns(S, q)),$is_non_primitive($typ(p)) } $good_state(S) && $closed(S, q) && $is_non_primitive($typ(p)) ==> ($set_in(p, $owns(S, q)) <==> $owner(S, p) == q));
axiom (forall #s1 : $state, #s2 : $state, #p : $ptr, #t : $ctype :: { $is_arraytype(#t),$inv2(#s1, #s2, #p, #t) } $is_arraytype(#t) && $typ(#p) == #t ==> $inv2(#s1, #s2, #p, #t) == $typed(#s2, #p) && $sequential(#s1, #s2, #p, #t));
axiom (forall S : $state, #r : int, #t : $ctype :: { $owns(S, $ptr(#t, #r)),$is_arraytype(#t) } $good_state(S) ==> $is_arraytype(#t) ==> $owns(S, $ptr(#t, #r)) == $set_empty());
axiom (forall S : $state, #p : $ptr, #t : $ctype :: { $inv2(S, S, #p, #t) } $invok_state(S) && $closed(S, #p) ==> $inv2(S, S, #p, #t));
axiom (forall S : $state :: { $good_state(S) } $good_state(S) ==> (forall #p : $ptr, #q : $ptr :: { $set_in(#p, $owns(S, #q)) } $good_state(S) && $set_in(#p, $owns(S, #q)) && $closed(S, #q) ==> $closed(S, #p) && $ref(#p) != 0));
axiom (forall S : $state, #p : $ptr :: { $closed(S, #p) } $closed(S, #p) ==> $typed(S, #p));
function $good_for_admissibility(S:$state) returns (bool);
function $good_for_post_admissibility(S:$state) returns (bool);
procedure $havoc_others(p:$ptr, t:$ctype) returns ();
    modifies $s;
    requires $good_for_admissibility($s);
    ensures $is_stuttering_check() || $spans_the_same(old($s), $s, p, t);
    ensures $nonvolatile_spans_the_same(old($s), $s, p, t);
    ensures $closed($s, p);
    ensures $typed($s, p);
    ensures (forall #p : $ptr, #q : $ptr :: { $set_in(#p, $owns($s, #q)) } $good_state($s) && $set_in(#p, $owns($s, #q)) && $closed($s, #q) ==> $closed($s, #p) && $ref(#p) != 0);
    ensures $good_state($s);
    ensures $good_for_post_admissibility($s);
    ensures (forall #q : $ptr :: { $select.sm($statusmap(old($s)), #q) } { $select.sm($statusmap($s), #q) } ($closed(old($s), #q) || $closed($s, #q)) && (!$spans_the_same(old($s), $s, #q, $typ(#q)) || $closed(old($s), #q) != $closed($s, #q)) ==> $inv2(old($s), $s, #q, $typ(#q)) && $nonvolatile_spans_the_same(old($s), $s, #q, $typ(#q)));
    ensures (forall #q : $ptr :: { $set_in(#q, $owns(old($s), p)) } $set_in(#q, $owns(old($s), p)) ==> $ref_cnt(old($s), #q) == $ref_cnt($s, #q));
    ensures $current_timestamp(old($s)) <= $current_timestamp($s) && (forall p$0 : $ptr :: { :weight 0 } { $timestamp($s, p$0) } $timestamp(old($s), p$0) <= $timestamp($s, p$0)) && $call_transition(old($s), $s);

function $is_stuttering_check() returns (bool);
function $is_unwrap_check() returns (bool);
function $good_for_pre_can_unwrap(S:$state) returns (bool);
function $good_for_post_can_unwrap(S:$state) returns (bool);
procedure $unwrap_check(#l:$ptr) returns ();
    modifies $s;
    requires $good_for_pre_can_unwrap($s);
    ensures $good_state($s);
    ensures $good_for_post_can_unwrap($s);
    ensures $mutable($s, #l);
    ensures $spans_the_same(old($s), $s, #l, $typ(#l));
    ensures (forall #p : $ptr :: { $set_in(#p, $owns(old($s), #l)) } $set_in(#p, $owns(old($s), #l)) ==> $typed(old($s), #p) && ($closed($s, #p) && $owner($s, #p) == $me() && ($is(#p, $typ(#p)) && $typed($s, #p)) && $kind_of($typ(#p)) != $kind_primitive && $is_non_primitive($typ(#p))) && $timestamp($s, #p) == $current_timestamp($s) && $is_non_primitive($typ(#p)));
    ensures (forall #p : $ptr :: { $set_in(#p, $owns(old($s), #l)),$is_claimable($typ(#p)) } $set_in(#p, $owns(old($s), #l)) ==> $is_claimable($typ(#p)) ==> old($ref_cnt($s, #p)) == $ref_cnt($s, #p));
    ensures $timestamp($s, #l) == $current_timestamp($s);
    ensures $typemap(old($s)) == $typemap($s);
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } #p == #l || ($kind_of($typ($owner(old($s), #p))) != $kind_thread && $set_in(#p, $owns(old($s), #l))) || $select.sm($statusmap($s), #p) == $select.sm($statusmap(old($s)), #p));
    ensures (exists #x : int :: $memory($s) == $store.mem($memory(old($s)), #l, #x));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

procedure $write_int(p:$ptr, v:int) returns ();
    modifies $s;
    ensures $typemap($s) == $typemap(old($s));
    ensures $statusmap($s) == $statusmap(old($s));
    ensures $memory($s) == $store.mem($memory(old($s)), p, v);
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p$0 : $ptr :: { :weight 0 } { $timestamp($s, p$0) } $timestamp(old($s), p$0) <= $timestamp($s, p$0)) && $call_transition(old($s), $s);

function $update_int(S:$state, p:$ptr, v:int) returns ($state);
axiom (forall S : $state, p : $ptr, v : int :: { $update_int(S, p, v) } $typemap($update_int(S, p, v)) == $typemap(S) && $statusmap($update_int(S, p, v)) == $statusmap(S) && $memory($update_int(S, p, v)) == $store.mem($memory(S), p, v) && $current_timestamp(S) < $current_timestamp($update_int(S, p, v)) && (forall p$0 : $ptr :: { :weight 0 } { $timestamp($update_int(S, p, v), p$0) } $timestamp(S, p$0) <= $timestamp($update_int(S, p, v), p$0)) && $call_transition(S, $update_int(S, p, v)));
function $pre_wrap($state) returns (bool);
function $pre_unwrap($state) returns (bool);
function $pre_static_wrap($state) returns (bool);
function $pre_static_unwrap($state) returns (bool);
function $expect_unreachable() returns (bool);
function $taken_over(S:$state, #l:$ptr, #p:$ptr) returns ($status);
function $take_over(S:$state, #l:$ptr, #p:$ptr) returns ($state);
axiom (forall S : $state, l : $ptr, p : $ptr :: { $take_over(S, l, p) } $kind_of($typ(l)) != $kind_primitive ==> $statusmap($take_over(S, l, p)) == $store.sm($statusmap(S), p, $taken_over(S, l, p)) && $closed($take_over(S, l, p), p) && $owner($take_over(S, l, p), p) == l && $ref_cnt($take_over(S, l, p), p) == $ref_cnt(S, p) && true);
function $released(S:$state, #l:$ptr, #p:$ptr) returns ($status);
function $release(S0:$state, S:$state, #l:$ptr, #p:$ptr) returns ($state);
axiom (forall S0 : $state, S : $state, l : $ptr, p : $ptr :: { $release(S0, S, l, p) } $statusmap($release(S0, S, l, p)) == $store.sm($statusmap(S), p, $released(S, l, p)) && $closed($release(S0, S, l, p), p) && $owner($release(S0, S, l, p), p) == $me() && $ref_cnt($release(S0, S, l, p), p) == $ref_cnt(S, p) && $timestamp($release(S0, S, l, p), p) == $current_timestamp(S0) && true);
function $post_unwrap(S1:$state, S2:$state) returns (bool);
procedure $static_unwrap(#l:$ptr, S:$state) returns ();
    modifies $s;
    requires !$is_claimable($typ(#l)) || $ref_cnt($s, #l) == 0;
    requires $pre_static_unwrap($s);
    ensures $mutable($s, #l);
    ensures $owns(old($s), #l) == $owns($s, #l);
    ensures $timestamp($s, #l) == $current_timestamp($s);
    ensures $typemap(old($s)) == $typemap($s);
    ensures (exists #x : int :: $memory($s) == $store.mem($memory(old($s)), #l, #x));
    ensures (exists #st : $status :: $statusmap($s) == $store.sm($statusmap(S), #l, #st));
    ensures (forall #p : $ptr :: { $thread_local($s, #p) } $thread_local(old($s), #p) ==> $thread_local($s, #p));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures $post_unwrap(old($s), $s);

procedure $static_wrap(#l:$ptr, S:$state, owns:$ptrset) returns ();
    modifies $s;
    requires $pre_static_wrap($s);
    requires $kind_of($typ(#l)) != $kind_primitive;
    requires $typed($s, #l);
    requires !$closed($s, #l);
    requires $owner($s, #l) == $me();
    ensures $closed($s, #l) && $owner($s, #l) == $me() && ($is(#l, $typ(#l)) && $typed($s, #l)) && $kind_of($typ(#l)) != $kind_primitive && $is_non_primitive($typ(#l));
    ensures $is_claimable($typ(#l)) ==> old($ref_cnt($s, #l)) == 0 && $ref_cnt($s, #l) == 0;
    ensures $typemap(old($s)) == $typemap($s);
    ensures (exists #st : $status :: $statusmap($s) == $store.sm($statusmap(S), #l, #st));
    ensures (exists #x : int :: $memory($s) == $store.mem($store.mem($memory(old($s)), #l, #x), $dot(#l, $owns_set_field($typ(#l))), $ptrset_to_int(owns)));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

procedure $static_wrap_non_owns(#l:$ptr, S:$state) returns ();
    modifies $s;
    requires $pre_static_wrap($s);
    requires $kind_of($typ(#l)) != $kind_primitive;
    requires $typed($s, #l);
    requires !$closed($s, #l);
    requires $owner($s, #l) == $me();
    ensures $closed($s, #l) && $owner($s, #l) == $me() && ($is(#l, $typ(#l)) && $typed($s, #l)) && $kind_of($typ(#l)) != $kind_primitive && $is_non_primitive($typ(#l));
    ensures $is_claimable($typ(#l)) ==> old($ref_cnt($s, #l)) == 0 && $ref_cnt($s, #l) == 0;
    ensures $typemap(old($s)) == $typemap($s);
    ensures (exists #st : $status :: $statusmap($s) == $store.sm($statusmap(S), #l, #st));
    ensures (exists #x : int :: $memory($s) == $store.mem($memory(old($s)), #l, #x));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

procedure $unwrap(#l:$ptr, T:$ctype) returns ();
    modifies $s;
    requires !$is_claimable(T) || $ref_cnt($s, #l) == 0;
    requires $pre_unwrap($s);
    ensures $mutable($s, #l);
    ensures $owns(old($s), #l) == $owns($s, #l);
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } { $select.tm($typemap($s), #p) } { $set_in(#p, $owns(old($s), #l)) } $set_in(#p, $owns(old($s), #l)) ==> $typed(old($s), #p) && ($closed($s, #p) && $owner($s, #p) == $me() && ($is(#p, $typ(#p)) && $typed($s, #p)) && $kind_of($typ(#p)) != $kind_primitive && $is_non_primitive($typ(#p))) && $timestamp($s, #p) == $current_timestamp($s) && $is_non_primitive($typ(#p)));
    ensures (forall #p : $ptr :: { $set_in(#p, $owns(old($s), #l)),$is_claimable($typ(#p)) } $set_in(#p, $owns(old($s), #l)) ==> $is_claimable($typ(#p)) ==> old($ref_cnt($s, #p)) == $ref_cnt($s, #p));
    ensures (forall #p : $ptr :: { $thread_local($s, #p) } $thread_local(old($s), #p) ==> $thread_local($s, #p));
    ensures $timestamp($s, #l) == $current_timestamp($s);
    ensures $typemap(old($s)) == $typemap($s);
    ensures (forall #p : $ptr :: { :weight 0 } { $select.sm($statusmap($s), #p) } $select.sm($statusmap($s), #p) == $select.sm($statusmap(old($s)), #p) || ($kind_of($typ($owner(old($s), #p))) != $kind_thread && $set_in(#p, $owns(old($s), #l))) || #p == #l);
    ensures (exists #x : int :: $memory($s) == $store.mem($memory(old($s)), #l, #x));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures $post_unwrap(old($s), $s);

procedure $wrap(#l:$ptr, T:$ctype) returns ();
    modifies $s;
    requires $pre_wrap($s);
    requires $kind_of($typ(#l)) != $kind_primitive;
    requires $is(#l, T) && $typed($s, #l);
    requires !$closed($s, #l);
    requires $owner($s, #l) == $me();
    requires (forall #p : $ptr :: { $dont_instantiate(#p) } $set_in0(#p, $owns($s, #l)) ==> $closed($s, #p) && $owner($s, #p) == $me() && ($is(#p, $typ(#p)) && $typed($s, #p)) && $kind_of($typ(#p)) != $kind_primitive && $is_non_primitive($typ(#p)));
    ensures $owns(old($s), #l) == $owns($s, #l);
    ensures (forall #p : $ptr :: { $set_in(#p, $owns($s, #l)) } $set_in(#p, $owns($s, #l)) ==> $is_non_primitive($typ(#p)) && $owner($s, #p) == #l && $closed($s, #p));
    ensures $closed($s, #l) && $owner($s, #l) == $me() && ($is(#l, $typ(#l)) && $typed($s, #l)) && $kind_of($typ(#l)) != $kind_primitive && $is_non_primitive($typ(#l));
    ensures $is_claimable(T) ==> old($ref_cnt($s, #l)) == 0 && $ref_cnt($s, #l) == 0;
    ensures (forall #p : $ptr :: { $set_in(#p, $owns(old($s), #l)),$is_claimable($typ(#p)) } $set_in(#p, $owns(old($s), #l)) ==> $is_claimable($typ(#p)) ==> old($ref_cnt($s, #p)) == $ref_cnt($s, #p));
    ensures $typemap(old($s)) == $typemap($s);
    ensures (forall #p : $ptr :: { :weight 0 } { $select.sm($statusmap($s), #p) } $select.sm($statusmap($s), #p) == $select.sm($statusmap(old($s)), #p) || (($closed(old($s), #p) && $owner(old($s), #p) == $me() && ($is(#p, $typ(#p)) && $typed(old($s), #p)) && $kind_of($typ(#p)) != $kind_primitive && $is_non_primitive($typ(#p))) && $set_in(#p, $owns(old($s), #l))) || #p == #l);
    ensures (exists #x : int :: $memory($s) == $store.mem($memory(old($s)), #l, #x));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

procedure $bump_timestamp() returns ();
    modifies $s;
    ensures $memory($s) == $memory(old($s));
    ensures $typemap($s) == $typemap(old($s));
    ensures (exists x : $status :: $statusmap($s) == $store.sm($statusmap(old($s)), $null, x));
    ensures $current_timestamp(old($s)) < $current_timestamp($s);

procedure $deep_unwrap(#l:$ptr, T:$ctype) returns ();
    modifies $s;
    requires $closed($s, #l) && $owner($s, #l) == $me() && ($is(#l, T) && $typed($s, #l)) && $kind_of(T) != $kind_primitive && $is_non_primitive(T);
    requires $inv2($s, $s, #l, T) ==> $set_eq($owns($s, #l), $set_empty());
    ensures $inv2($s, $s, #l, T);
    ensures !$closed($s, #l);
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } $set_in(#p, $full_extent(#l)) ==> $timestamp($s, #p) == $current_timestamp($s) && !$closed($s, #p) && (#p == #l || $kind_of($typ($owner(old($s), #p))) != $kind_thread));
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } $set_in(#p, $extent($s, #l)) ==> $owner($s, #p) == $me());
    ensures (forall #p : $ptr :: { $thread_local($s, #p) } $thread_local(old($s), #p) ==> $thread_local($s, #p));
    ensures $typemap($s) == $typemap(old($s));
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } !$typed(old($s), #p) || $set_in(#p, $full_extent(#l)) || $select.sm($statusmap(old($s)), #p) == $select.sm($statusmap($s), #p));
    ensures (forall #p : $ptr :: { $select.mem($memory($s), #p) } $set_in(#p, $full_extent(#l)) || $select.mem($memory(old($s)), #p) == $select.mem($memory($s), #p));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures $post_unwrap(old($s), $s);

procedure $set_owns(#p:$ptr, owns:$ptrset) returns ();
    modifies $s;
    requires $kind_of($typ(#p)) == $kind_composite;
    requires $mutable($s, #p);
    ensures $statusmap(old($s)) == $statusmap($s);
    ensures $typemap(old($s)) == $typemap($s);
    ensures $memory($s) == $store.mem(old($memory($s)), $dot(#p, $owns_set_field($typ(#p))), $ptrset_to_int(owns));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

procedure $set_closed_owner(#p:$ptr, owner:$ptr) returns ();
    modifies $s;
    requires $kind_of($typ(owner)) == $kind_composite;
    requires $kind_of($typ(#p)) != $kind_primitive;
    requires $owner($s, #p) == $me();
    requires $closed($s, #p);
    requires $closed($s, owner);
    requires $has_volatile_owns_set($typ(owner));
    ensures $typemap(old($s)) == $typemap($s);
    ensures (exists st : $status :: $statusmap($s) == $store.sm(old($statusmap($s)), #p, st) && $st_owner(st) == owner && $st_closed(st));
    ensures $ref_cnt(old($s), #p) == $ref_cnt($s, #p);
    ensures $memory($s) == $store.mem(old($memory($s)), $dot(owner, $owns_set_field($typ(owner))), $ptrset_to_int($set_union($set_singleton(#p), $owns(old($s), owner))));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures $set_in(#p, $owns($s, owner));

procedure $set_closed_owns(owner:$ptr, owns:$ptrset) returns ();
    modifies $s;
    requires $kind_of($typ(owner)) == $kind_composite;
    requires (forall p : $ptr :: { $dont_instantiate(p) } { sk_hack($set_in0(p, $owns($s, owner))) } $set_in(p, $set_difference(owns, $owns($s, owner))) ==> $closed($s, p) && $owner($s, p) == $me() && ($is(p, $typ(p)) && $typed($s, p)) && $kind_of($typ(p)) != $kind_primitive && $is_non_primitive($typ(p)));
    requires $closed($s, owner);
    requires $has_volatile_owns_set($typ(owner));
    ensures $typemap(old($s)) == $typemap($s);
    ensures (forall #p : $ptr :: { $set_in(#p, $owns(old($s), owner)) } $set_in(#p, $owns(old($s), owner)) ==> $is_non_primitive($typ(#p)));
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } { $select.tm($typemap($s), #p) } $ref_cnt(old($s), #p) == $ref_cnt($s, #p) && (if $set_in(#p, $owns(old($s), owner)) then (if $set_in(#p, owns) then $select.sm($statusmap(old($s)), #p) == $select.sm($statusmap($s), #p) else ($closed($s, #p) && $owner($s, #p) == $me() && ($is(#p, $typ(#p)) && $typed($s, #p)) && $kind_of($typ(#p)) != $kind_primitive && $is_non_primitive($typ(#p))) && $timestamp($s, #p) == $current_timestamp($s)) else (if $set_in(#p, owns) then $owner($s, #p) == owner && $closed($s, #p) else $select.sm($statusmap(old($s)), #p) == $select.sm($statusmap($s), #p))));
    ensures $memory($s) == $store.mem(old($memory($s)), $dot(owner, $owns_set_field($typ(owner))), $ptrset_to_int(owns));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

procedure $giveup_closed_owner(#p:$ptr, owner:$ptr) returns ();
    modifies $s;
    requires $kind_of($typ(owner)) == $kind_composite;
    requires $set_in(#p, $owns($s, owner));
    requires $closed($s, owner);
    requires $has_volatile_owns_set($typ(owner));
    ensures $typed($s, #p);
    ensures $typemap(old($s)) == $typemap($s);
    ensures (exists st : $status :: $statusmap($s) == $store.sm($statusmap(old($s)), #p, st));
    ensures $closed($s, #p) && $owner($s, #p) == $me() && ($is(#p, $typ(#p)) && $typed($s, #p)) && $kind_of($typ(#p)) != $kind_primitive && $is_non_primitive($typ(#p));
    ensures $timestamp($s, #p) == $current_timestamp($s);
    ensures $ref_cnt(old($s), #p) == $ref_cnt($s, #p);
    ensures $memory($s) == $store.mem(old($memory($s)), $dot(owner, $owns_set_field($typ(owner))), $ptrset_to_int($set_difference($owns(old($s), owner), $set_singleton(#p))));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

function $get_memory_allocator() returns ($ptr);
function $is_in_stackframe(#sf:int, p:$ptr) returns (bool);
const $memory_allocator_type : $ctype;
const $memory_allocator_ref : int;
axiom $get_memory_allocator() == $ptr($memory_allocator_type, $memory_allocator_ref);
axiom $ptr_level($memory_allocator_type) == 0;
procedure $stack_alloc(#t:$ctype, #sf:int, #spec:bool) returns (#r:$ptr);
    modifies $s;
    ensures $is(#r, #t) && $typed($s, #r);
    ensures $extent_mutable($s, #r);
    ensures $extent_is_fresh(old($s), $s, #r);
    ensures $mutable($s, $ts_emb($select.tm($typemap($s), #r)));
    ensures (forall #p : $ptr :: { $select.tm($typemap($s), #p) } { $select.sm($statusmap($s), #p) } $set_in(#p, $extent($s, #r)) ==> $mutable($s, #p) && $kind_of($typ($owner(old($s), #p))) != $kind_thread && $owns($s, #p) == $set_empty() && $timestamp($s, #p) == $current_timestamp($s));
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } #p == $ts_emb($select.tm($typemap($s), #r)) || $set_in(#p, $full_extent(#r)) ==> $timestamp($s, #p) == $current_timestamp($s));
    ensures $memory(old($s)) == $memory($s);
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } $typed(old($s), #p) || !($kind_of($typ($owner(old($s), #p))) != $kind_thread) ==> $select.sm($statusmap(old($s)), #p) == $select.sm($statusmap($s), #p));
    ensures (forall #p : $ptr :: { $select.tm($typemap($s), #p) } $typed(old($s), #p) || !($kind_of($typ($owner(old($s), #p))) != $kind_thread) ==> $select.tm($typemap(old($s)), #p) == $select.tm($typemap($s), #p));
    ensures (forall #p : $ptr :: { $thread_local($s, #p) } $thread_local(old($s), #p) ==> $thread_local($s, #p));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures !$typed(old($s), #r);
    ensures $is_in_stackframe(#sf, #r);
    ensures $ts_emb($select.tm($typemap($s), #r)) == $ptr(^^root_emb, $ref(#r));
    ensures $first_option_typed($s, #r);
    ensures #spec ==> $in_range_spec_ptr($ref(#r));
    ensures !#spec ==> $in_range_phys_ptr($ref(#r)) && $in_range_phys_ptr($ref(#r) + $sizeof(#t) - 1);

procedure $stack_free(#sf:int, #x:$ptr) returns ();
    modifies $s;
    requires $extent_mutable($s, #x);
    requires $is_in_stackframe(#sf, #x);
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } $set_in(#p, $full_extent(#x)) || $select.sm($statusmap($s), #p) == $select.sm($statusmap(old($s)), #p));
    ensures (forall #p : $ptr :: { $select.tm($typemap($s), #p) } $set_in(#p, $full_extent(#x)) || $select.tm($typemap($s), #p) == $select.tm($typemap(old($s)), #p));
    ensures $memory($s) == $memory(old($s));
    ensures $current_timestamp(old($s)) <= $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

procedure $spec_alloc(#t:$ctype) returns (#r:$ptr);
    modifies $s;
    ensures $is(#r, #t) && $typed($s, #r);
    ensures $extent_mutable($s, #r);
    ensures $extent_is_fresh(old($s), $s, #r);
    ensures $mutable($s, $ts_emb($select.tm($typemap($s), #r)));
    ensures (forall #p : $ptr :: { $select.tm($typemap($s), #p) } { $select.sm($statusmap($s), #p) } $set_in(#p, $extent($s, #r)) ==> $mutable($s, #p) && $kind_of($typ($owner(old($s), #p))) != $kind_thread && $owns($s, #p) == $set_empty() && $timestamp($s, #p) == $current_timestamp($s));
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } #p == $ts_emb($select.tm($typemap($s), #r)) || $set_in(#p, $full_extent(#r)) ==> $timestamp($s, #p) == $current_timestamp($s));
    ensures $memory(old($s)) == $memory($s);
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } $typed(old($s), #p) || !($kind_of($typ($owner(old($s), #p))) != $kind_thread) ==> $select.sm($statusmap(old($s)), #p) == $select.sm($statusmap($s), #p));
    ensures (forall #p : $ptr :: { $select.tm($typemap($s), #p) } $typed(old($s), #p) || !($kind_of($typ($owner(old($s), #p))) != $kind_thread) ==> $select.tm($typemap(old($s)), #p) == $select.tm($typemap($s), #p));
    ensures (forall #p : $ptr :: { $thread_local($s, #p) } $thread_local(old($s), #p) ==> $thread_local($s, #p));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures !$typed(old($s), #r);
    ensures $ts_emb($select.tm($typemap($s), #r)) == $ptr(^^root_emb, $ref(#r));
    ensures $ts_emb($select.tm($typemap($s), #r)) == $ptr(^^root_emb, $ref(#r));
    ensures $first_option_typed($s, #r);
    ensures $in_range_spec_ptr($ref(#r));

procedure $spec_alloc_array(#t:$ctype, sz:int) returns (#r:$ptr);
    modifies $s;
    ensures $is(#r, $array(#t, sz)) && $typed($s, #r);
    ensures $extent_mutable($s, #r);
    ensures $extent_is_fresh(old($s), $s, #r);
    ensures $mutable($s, $ts_emb($select.tm($typemap($s), #r)));
    ensures (forall #p : $ptr :: { $select.tm($typemap($s), #p) } { $select.sm($statusmap($s), #p) } $set_in(#p, $extent($s, #r)) ==> $mutable($s, #p) && $kind_of($typ($owner(old($s), #p))) != $kind_thread && $owns($s, #p) == $set_empty() && $timestamp($s, #p) == $current_timestamp($s));
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } #p == $ts_emb($select.tm($typemap($s), #r)) || $set_in(#p, $full_extent(#r)) ==> $timestamp($s, #p) == $current_timestamp($s));
    ensures $memory(old($s)) == $memory($s);
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } $typed(old($s), #p) || !($kind_of($typ($owner(old($s), #p))) != $kind_thread) ==> $select.sm($statusmap(old($s)), #p) == $select.sm($statusmap($s), #p));
    ensures (forall #p : $ptr :: { $select.tm($typemap($s), #p) } $typed(old($s), #p) || !($kind_of($typ($owner(old($s), #p))) != $kind_thread) ==> $select.tm($typemap(old($s)), #p) == $select.tm($typemap($s), #p));
    ensures (forall #p : $ptr :: { $thread_local($s, #p) } $thread_local(old($s), #p) ==> $thread_local($s, #p));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures !$typed(old($s), #r);
    ensures $ts_emb($select.tm($typemap($s), #r)) == $ptr(^^root_emb, $ref(#r));
    ensures $ts_emb($select.tm($typemap($s), #r)) == $ptr(^^root_emb, $ref(#r));
    ensures $first_option_typed($s, #r);
    ensures $in_range_spec_ptr($ref(#r));

procedure $alloc(#t:$ctype) returns (#r:$ptr);
    modifies $s;
    ensures $ref(#r) == 0 || ($is(#r, #t) && $typed($s, #r));
    ensures $ref(#r) == 0 || $extent_mutable($s, #r);
    ensures $ref(#r) == 0 || $extent_is_fresh(old($s), $s, #r);
    ensures $ref(#r) == 0 || $mutable($s, $ts_emb($select.tm($typemap($s), #r)));
    ensures (forall #p : $ptr :: { $select.tm($typemap($s), #p) } { $select.sm($statusmap($s), #p) } $set_in(#p, $extent($s, #r)) ==> $mutable($s, #p) && $kind_of($typ($owner(old($s), #p))) != $kind_thread && $owns($s, #p) == $set_empty() && $timestamp($s, #p) == $current_timestamp($s));
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } #p == $ts_emb($select.tm($typemap($s), #r)) || $set_in(#p, $full_extent(#r)) ==> $timestamp($s, #p) == $current_timestamp($s));
    ensures $memory(old($s)) == $memory($s);
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } $typed(old($s), #p) || !($kind_of($typ($owner(old($s), #p))) != $kind_thread) ==> $select.sm($statusmap(old($s)), #p) == $select.sm($statusmap($s), #p));
    ensures (forall #p : $ptr :: { $select.tm($typemap($s), #p) } $typed(old($s), #p) || !($kind_of($typ($owner(old($s), #p))) != $kind_thread) ==> $select.tm($typemap(old($s)), #p) == $select.tm($typemap($s), #p));
    ensures (forall #p : $ptr :: { $thread_local($s, #p) } $thread_local(old($s), #p) ==> $thread_local($s, #p));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures !$typed(old($s), #r);
    ensures $ref(#r) == 0 || $ts_emb($select.tm($typemap($s), #r)) == $ptr(^^root_emb, $ref(#r));
    ensures $ref(#r) == 0 || $ts_emb($select.tm($typemap($s), #r)) == $ptr(^^root_emb, $ref(#r));
    ensures $ref(#r) == 0 || $first_option_typed($s, #r);
    ensures $in_range_phys_ptr($ref(#r)) && $in_range_phys_ptr($ref(#r) + $sizeof(#t) - 1);

procedure $free(#x:$ptr) returns ();
    modifies $s;
    requires $typed($s, #x);
    requires $ts_emb($select.tm($typemap($s), #x)) == $ptr(^^root_emb, $ref(#x));
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } $set_in(#p, $full_extent(#x)) || $select.sm($statusmap($s), #p) == $select.sm($statusmap(old($s)), #p));
    ensures (forall #p : $ptr :: { $select.tm($typemap($s), #p) } $set_in(#p, $full_extent(#x)) || $select.tm($typemap($s), #p) == $select.tm($typemap(old($s)), #p));
    ensures $memory($s) == $memory(old($s));
    ensures $current_timestamp(old($s)) <= $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

function $program_entry_point(s:$state) returns (bool);
function $program_entry_point_ch(s:$state) returns (bool);
axiom (forall S : $state :: { $program_entry_point(S) } $program_entry_point(S) ==> $program_entry_point_ch(S));
procedure $havoc(o:$ptr, t:$ctype) returns ();
    modifies $s;
    requires $is(o, t);
    ensures $typemap($s) == $typemap(old($s));
    ensures $statusmap($s) == $statusmap(old($s));
    ensures (forall #p : $ptr :: { $select.mem($memory($s), #p) } $set_in(#p, $extent(old($s), o)) || $select.mem($memory(old($s)), #p) == $select.mem($memory($s), #p));

function $ts_active_option($type_state) returns ($field);
procedure $union_reinterpret(#x:$ptr, #off:$field) returns ();
    modifies $s;
    requires $is_union_field($typ(#x), #off);
    requires $typed($s, #x);
    ensures $ts_active_option($select.tm($typemap($s), #x)) == #off;
    ensures $typed($s, #x);
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } $set_in(#p, $extent($s, #x)) ==> $timestamp($s, #p) == $current_timestamp($s) && $mutable($s, #p));
    ensures (forall #p : $ptr :: { $select.mem($memory($s), #p) } #p == #x || ($set_in(#p, $full_extent(#x)) && (!$typed(old($s), #p) || !$typed($s, #p))) || $select.mem($memory(old($s)), #p) == $select.mem($memory($s), #p));
    ensures $ts_emb($select.tm($typemap(old($s)), #x)) == $ptr(^^root_emb, $ref(#x)) <==> $ts_emb($select.tm($typemap($s), #x)) == $ptr(^^root_emb, $ref(#x));
    ensures (forall #p : $ptr :: { $select.tm($typemap($s), #p) } $set_in(#p, $full_extent(#x)) || $select.tm($typemap($s), #p) == $select.tm($typemap(old($s)), #p));
    ensures (forall #p : $ptr :: { $select.sm($statusmap($s), #p) } $set_in(#p, $full_extent(#x)) || $select.sm($statusmap($s), #p) == $select.sm($statusmap(old($s)), #p));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

function $is_union_field($ctype, $field) returns (bool);
function $full_extent(#p:$ptr) returns ($ptrset);
function $extent(S:$state, #p:$ptr) returns ($ptrset);
function $span(#p:$ptr) returns ($ptrset);
function $first_option_typed(S:$state, #p:$ptr) returns (bool);
function $volatile_span(S:$state, #p:$ptr) returns ($ptrset);
axiom (forall S : $state, p : $ptr, q : $ptr :: { $set_in(p, $volatile_span(S, q)) } $set_in(p, $volatile_span(S, q)) <==> p == q || ($ts_is_volatile($select.tm($typemap(S), p)) && $set_in(p, $span(q))));
function $left_split(a:$ptr, i:int) returns ($ptr);
axiom (forall a : $ptr, i : int :: { $left_split(a, i) } $left_split(a, i) == $ptr($array($element_type($typ(a)), i), $ref(a)));
function $right_split(a:$ptr, i:int) returns ($ptr);
axiom (forall a : $ptr, i : int :: { $right_split(a, i) } $right_split(a, i) == $ptr($array($element_type($typ(a)), $array_length($typ(a)) - i), $ref($idx($ptr($element_type($typ(a)), $ref(a)), i, $element_type($typ(a))))));
function $joined_array(a1:$ptr, a2:$ptr) returns ($ptr);
axiom (forall a1 : $ptr, a2 : $ptr :: { $joined_array(a1, a2) } $joined_array(a1, a2) == $ptr($array($element_type($typ(a1)), $array_length($typ(a1)) + $array_length($typ(a2))), $ref(a1)));
procedure $split_array(a:$ptr, i:int) returns ();
    modifies $s;
    requires 0 < i;
    requires i < $array_length($typ(a));
    requires $ts_emb($select.tm($typemap($s), a)) == $ptr(^^root_emb, $ref(a));
    ensures $memory(old($s)) == $memory($s);
    ensures (forall p : $ptr :: { $select.sm($statusmap($s), p) } p == a || p == $left_split(a, i) || p == $right_split(a, i) || $select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p));
    ensures (forall p : $ptr :: { $select.tm($typemap($s), p) } p == a || p == $left_split(a, i) || p == $right_split(a, i) || $ts_emb($select.tm($typemap(old($s)), p)) == a || $select.tm($typemap(old($s)), p) == $select.tm($typemap($s), p));
    ensures ($extent_mutable($s, $left_split(a, i)) && $ts_emb($select.tm($typemap($s), $left_split(a, i))) == $ptr(^^root_emb, $ref($left_split(a, i))) && $timestamp($s, $left_split(a, i)) == $current_timestamp($s)) && $extent_mutable($s, $right_split(a, i)) && $ts_emb($select.tm($typemap($s), $right_split(a, i))) == $ptr(^^root_emb, $ref($right_split(a, i))) && $timestamp($s, $right_split(a, i)) == $current_timestamp($s);
    ensures $memory($s) == $memory(old($s));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

procedure $join_arrays(a1:$ptr, a2:$ptr) returns ();
    modifies $s;
    requires $ts_emb($select.tm($typemap($s), a1)) == $ptr(^^root_emb, $ref(a1));
    requires $ts_emb($select.tm($typemap($s), a2)) == $ptr(^^root_emb, $ref(a2));
    requires $element_type($typ(a1)) == $element_type($typ(a2));
    requires $ref($idx(a1, $array_length($typ(a1)), $element_type($typ(a1)))) == $ref(a2);
    ensures $memory(old($s)) == $memory($s);
    ensures (forall p : $ptr :: { $select.sm($statusmap($s), p) } p == $joined_array(a1, a2) || p == a1 || p == a2 || $select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p));
    ensures (forall p : $ptr :: { $select.tm($typemap($s), p) } p == $joined_array(a1, a2) || p == a1 || p == a2 || $ts_emb($select.tm($typemap(old($s)), p)) == a1 || $ts_emb($select.tm($typemap(old($s)), p)) == a2 || $select.tm($typemap(old($s)), p) == $select.tm($typemap($s), p));
    ensures $extent_mutable($s, $joined_array(a1, a2)) && $ts_emb($select.tm($typemap($s), $joined_array(a1, a2))) == $ptr(^^root_emb, $ref($joined_array(a1, a2))) && $timestamp($s, $joined_array(a1, a2)) == $current_timestamp($s);
    ensures $memory($s) == $memory(old($s));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

procedure $to_bytes(a:$ptr) returns ();
    modifies $s;
    requires $ts_emb($select.tm($typemap($s), a)) == $ptr(^^root_emb, $ref(a));
    ensures $extent_mutable($s, $ptr($array(^^u1, $sizeof($typ(a))), $ref(a))) && $ts_emb($select.tm($typemap($s), $ptr($array(^^u1, $sizeof($typ(a))), $ref(a)))) == $ptr(^^root_emb, $ref($ptr($array(^^u1, $sizeof($typ(a))), $ref(a)))) && $timestamp($s, $ptr($array(^^u1, $sizeof($typ(a))), $ref(a))) == $current_timestamp($s);
    ensures (forall p : $ptr :: { $select.sm($statusmap($s), p) } { $select.sm($statusmap($s), p) } ($set_in(p, $extent($s, $ptr($array(^^u1, $sizeof($typ(a))), $ref(a)))) ==> $timestamp($s, p) == $current_timestamp($s) && $mutable($s, p)) && ($set_in(p, $full_extent(a)) || $set_in(p, $extent($s, $ptr($array(^^u1, $sizeof($typ(a))), $ref(a)))) || ($select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p) && $select.tm($typemap(old($s)), p) == $select.tm($typemap($s), p))));
    ensures (forall p : $ptr :: { $select.mem($memory($s), p) } $set_in(p, $full_extent(a)) || $set_in(p, $full_extent($ptr($array(^^u1, $sizeof($typ(a))), $ref(a)))) || ($select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p) && $select.tm($typemap(old($s)), p) == $select.tm($typemap($s), p) && $select.mem($memory(old($s)), p) == $select.mem($memory($s), p)));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

procedure $from_bytes(a:$ptr, t:$ctype, preserve_zero:bool) returns ();
    modifies $s;
    requires $ts_emb($select.tm($typemap($s), a)) == $ptr(^^root_emb, $ref(a));
    requires $element_type($typ(a)) == ^^u1;
    requires $sizeof(t) <= $array_length($typ(a));
    requires preserve_zero ==> $extent_zero($s, a);
    ensures $extent_mutable($s, $ptr(t, $ref(a))) && $ts_emb($select.tm($typemap($s), $ptr(t, $ref(a)))) == $ptr(^^root_emb, $ref($ptr(t, $ref(a)))) && $timestamp($s, $ptr(t, $ref(a))) == $current_timestamp($s);
    ensures (forall p : $ptr :: { $select.sm($statusmap($s), p) } { $select.tm($typemap($s), p) } ($set_in(p, $extent($s, $ptr(t, $ref(a)))) ==> $timestamp($s, p) == $current_timestamp($s) && $mutable($s, p)) && ($set_in(p, $full_extent(a)) || $set_in(p, $extent($s, $ptr(t, $ref(a)))) || ($select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p) && $select.tm($typemap(old($s)), p) == $select.tm($typemap($s), p))));
    ensures (forall p : $ptr :: { $select.mem($memory($s), p) } $set_in(p, $full_extent(a)) || $set_in(p, $full_extent($ptr(t, $ref(a)))) || ($select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p) && $select.tm($typemap(old($s)), p) == $select.tm($typemap($s), p) && $select.mem($memory(old($s)), p) == $select.mem($memory($s), p)));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures preserve_zero ==> $extent_zero($s, $ptr(t, $ref(a)));

type $ptrset;
function $set_in($ptr, $ptrset) returns (bool);
function $set_empty() returns ($ptrset);
axiom (forall #o : $ptr :: { :weight 0 } { $set_in(#o, $set_empty()) } !$set_in(#o, $set_empty()));
function $set_singleton($ptr) returns ($ptrset);
axiom (forall #r : $ptr, #o : $ptr :: { :weight 0 } { $set_in(#o, $set_singleton(#r)) } $set_in(#o, $set_singleton(#r)) <==> #r == #o);
function $non_null_set_singleton($ptr) returns ($ptrset);
axiom (forall #r : $ptr, #o : $ptr :: { :weight 0 } { $set_in(#o, $non_null_set_singleton(#r)) } $set_in(#o, $non_null_set_singleton(#r)) <==> #r == #o && $ref(#r) != $ref($null));
function $set_union($ptrset, $ptrset) returns ($ptrset);
axiom (forall #a : $ptrset, #b : $ptrset, #o : $ptr :: { :weight 0 } { $set_in(#o, $set_union(#a, #b)) } $set_in(#o, $set_union(#a, #b)) <==> $set_in(#o, #a) || $set_in(#o, #b));
function $set_difference($ptrset, $ptrset) returns ($ptrset);
axiom (forall #a : $ptrset, #b : $ptrset, #o : $ptr :: { :weight 0 } { $set_in(#o, $set_difference(#a, #b)) } $set_in(#o, $set_difference(#a, #b)) <==> $set_in(#o, #a) && !$set_in(#o, #b));
function $set_intersection($ptrset, $ptrset) returns ($ptrset);
axiom (forall #a : $ptrset, #b : $ptrset, #o : $ptr :: { :weight 0 } { $set_in(#o, $set_intersection(#a, #b)) } $set_in(#o, $set_intersection(#a, #b)) <==> $set_in(#o, #a) && $set_in(#o, #b));
function $set_subset($ptrset, $ptrset) returns (bool);
axiom (forall #a : $ptrset, #b : $ptrset :: { :weight 0 } { $set_subset(#a, #b) } $set_subset(#a, #b) <==> (forall #o : $ptr :: { :weight 0 } { $set_in(#o, #a) } { $set_in(#o, #b) } $set_in(#o, #a) ==> $set_in(#o, #b)));
function $set_eq($ptrset, $ptrset) returns (bool);
axiom (forall #a : $ptrset, #b : $ptrset :: { :weight 0 } { $set_eq(#a, #b) } (forall #o : $ptr :: { :weight 0 } { $dont_instantiate(#o) } $set_in(#o, #a) <==> $set_in(#o, #b)) ==> $set_eq(#a, #b));
axiom (forall #a : $ptrset, #b : $ptrset :: { :weight 0 } { $set_eq(#a, #b) } $set_eq(#a, #b) ==> #a == #b);
function $set_cardinality($ptrset) returns (int);
axiom $set_cardinality($set_empty()) == 0;
axiom (forall p : $ptr :: { :weight 0 } $set_cardinality($set_singleton(p)) == 1);
function $set_universe() returns ($ptrset);
axiom (forall #o : $ptr :: { :weight 0 } { $set_in(#o, $set_universe()) } $set_in(#o, $set_universe()));
function $set_disjoint(s1:$ptrset, s2:$ptrset) returns (bool);
function $id_set_disjoint(p:$ptr, s1:$ptrset, s2:$ptrset) returns (int);
axiom (forall p : $ptr, s1 : $ptrset, s2 : $ptrset :: { :weight 0 } { $set_disjoint(s1, s2),$set_in(p, s1) } $set_disjoint(s1, s2) && $set_in(p, s1) ==> $id_set_disjoint(p, s1, s2) == 1);
axiom (forall p : $ptr, s1 : $ptrset, s2 : $ptrset :: { :weight 0 } { $set_disjoint(s1, s2),$set_in(p, s2) } $set_disjoint(s1, s2) && $set_in(p, s2) ==> $id_set_disjoint(p, s1, s2) == 2);
axiom (forall s1 : $ptrset, s2 : $ptrset :: { :weight 0 } { $set_disjoint(s1, s2) } (forall p : $ptr :: { $dont_instantiate(p) } ($set_in(p, s1) ==> !$set_in(p, s2)) && ($set_in(p, s2) ==> !$set_in(p, s1))) ==> $set_disjoint(s1, s2));
function $set_in3($ptr, $ptrset) returns (bool);
function $set_in2($ptr, $ptrset) returns (bool);
function $in_some_owns($ptr) returns (bool);
axiom (forall p : $ptr, S1 : $state, p1 : $ptr :: { :weight 0 } { $set_in(p, $owns(S1, p1)) } $set_in(p, $owns(S1, p1)) ==> $in_some_owns(p));
axiom (forall p : $ptr, S1 : $state, p1 : $ptr :: { :weight 0 } { $set_in2(p, $owns(S1, p1)),$in_some_owns(p) } $set_in(p, $owns(S1, p1)) <==> $set_in2(p, $owns(S1, p1)));
axiom (forall p : $ptr, s : $ptrset :: { :weight 0 } { $set_in(p, s) } $set_in(p, s) <==> $set_in2(p, s));
axiom (forall p : $ptr, s : $ptrset :: { :weight 0 } { $set_in(p, s) } $set_in(p, s) <==> $set_in3(p, s));
function $set_in0($ptr, $ptrset) returns (bool);
axiom (forall p : $ptr, s : $ptrset :: { :weight 0 } { $set_in0(p, s) } $set_in(p, s) <==> $set_in0(p, s));
function sk_hack(bool) returns (bool);
function $array($ctype, int) returns ($ctype);
function $element_type($ctype) returns ($ctype);
function $array_length($ctype) returns (int);
axiom (forall T : $ctype, s : int :: { $array(T, s) } $element_type($array(T, s)) == T);
axiom (forall T : $ctype, s : int :: { $array(T, s) } $array_length($array(T, s)) == s);
axiom (forall T : $ctype, s : int :: { $array(T, s) } $ptr_level($array(T, s)) == 0);
axiom (forall T : $ctype, s : int :: { $array(T, s) } $is_arraytype($array(T, s)));
axiom (forall T : $ctype, s : int :: { $array(T, s) } !$is_claimable($array(T, s)));
axiom (forall T : $ctype, s : int :: { $sizeof($array(T, s)) } $sizeof($array(T, s)) == $sizeof(T) * s);
function { :weight 0 } $inlined_array(p:$ptr, T:$ctype) returns ($ptr);
axiom (forall p : $ptr, T : $ctype :: { $inlined_array(p, T) } $inlined_array(p, T) == p);
function $idx($ptr, int, $ctype) returns ($ptr);
axiom (forall #p : $ptr, #i : int, #t : $ctype :: { $idx(#p, #i, #t) } $extent_hint($idx(#p, #i, #t), #p) && $idx(#p, #i, #t) == $ptr(#t, $ref(#p) + #i * $sizeof(#t)));
axiom (forall p : $ptr, i : int, j : int, T : $ctype :: { $idx($idx(p, i, T), j, T) } i != 0 && j != 0 ==> $idx($idx(p, i, T), j, T) == $idx(p, i + j, T));
function { :weight 0 } $is_array_vol_or_nonvol(S:$state, p:$ptr, T:$ctype, sz:int, vol:bool) returns (bool);
axiom (forall S : $state, p : $ptr, T : $ctype, sz : int, vol : bool :: { $is_array_vol_or_nonvol(S, p, T, sz, vol) } $is_array_vol_or_nonvol(S, p, T, sz, vol) == ($is(p, T) && (forall i : int :: { $select.sm($statusmap(S), $idx(p, i, T)) } { $select.tm($typemap(S), $idx(p, i, T)) } { $select.mem($memory(S), $idx(p, i, T)) } 0 <= i && i < sz ==> $ts_is_volatile($select.tm($typemap(S), $idx(p, i, T))) == vol && $typed(S, $idx(p, i, T)))));
function { :weight 0 } $is_array(S:$state, p:$ptr, T:$ctype, sz:int) returns (bool);
axiom (forall S : $state, p : $ptr, T : $ctype, sz : int :: { $is_array(S, p, T, sz) } $is_array(S, p, T, sz) == ($is(p, T) && (forall i : int :: { $select.sm($statusmap(S), $idx(p, i, T)) } { $select.tm($typemap(S), $idx(p, i, T)) } { $select.mem($memory(S), $idx(p, i, T)) } 0 <= i && i < sz ==> $typed(S, $idx(p, i, T)))));
axiom (forall p : $ptr, #r : int, T : $ctype, sz : int :: { $set_in(p, $full_extent($ptr($array(T, sz), #r))) } $set_in(p, $full_extent($ptr($array(T, sz), #r))) <==> p == $ptr($array(T, sz), #r) || ((0 <= $index_within(p, $ptr(T, #r)) && $index_within(p, $ptr(T, #r)) <= sz - 1) && $set_in(p, $full_extent($idx($ptr(T, #r), $index_within(p, $ptr(T, #r)), T)))));
axiom (forall S : $state, p : $ptr, #r : int, T : $ctype, sz : int :: { $set_in(p, $extent(S, $ptr($array(T, sz), #r))) } $set_in(p, $extent(S, $ptr($array(T, sz), #r))) <==> p == $ptr($array(T, sz), #r) || ((0 <= $index_within(p, $ptr(T, #r)) && $index_within(p, $ptr(T, #r)) <= sz - 1) && $set_in(p, $extent(S, $idx($ptr(T, #r), $index_within(p, $ptr(T, #r)), T)))));
axiom (forall S : $state, #r : int, T : $ctype, sz : int, i : int :: { $select.sm($statusmap(S), $idx($ptr(T, #r), i, T)),$ptr($array(T, sz), #r) } { $select.tm($typemap(S), $idx($ptr(T, #r), i, T)),$ptr($array(T, sz), #r) } $typed(S, $ptr($array(T, sz), #r)) ==> 0 <= i && i < sz ==> $ts_emb($select.tm($typemap(S), $idx($ptr($array(T, sz), #r), i, T))) == $ptr($array(T, sz), #r) && !$ts_is_volatile($select.tm($typemap(S), $idx($ptr($array(T, sz), #r), i, T))) && $typed(S, $idx($ptr($array(T, sz), #r), i, T)));
function $array_members(p:$ptr, T:$ctype, sz:int) returns ($ptrset);
axiom (forall p : $ptr, T : $ctype, sz : int, elem : $ptr :: { $set_in(elem, $array_members(p, T, sz)) } $set_in(elem, $array_members(p, T, sz)) <==> (0 <= $index_within(elem, p) && $index_within(elem, p) <= sz - 1) && elem == $idx(p, $index_within(elem, p), T));
function $array_range_no_state(p:$ptr, T:$ctype, sz:int) returns ($ptrset);
function $array_range(S:$state, p:$ptr, T:$ctype, sz:int) returns ($ptrset);
axiom (forall S : $state, p : $ptr, T : $ctype, sz : int :: { $array_range(S, p, T, sz) } $array_range(S, p, T, sz) == $array_range_no_state(p, T, sz));
axiom (forall S : $state, p : $ptr, #r : int, T : $ctype, sz : int :: { $set_in(p, $array_range(S, $ptr(T, #r), T, sz)) } $instantiate_bool($typed(S, p)) && ($set_in(p, $array_range(S, $ptr(T, #r), T, sz)) <==> (0 <= $index_within(p, $ptr(T, #r)) && $index_within(p, $ptr(T, #r)) <= sz - 1) && $set_in(p, $full_extent($idx($ptr(T, #r), $index_within(p, $ptr(T, #r)), T)))));
axiom (forall p : $ptr, T : $ctype, sz : int, idx : int, S : $ptrset :: { $idx(p, idx, T),$set_disjoint($array_range_no_state(p, T, sz), S) } $set_disjoint($array_range_no_state(p, T, sz), S) ==> 0 <= idx && idx < sz ==> $id_set_disjoint($idx(p, idx, T), $array_range_no_state(p, T, sz), S) == 1);
axiom (forall p : $ptr, T : $ctype, sz : int, idx : int, S : $ptrset :: { $idx(p, idx, T),$set_disjoint(S, $array_range_no_state(p, T, sz)) } $set_disjoint(S, $array_range_no_state(p, T, sz)) ==> 0 <= idx && idx < sz ==> $id_set_disjoint($idx(p, idx, T), S, $array_range_no_state(p, T, sz)) == 2);
function $non_null_array_range(p:$ptr, T:$ctype, sz:int) returns ($ptrset);
axiom (forall p : $ptr, #r : int, T : $ctype, sz : int :: { $set_in(p, $non_null_array_range($ptr(T, #r), T, sz)) } $set_in(p, $non_null_array_range($ptr(T, #r), T, sz)) <==> #r != 0 && (0 <= $index_within(p, $ptr(T, #r)) && $index_within(p, $ptr(T, #r)) <= sz - 1) && $set_in(p, $full_extent($idx($ptr(T, #r), $index_within(p, $ptr(T, #r)), T))));
function $non_null_extent(S:$state, p:$ptr) returns ($ptrset);
axiom (forall q : $ptr, S : $state, p : $ptr :: { $set_in(q, $non_null_extent(S, p)) } $set_in(q, $non_null_extent(S, p)) <==> $ref(p) != $ref($null) && $set_in(q, $extent(S, p)));
function $index_within(p:$ptr, arr:$ptr) returns (int);
function $simple_index(p:$ptr, arr:$ptr) returns (bool);
axiom (forall p : $ptr, k : int :: { $idx(p, k, $typ(p)) } $index_within($idx(p, k, $typ(p)), p) == k && $simple_index($idx(p, k, $typ(p)), p));
axiom (forall p : $ptr, q : $ptr, f : $field :: { $simple_index($dot(p, f), q) } { $index_within($dot(p, f), q) } $simple_index(p, q) ==> $simple_index($dot(p, f), q) && $index_within($dot(p, f), q) == $index_within(p, q));
axiom (forall p : $ptr, q : $ptr, f : $field, i : int, t : $ctype :: { $simple_index($idx($dot(p, f), i, t), q) } { $index_within($idx($dot(p, f), i, t), q) } 0 <= i && i < $embedded_array_size(f, t) && $simple_index(p, q) ==> $simple_index($idx($dot(p, f), i, t), q) && $index_within($idx($dot(p, f), i, t), q) == $index_within(p, q));
axiom (forall s1 : $state, s2 : $state, p : $ptr, t : $ctype, sz : int :: { $state_spans_the_same(s1, s2, p, $array(t, sz)),$is_primitive(t) } $is_primitive(t) ==> $state_spans_the_same(s1, s2, p, $array(t, sz)) ==> (forall i : int :: { $select.mem($memory(s2), $idx($ptr(t, $ref(p)), i, t)) } 0 <= i && i < sz ==> $select.mem($memory(s1), $idx($ptr(t, $ref(p)), i, t)) == $select.mem($memory(s2), $idx($ptr(t, $ref(p)), i, t))));
function { :weight 0 } $bool_id(x:bool) returns (bool);
axiom (forall x : bool :: { $bool_id(x) } $bool_id(x) == x);
const $min.i1 : int;
const $max.i1 : int;
const $min.i2 : int;
const $max.i2 : int;
const $min.i4 : int;
const $max.i4 : int;
const $min.i8 : int;
const $max.i8 : int;
const $max.u1 : int;
const $max.u2 : int;
const $max.u4 : int;
const $max.u8 : int;
axiom $min.i1 == -128;
axiom $max.i1 == 127;
axiom $min.i2 == -32768;
axiom $max.i2 == 32767;
axiom $min.i4 == -(65536 * 32768);
axiom $max.i4 == 65536 * 32768 - 1;
axiom $min.i8 == -(65536 * 65536 * 65536 * 32768);
axiom $max.i8 == 65536 * 65536 * 65536 * 32768 - 1;
axiom $max.u1 == 255;
axiom $max.u2 == 65535;
axiom $max.u4 == 65536 * 65536 - 1;
axiom $max.u8 == 65536 * 65536 * 65536 * 65536 - 1;
function $ptr_to_u8($ptr) returns (int);
function $ptr_to_i8($ptr) returns (int);
function $ptr_to_u4($ptr) returns (int);
function $ptr_to_i4($ptr) returns (int);
function $ptr_to_u2($ptr) returns (int);
function $ptr_to_i2($ptr) returns (int);
function $ptr_to_u1($ptr) returns (int);
function $ptr_to_i1($ptr) returns (int);
axiom $ptr_to_u8($null) == 0;
axiom $ptr_to_i8($null) == 0;
axiom $ptr_to_u4($null) == 0;
axiom $ptr_to_i4($null) == 0;
axiom $ptr_to_u2($null) == 0;
axiom $ptr_to_i2($null) == 0;
axiom $ptr_to_u1($null) == 0;
axiom $ptr_to_i1($null) == 0;
axiom (forall p : $ptr :: { $ptr_to_u8(p) } 0 <= $ref(p) && $ref(p) <= $max.u8 ==> $ptr_to_u8(p) == $ref(p));
axiom (forall p : $ptr :: { $ptr_to_i8(p) } $min.i8 <= $ref(p) && $ref(p) <= $max.i8 ==> $ptr_to_i8(p) == $ref(p));
axiom (forall p : $ptr :: { $ptr_to_u4(p) } 0 <= $ref(p) && $ref(p) <= $max.u4 ==> $ptr_to_u4(p) == $ref(p));
axiom (forall p : $ptr :: { $ptr_to_i4(p) } $min.i4 <= $ref(p) && $ref(p) <= $max.i4 ==> $ptr_to_i4(p) == $ref(p));
axiom (forall p : $ptr :: { $ptr_to_u2(p) } 0 <= $ref(p) && $ref(p) <= $max.u2 ==> $ptr_to_u2(p) == $ref(p));
axiom (forall p : $ptr :: { $ptr_to_i2(p) } $min.i2 <= $ref(p) && $ref(p) <= $max.i2 ==> $ptr_to_i2(p) == $ref(p));
axiom (forall p : $ptr :: { $ptr_to_u1(p) } 0 <= $ref(p) && $ref(p) <= $max.u1 ==> $ptr_to_u1(p) == $ref(p));
axiom (forall p : $ptr :: { $ptr_to_i1(p) } $min.i1 <= $ref(p) && $ref(p) <= $max.i1 ==> $ptr_to_i1(p) == $ref(p));
function { :weight 0 } $byte_ptr_subtraction(p1:$ptr, p2:$ptr) returns (int);
axiom (forall p1 : $ptr, p2 : $ptr :: { $byte_ptr_subtraction(p1, p2) } $byte_ptr_subtraction(p1, p2) == $ref(p1) - $ref(p2));
axiom (forall S : $state, r : int, t : $ctype :: { $select.mem($memory(S), $ptr($as_in_range_t(t), r)) } $good_state(S) ==> $in_range_t(t, $select.mem($memory(S), $ptr($as_in_range_t(t), r))));
axiom (forall S : $state, r : int, t : $ctype :: { $select.mem($memory(S), $ptr($ptr_to(t), r)) } $good_state(S) ==> $in_range_phys_ptr($select.mem($memory(S), $ptr($ptr_to(t), r))));
axiom (forall S : $state, r : int, t : $ctype :: { $select.mem($memory(S), $ptr($spec_ptr_to(t), r)) } $good_state(S) ==> $in_range_spec_ptr($select.mem($memory(S), $ptr($spec_ptr_to(t), r))));
function $_pow2(int) returns (int);
axiom $_pow2(0) == 1 && $_pow2(1) == 2 && $_pow2(2) == 4 && $_pow2(3) == 8 && $_pow2(4) == 16 && $_pow2(5) == 32 && $_pow2(6) == 64 && $_pow2(7) == 128 && $_pow2(8) == 256 && $_pow2(9) == 512 && $_pow2(10) == 1024 && $_pow2(11) == 2048 && $_pow2(12) == 4096 && $_pow2(13) == 8192 && $_pow2(14) == 16384 && $_pow2(15) == 32768 && $_pow2(16) == 65536 && $_pow2(17) == 131072 && $_pow2(18) == 262144 && $_pow2(19) == 524288 && $_pow2(20) == 1048576 && $_pow2(21) == 2097152 && $_pow2(22) == 4194304 && $_pow2(23) == 8388608 && $_pow2(24) == 16777216 && $_pow2(25) == 33554432 && $_pow2(26) == 67108864 && $_pow2(27) == 134217728 && $_pow2(28) == 268435456 && $_pow2(29) == 536870912 && $_pow2(30) == 1073741824 && $_pow2(31) == 2147483648 && $_pow2(32) == 4294967296 && $_pow2(33) == 8589934592 && $_pow2(34) == 17179869184 && $_pow2(35) == 34359738368 && $_pow2(36) == 68719476736 && $_pow2(37) == 137438953472 && $_pow2(38) == 274877906944 && $_pow2(39) == 549755813888 && $_pow2(40) == 1099511627776 && $_pow2(41) == 2199023255552 && $_pow2(42) == 4398046511104 && $_pow2(43) == 8796093022208 && $_pow2(44) == 17592186044416 && $_pow2(45) == 35184372088832 && $_pow2(46) == 70368744177664 && $_pow2(47) == 140737488355328 && $_pow2(48) == 281474976710656 && $_pow2(49) == 562949953421312 && $_pow2(50) == 1125899906842624 && $_pow2(51) == 2251799813685248 && $_pow2(52) == 4503599627370496 && $_pow2(53) == 9007199254740992 && $_pow2(54) == 18014398509481984 && $_pow2(55) == 36028797018963968 && $_pow2(56) == 72057594037927936 && $_pow2(57) == 144115188075855872 && $_pow2(58) == 288230376151711744 && $_pow2(59) == 576460752303423488 && $_pow2(60) == 1152921504606846976 && $_pow2(61) == 2305843009213693952 && $_pow2(62) == 4611686018427387904 && $_pow2(63) == 9223372036854775808;
function $in_range_ubits(bits:int, v:int) returns (bool);
axiom (forall bits : int, v : int :: { $in_range_ubits(bits, v) } $in_range_ubits(bits, v) == (0 <= v && v <= $_pow2(bits) - 1));
function $unchecked_sbits(bits:int, v:int) returns (int);
axiom (forall bits : int, v : int :: { $unchecked_sbits(bits, v) } $in_range_sbits(bits, $unchecked_sbits(bits, v)) && ($in_range_sbits(bits, v) ==> $unchecked_sbits(bits, v) == v));
function $in_range_sbits(bits:int, v:int) returns (bool);
axiom (forall bits : int, v : int :: { $in_range_sbits(bits, v) } $in_range_sbits(bits, v) == (-$_pow2(bits - 1) <= v && v <= $_pow2(bits - 1) - 1));
function $unchecked_ubits(bits:int, v:int) returns (int);
axiom (forall bits : int, v : int :: { $unchecked_ubits(bits, v) } $in_range_ubits(bits, $unchecked_ubits(bits, v)) && ($in_range_ubits(bits, v) ==> $unchecked_ubits(bits, v) == v));
function $_or(t:$ctype, x:int, y:int) returns (int);
function $_xor(t:$ctype, x:int, y:int) returns (int);
function $_and(t:$ctype, x:int, y:int) returns (int);
function $_not(t:$ctype, x:int) returns (int);
function { :weight 0 } $unchk_add(t:$ctype, x:int, y:int) returns (int);
axiom (forall t : $ctype, x : int, y : int :: { $unchk_add(t, x, y) } $unchk_add(t, x, y) == $unchecked(t, x + y));
function { :weight 0 } $unchk_sub(t:$ctype, x:int, y:int) returns (int);
axiom (forall t : $ctype, x : int, y : int :: { $unchk_sub(t, x, y) } $unchk_sub(t, x, y) == $unchecked(t, x - y));
function { :weight 0 } $unchk_mul(t:$ctype, x:int, y:int) returns (int);
axiom (forall t : $ctype, x : int, y : int :: { $unchk_mul(t, x, y) } $unchk_mul(t, x, y) == $unchecked(t, x * y));
function { :weight 0 } $unchk_div(t:$ctype, x:int, y:int) returns (int);
axiom (forall t : $ctype, x : int, y : int :: { $unchk_div(t, x, y) } $unchk_div(t, x, y) == $unchecked(t, x / y));
function { :weight 0 } $unchk_mod(t:$ctype, x:int, y:int) returns (int);
axiom (forall t : $ctype, x : int, y : int :: { $unchk_mod(t, x, y) } $unchk_mod(t, x, y) == $unchecked(t, x % y));
function { :weight 0 } $_shl(t:$ctype, x:int, y:int) returns (int);
axiom (forall t : $ctype, x : int, y : int :: { $_shl(t, x, y) } $_shl(t, x, y) == $unchecked(t, x * $_pow2(y)));
function { :weight 0 } $_shr(x:int, y:int) returns (int);
axiom (forall x : int, y : int :: { $_shr(x, y) } $_shr(x, y) == x / $_pow2(y));
function $bv_extract_signed(val:int, val_bitsize:int, from:int, to:int) returns (int);
function $bv_extract_unsigned(val:int, val_bitsize:int, from:int, to:int) returns (int);
function $bv_update(val:int, val_bitsize:int, from:int, to:int, repl:int) returns (int);
axiom (forall x : int, from : int, to : int, xs : int, val : int :: { $bv_update(x, xs, from, to, val) } 0 <= from && from < to && to <= xs ==> 0 <= val && val < $_pow2(to - from) ==> 0 <= $bv_update(x, xs, from, to, val) && $bv_update(x, xs, from, to, val) < $_pow2(xs));
axiom (forall from : int, to : int, xs : int :: { $bv_update(0, xs, from, to, 0) } 0 <= from && from < to && to <= xs ==> $bv_update(0, xs, from, to, 0) == 0);
axiom (forall from : int, to : int, val : int, x : int, xs : int :: { $bv_extract_signed($bv_update(x, xs, from, to, val), xs, from, to) } 0 <= from && from < to && to <= xs ==> -$_pow2(to - from - 1) <= val && val < $_pow2(to - from - 1) ==> $bv_extract_signed($bv_update(x, xs, from, to, val), xs, from, to) == val);
axiom (forall from : int, to : int, val : int, x : int, xs : int :: { $bv_extract_unsigned($bv_update(x, xs, from, to, val), xs, from, to) } 0 <= from && from < to && to <= xs ==> 0 <= val && val < $_pow2(to - from) ==> $bv_extract_unsigned($bv_update(x, xs, from, to, val), xs, from, to) == val);
axiom (forall from : int, to : int, x : int, xs : int :: { $bv_extract_signed(x, xs, from, to) } 0 <= from && from < to && to <= xs ==> -$_pow2(to - from - 1) <= $bv_extract_signed(x, xs, from, to) && $bv_extract_signed(x, xs, from, to) <= $_pow2(to - from - 1) - 1);
axiom (forall from : int, to : int, x : int, xs : int :: { $bv_extract_unsigned(x, xs, from, to) } 0 <= from && from < to && to <= xs ==> 0 <= $bv_extract_unsigned(x, xs, from, to) && $bv_extract_unsigned(x, xs, from, to) <= $_pow2(to - from) - 1);
axiom (forall from : int, to : int, val : int, x : int, xs : int, from2 : int, to2 : int :: { $bv_extract_signed($bv_update(x, xs, from, to, val), xs, from2, to2) } 0 <= from && from < to && to <= xs ==> 0 <= from2 && from2 < to2 && to2 <= xs ==> to2 <= from || to <= from2 ==> $bv_extract_signed($bv_update(x, xs, from, to, val), xs, from2, to2) == $bv_extract_signed(x, xs, from2, to2));
axiom (forall from : int, to : int, val : int, x : int, xs : int, from2 : int, to2 : int :: { $bv_extract_unsigned($bv_update(x, xs, from, to, val), xs, from2, to2) } 0 <= from && from < to && to <= xs ==> 0 <= from2 && from2 < to2 && to2 <= xs ==> to2 <= from || to <= from2 ==> $bv_extract_unsigned($bv_update(x, xs, from, to, val), xs, from2, to2) == $bv_extract_unsigned(x, xs, from2, to2));
axiom (forall from : int, to : int, xs : int :: { $bv_extract_signed(0, xs, from, to) } 0 <= from && from < to && to <= xs ==> $bv_extract_signed(0, xs, from, to) == 0);
axiom (forall from : int, to : int, xs : int :: { $bv_extract_unsigned(0, xs, from, to) } 0 <= from && from < to && to <= xs ==> $bv_extract_unsigned(0, xs, from, to) == 0);
axiom (forall from : int, to : int, val : int, xs : int :: { $bv_extract_unsigned(val, xs, from, to) } 0 <= from && from < to && to <= xs && 0 <= val ==> $bv_extract_unsigned(val, xs, from, to) == val / $_pow2(from) % $_pow2(to - from));
axiom (forall from : int, to : int, val : int, xs : int :: { $bv_extract_signed(val, xs, from, to) } 0 <= from && from < to && to <= xs && 0 <= val && val / $_pow2(from) % $_pow2(to - from) < $_pow2(to - from - 1) ==> $bv_extract_signed(val, xs, from, to) == val / $_pow2(from) % $_pow2(to - from));
axiom (forall from : int, to : int, val : int, xs : int :: { $bv_extract_signed(val, xs, from, to) } 0 <= from && from < to && to <= xs && 0 <= val && val / $_pow2(from) % $_pow2(to - from) >= $_pow2(to - from - 1) ==> $bv_extract_signed(val, xs, from, to) == $_pow2(to - from - 1) - val / $_pow2(from) % $_pow2(to - from));
function $unchecked(t:$ctype, val:int) returns (int);
function $in_range_t(t:$ctype, x:int) returns (bool);
axiom (forall val : int :: { $in_range_t(^^i1, val) } $in_range_t(^^i1, val) <==> $min.i1 <= val && val <= $max.i1);
axiom (forall val : int :: { $in_range_t(^^i2, val) } $in_range_t(^^i2, val) <==> $min.i2 <= val && val <= $max.i2);
axiom (forall val : int :: { $in_range_t(^^i4, val) } $in_range_t(^^i4, val) <==> $min.i4 <= val && val <= $max.i4);
axiom (forall val : int :: { $in_range_t(^^i8, val) } $in_range_t(^^i8, val) <==> $min.i8 <= val && val <= $max.i8);
axiom (forall val : int :: { $in_range_t(^^u1, val) } $in_range_t(^^u1, val) <==> 0 <= val && val <= $max.u1);
axiom (forall val : int :: { $in_range_t(^^u2, val) } $in_range_t(^^u2, val) <==> 0 <= val && val <= $max.u2);
axiom (forall val : int :: { $in_range_t(^^u4, val) } $in_range_t(^^u4, val) <==> 0 <= val && val <= $max.u4);
axiom (forall val : int :: { $in_range_t(^^u8, val) } $in_range_t(^^u8, val) <==> 0 <= val && val <= $max.u8);
axiom (forall val : int :: { $in_range_t(^^mathint, val) } $in_range_t(^^mathint, val));
axiom (forall t : $ctype, val : int :: { $unchecked(t, val) } $in_range_t(t, val) ==> $unchecked(t, val) == val);
axiom (forall t : $ctype, val : int :: { $unchecked(t, val) } $in_range_t(t, $unchecked(t, val)));
axiom (forall val : int :: { $unchecked(^^u1, $unchecked(^^i1, val)) } 0 <= val && val <= $max.u1 ==> $unchecked(^^u1, $unchecked(^^i1, val)) == val);
axiom (forall val : int :: { $unchecked(^^u2, $unchecked(^^i2, val)) } 0 <= val && val <= $max.u2 ==> $unchecked(^^u2, $unchecked(^^i2, val)) == val);
axiom (forall val : int :: { $unchecked(^^u4, $unchecked(^^i4, val)) } 0 <= val && val <= $max.u4 ==> $unchecked(^^u4, $unchecked(^^i4, val)) == val);
axiom (forall val : int :: { $unchecked(^^u8, $unchecked(^^i8, val)) } 0 <= val && val <= $max.u8 ==> $unchecked(^^u8, $unchecked(^^i8, val)) == val);
axiom (forall val : int :: { $unchecked(^^i1, $unchecked(^^u1, val)) } $min.i1 <= val && val <= $max.i1 ==> $unchecked(^^i1, $unchecked(^^u1, val)) == val);
axiom (forall val : int :: { $unchecked(^^i2, $unchecked(^^u2, val)) } $min.i2 <= val && val <= $max.i2 ==> $unchecked(^^i2, $unchecked(^^u2, val)) == val);
axiom (forall val : int :: { $unchecked(^^i4, $unchecked(^^u4, val)) } $min.i4 <= val && val <= $max.i4 ==> $unchecked(^^i4, $unchecked(^^u4, val)) == val);
axiom (forall val : int :: { $unchecked(^^i8, $unchecked(^^u8, val)) } $min.i8 <= val && val <= $max.i8 ==> $unchecked(^^i8, $unchecked(^^u8, val)) == val);
axiom (forall t : $ctype, x : int, y : int, z : int :: { x % $_pow2(y),$_and(t, x, z) } $in_range_t(t, x) && $in_range_t(t, $_pow2(y) - 1) && x >= 0 ==> x % $_pow2(y) == $_and(t, x, $_pow2(y) - 1));
axiom (forall i : int, j : int :: { i / j } 0 <= i && 0 < j ==> i / j <= i);
axiom (forall i : int, j : int :: { i / j } i > 0 && j > 0 ==> i - j < i / j * j && i / j * j <= i);
axiom (forall i : int :: { i / i } i != 0 ==> i / i == 1);
axiom (forall i : int :: { 0 / i } i != 0 ==> 0 / i == 0);
axiom (forall x : int, y : int :: { x % y } { x / y } x % y == x - x / y * y);
axiom (forall x : int, y : int :: { x % y } 0 <= x && 0 < y ==> 0 <= x % y && x % y < y);
axiom (forall x : int, y : int :: { x % y } 0 <= x && y < 0 ==> 0 <= x % y && x % y < 0 - y);
axiom (forall x : int, y : int :: { x % y } x <= 0 && 0 < y ==> 0 - y < x % y && x % y <= 0);
axiom (forall x : int, y : int :: { x % y } x <= 0 && y < 0 ==> y < x % y && x % y <= 0);
axiom (forall t : $ctype, x : int, y : int :: { $_and(t, x, y) } 0 <= x && $in_range_t(t, x) ==> 0 <= $_and(t, x, y) && $_and(t, x, y) <= x);
axiom (forall t : $ctype, x : int, y : int :: { $_and(t, x, y) } 0 <= x && 0 <= y && $in_range_t(t, x) && $in_range_t(t, y) ==> $_and(t, x, y) <= x && $_and(t, x, y) <= y);
axiom (forall t : $ctype, x : int, y : int :: { $_or(t, x, y) } 0 <= x && 0 <= y && $in_range_t(t, x) && $in_range_t(t, y) ==> 0 <= $_or(t, x, y) && $_or(t, x, y) <= x + y);
axiom (forall t : $ctype, x : int, y : int :: { $_or(t, x, y) } 0 <= x && 0 <= y && $in_range_t(t, x) && $in_range_t(t, y) ==> x <= $_or(t, x, y) && y <= $_or(t, x, y));
axiom (forall t : $ctype, x : int, y : int, z : int :: { $_or(t, x, y),$_pow2(z) } 0 <= x && 0 <= y && 0 <= z && z < 64 && x < $_pow2(z) && y < $_pow2(z) && $in_range_t(t, x) && $in_range_t(t, y) ==> $_or(t, x, y) < $_pow2(z));
axiom (forall t : $ctype, x : int, y : int :: { $_or(t, x, y) } (0 <= x && x <= $max.u1) && 0 <= y && y <= $max.u1 ==> 0 <= $_or(t, x, y) && $_or(t, x, y) <= $max.u1);
axiom (forall t : $ctype, x : int, y : int :: { $_or(t, x, y) } (0 <= x && x <= $max.u2) && 0 <= y && y <= $max.u2 ==> 0 <= $_or(t, x, y) && $_or(t, x, y) <= $max.u2);
axiom (forall t : $ctype, x : int, y : int :: { $_or(t, x, y) } (0 <= x && x <= $max.u4) && 0 <= y && y <= $max.u4 ==> 0 <= $_or(t, x, y) && $_or(t, x, y) <= $max.u4);
axiom (forall t : $ctype, x : int, y : int :: { $_or(t, x, y) } (0 <= x && x <= $max.u8) && 0 <= y && y <= $max.u8 ==> 0 <= $_or(t, x, y) && $_or(t, x, y) <= $max.u8);
axiom (forall t : $ctype, x : int, y : int :: { $_and(t, x, y) } (0 <= x && x <= $max.u1) && 0 <= y && y <= $max.u1 ==> 0 <= $_and(t, x, y) && $_and(t, x, y) <= $max.u1);
axiom (forall t : $ctype, x : int, y : int :: { $_and(t, x, y) } (0 <= x && x <= $max.u2) && 0 <= y && y <= $max.u2 ==> 0 <= $_and(t, x, y) && $_and(t, x, y) <= $max.u2);
axiom (forall t : $ctype, x : int, y : int :: { $_and(t, x, y) } (0 <= x && x <= $max.u4) && 0 <= y && y <= $max.u4 ==> 0 <= $_and(t, x, y) && $_and(t, x, y) <= $max.u4);
axiom (forall t : $ctype, x : int, y : int :: { $_and(t, x, y) } (0 <= x && x <= $max.u8) && 0 <= y && y <= $max.u8 ==> 0 <= $_and(t, x, y) && $_and(t, x, y) <= $max.u8);
axiom (forall t : $ctype, x : int, y : int :: { $_xor(t, x, y) } (0 <= x && x <= $max.u1) && 0 <= y && y <= $max.u1 ==> 0 <= $_xor(t, x, y) && $_xor(t, x, y) <= $max.u1);
axiom (forall t : $ctype, x : int, y : int :: { $_xor(t, x, y) } (0 <= x && x <= $max.u2) && 0 <= y && y <= $max.u2 ==> 0 <= $_xor(t, x, y) && $_xor(t, x, y) <= $max.u2);
axiom (forall t : $ctype, x : int, y : int :: { $_xor(t, x, y) } (0 <= x && x <= $max.u4) && 0 <= y && y <= $max.u4 ==> 0 <= $_xor(t, x, y) && $_xor(t, x, y) <= $max.u4);
axiom (forall t : $ctype, x : int, y : int :: { $_xor(t, x, y) } (0 <= x && x <= $max.u8) && 0 <= y && y <= $max.u8 ==> 0 <= $_xor(t, x, y) && $_xor(t, x, y) <= $max.u8);
axiom (forall t : $ctype, x : int :: { $_not(t, x) } $in_range_t(t, $_not(t, x)));
axiom (forall t : $ctype, x : int :: { $_or(t, x, $_not(t, x)) } $_or(t, x, $_not(t, x)) == $_not(t, 0));
axiom (forall t : $ctype, x : int :: { $_and(t, x, $_not(t, x)) } $_and(t, x, $_not(t, x)) == 0);
axiom (forall t : $ctype, x : int :: { $_or(t, x, 0) } $in_range_t(t, x) ==> $_or(t, x, 0) == x);
axiom (forall t : $ctype, x : int :: { $_or(t, x, $_not(t, 0)) } $_or(t, x, $_not(t, 0)) == $_not(t, 0));
axiom (forall t : $ctype, x : int :: { $_or(t, x, x) } $in_range_t(t, x) ==> $_or(t, x, x) == x);
axiom (forall t : $ctype, x : int :: { $_and(t, x, 0) } $_and(t, x, 0) == 0);
axiom (forall t : $ctype, x : int :: { $_and(t, x, $_not(t, 0)) } $in_range_t(t, x) ==> $_and(t, x, $_not(t, 0)) == x);
axiom (forall t : $ctype, x : int :: { $_and(t, x, x) } $in_range_t(t, x) ==> $_and(t, x, x) == x);
axiom (forall t : $ctype, x : int, y : int :: { $_and(t, $_or(t, x, y), y) } $_and(t, $_or(t, x, y), y) == y);
axiom (forall t : $ctype, x : int, y : int :: { $_and(t, $_or(t, x, y), x) } $_and(t, $_or(t, x, y), x) == x);
axiom (forall t : $ctype, x : int :: { $_xor(t, x, 0) } $in_range_t(t, x) ==> $_xor(t, x, 0) == x);
axiom (forall t : $ctype, x : int :: { $_xor(t, x, x) } $_xor(t, x, x) == 0);
axiom (forall t : $ctype, x : int :: { $_xor(t, x, $_not(t, 0)) } $_xor(t, x, $_not(t, 0)) == $_not(t, x));
axiom (forall t : $ctype, x : int :: { $_not(t, $_not(t, x)) } $in_range_t(t, x) ==> $_not(t, $_not(t, x)) == x);
axiom (forall t : $ctype, x : int, y : int :: { $_or(t, x, y) } $_or(t, x, y) == $_or(t, y, x));
axiom (forall t : $ctype, x : int, y : int :: { $_xor(t, x, y) } $_xor(t, x, y) == $_xor(t, y, x));
axiom (forall t : $ctype, x : int, y : int :: { $_and(t, x, y) } $_and(t, x, y) == $_and(t, y, x));
function { :weight 0 } $_mul(x:int, y:int) returns (int);
axiom (forall x : int, y : int :: { $_mul(x, y) } $_mul(x, y) == x * y);
function $get_string_literal(id:int, length:int) returns ($ptr);
axiom (forall id : int, length : int :: { $get_string_literal(id, length) } $is($get_string_literal(id, length), ^^u1));
axiom (forall id : int, length : int, S : $state :: { $typed(S, $get_string_literal(id, length)) } { $is_array(S, $get_string_literal(id, length), ^^u1, length) } $good_state(S) ==> $typed(S, $get_string_literal(id, length)) && (forall i : int :: { $select.sm($statusmap(S), $idx($get_string_literal(id, length), i, ^^u1)) } { $select.tm($typemap(S), $idx($get_string_literal(id, length), i, ^^u1)) } 0 <= i && i < length ==> $is($idx($get_string_literal(id, length), i, ^^u1), ^^u1) && $thread_local(S, $idx($get_string_literal(id, length), i, ^^u1))));
function $get_fnptr(no:int, t:$ctype) returns ($ptr);
axiom (forall no : int, t : $ctype :: { $get_fnptr(no, t) } $get_fnptr(no, t) == $ptr(t, $get_fnptr_ref(no)));
function $get_fnptr_ref(no:int) returns (int);
function $get_fnptr_inv(rf:int) returns (int);
axiom (forall no : int :: $get_fnptr_inv($get_fnptr_ref(no)) == no);
axiom (forall S : $state, no : int, t : $ctype :: { $select.tm($typemap(S), $get_fnptr(no, t)) } { $select.sm($statusmap(S), $get_fnptr(no, t)) } $is_fnptr_type(t) && $good_state(S) ==> $mutable(S, $get_fnptr(no, t)));
function $is_fnptr_type(t:$ctype) returns (bool);
function $is_math_type(t:$ctype) returns (bool);
axiom (forall t : $ctype :: { $is_math_type(t) } $is_math_type(t) ==> $is_primitive(t));
axiom (forall t : $ctype :: { $is_fnptr_type(t) } $is_fnptr_type(t) ==> $is_primitive(t));
function $claims_obj(claim:$ptr, obj:$ptr) returns (bool);
function $valid_claim(S:$state, claim:$ptr) returns (bool);
axiom (forall S : $state, c : $ptr :: { $full_stop(S),$valid_claim(S, c) } $full_stop(S) && $closed(S, c) ==> $valid_claim(S, c));
axiom (forall S : $state, c : $ptr :: { $valid_claim(S, c) } $valid_claim(S, c) ==> $closed(S, c) && $invok_state(S));
function $claims_claim(c1:$ptr, c2:$ptr) returns (bool);
axiom (forall c1 : $ptr, c2 : $ptr :: { $claims_claim(c1, c2) } $is(c1, ^^claim) && $is(c2, ^^claim) && (forall S : $state :: $valid_claim(S, c1) ==> $closed(S, c2)) ==> $claims_claim(c1, c2));
axiom (forall S : $state, c1 : $ptr, c2 : $ptr :: { $valid_claim(S, c1),$claims_claim(c1, c2) } $valid_claim(S, c1) && $claims_claim(c1, c2) ==> $valid_claim(S, c2));
axiom (forall S : $state, c : $ptr, o : $ptr :: { $closed(S, c),$claims_obj(c, o) } $good_state(S) ==> $claims_obj(c, o) && $closed(S, c) ==> $instantiate_ptrset($owns(S, o)) && $closed(S, o) && $ref_cnt(S, o) > 0);
axiom (forall S : $state, c : $ptr, o : $ptr :: { $valid_claim(S, c),$claims_obj(c, o) } $valid_claim(S, c) && $claims_obj(c, o) ==> $inv2(S, S, o, $typ(o)));
axiom (forall S : $state, c : $ptr, r : int :: { $valid_claim(S, c),$claims_obj(c, $ptr(^^claim, r)) } $valid_claim(S, c) && $claims_obj(c, $ptr(^^claim, r)) ==> $valid_claim(S, $ptr(^^claim, r)));
function { :weight 0 } $not_shared(S:$state, p:$ptr) returns (bool);
axiom (forall S : $state, p : $ptr :: { $not_shared(S, p) } $not_shared(S, p) == (($closed(S, p) && $owner(S, p) == $me() && ($is(p, $typ(p)) && $typed(S, p)) && $kind_of($typ(p)) != $kind_primitive && $is_non_primitive($typ(p))) && (!$is_claimable($typ(p)) || $ref_cnt(S, p) == 0)));
function { :weight 0 } $claimed_closed(s:$state, p:$ptr) returns (bool);
axiom (forall s : $state, p : $ptr :: { $claimed_closed(s, p) } $claimed_closed(s, p) == $closed(s, p));
axiom (forall S : $state, p : $ptr :: { $invok_state(S),$claimed_closed(S, p) } $invok_state(S) && $claimed_closed(S, p) ==> $inv2(S, S, p, $typ(p)));
procedure $atomic_havoc() returns ();
    modifies $s;
    ensures (forall p : $ptr :: { $select.sm($statusmap($s), p) } $kind_of($typ($owner($s, p))) != $kind_thread ==> $kind_of($typ($owner(old($s), p))) != $kind_thread) && (forall p : $ptr :: { $select.mem($memory($s), p) } $thread_local(old($s), p) ==> $select.mem($memory(old($s)), p) == $select.mem($memory($s), p) && $thread_local($s, p)) && (forall p : $ptr :: { $select.sm($statusmap($s), p) } $thread_local(old($s), p) ==> $select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p) && $thread_local($s, p)) && (forall p : $ptr :: { $select.tm($typemap($s), p) } $thread_local(old($s), p) ==> $select.tm($typemap(old($s)), p) == $select.tm($typemap($s), p) && $thread_local($s, p)) && $current_timestamp(old($s)) <= $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures (forall r : int, t : $ctype, f : $field :: { $is_thread_local_storage(t),$select.mem($memory($s), $dot($ptr(t, r), f)) } $is_thread_local_storage(t) && $owner(old($s), $ptr(t, r)) == $me() ==> $select.mem($memory(old($s)), $dot($ptr(t, r), f)) == $select.mem($memory($s), $dot($ptr(t, r), f)));
    ensures (forall r : int, t : $ctype, f : $field, i : int, sz : int, t2 : $ctype :: { $is_thread_local_storage(t),$is_primitive_embedded_volatile_array(f, sz, t2),$select.mem($memory($s), $idx($dot($ptr(t, r), f), i, t2)) } $is_thread_local_storage(t) && $is_primitive_embedded_volatile_array(f, sz, t2) && 0 <= i && i < sz && $owner(old($s), $ptr(t, r)) == $me() ==> $select.mem($memory(old($s)), $idx($dot($ptr(t, r), f), i, t2)) == $select.mem($memory($s), $idx($dot($ptr(t, r), f), i, t2)));
    ensures (forall p : $ptr, f : $field :: { $not_shared(old($s), p),$select.mem($memory($s), $dot(p, f)) } $not_shared(old($s), p) ==> $select.mem($memory(old($s)), $dot(p, f)) == $select.mem($memory($s), $dot(p, f)));
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);

const $no_claim : $ptr;
axiom $no_claim == $ptr(^^claim, 0);
procedure $alloc_claim() returns (#r:$ptr);
    modifies $s;
    ensures $owns($s, #r) == $set_empty();
    ensures $memory($s) == $memory(old($s));
    ensures $typemap($s) == $typemap(old($s));
    ensures (forall p : $ptr :: { $select.sm($statusmap($s), p) } p == #r || $select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p));
    ensures $closed($s, #r) && $owner($s, #r) == $me() && ($is(#r, ^^claim) && $typed($s, #r)) && $kind_of(^^claim) != $kind_primitive && $is_non_primitive(^^claim);
    ensures $current_timestamp(old($s)) < $timestamp($s, #r) && $timestamp($s, #r) <= $current_timestamp($s);
    ensures $in_range_spec_ptr($ref(#r));
    ensures $ref_cnt($s, #r) == 0;
    ensures !$closed(old($s), #r) && $owner(old($s), #r) != $me();
    ensures $current_timestamp(old($s)) < $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures #r != $no_claim;

procedure $unclaim(c:$ptr) returns ();
    modifies $s;
    requires $closed($s, c) && $owner($s, c) == $me() && ($is(c, ^^claim) && $typed($s, c)) && $kind_of(^^claim) != $kind_primitive && $is_non_primitive(^^claim);
    requires $ref_cnt($s, c) == 0;
    ensures (forall p : $ptr :: { $select.sm($statusmap($s), p) } $select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p) || p == c);
    ensures $typemap(old($s)) == $typemap($s);
    ensures $memory(old($s)) == $memory($s);
    ensures $current_timestamp(old($s)) <= $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures $good_state($s);
    ensures !$closed($s, c);

procedure $kill_claim(c:$ptr) returns ();
    modifies $s;
    ensures (forall p : $ptr :: { $select.sm($statusmap($s), p) } $select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p) || p == c);
    ensures $typemap(old($s)) == $typemap($s);
    ensures $memory(old($s)) == $memory($s);
    ensures $current_timestamp(old($s)) <= $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    ensures $good_state($s);
    ensures !$closed($s, c);

function $claims_upgrade(the_new:$ptr, the_old:$ptr) returns (bool);
axiom (forall the_new : $ptr, the_old : $ptr :: { $claims_upgrade(the_new, the_old) } $claims_upgrade(the_new, the_old) == (forall o : $ptr :: $claims_obj(the_old, o) ==> $claims_obj(the_new, o)));
function { :weight 0 } $ref_cnt(S:$state, p:$ptr) returns (int);
axiom (forall S : $state, p : $ptr :: { $ref_cnt(S, p) } $ref_cnt(S, p) == $st_ref_cnt($select.sm($statusmap(S), p)));
function $is_claimable($ctype) returns (bool);
axiom $is_claimable(^^claim);
function $is_thread_local_storage($ctype) returns (bool);
function $account_claim(S:$state, c:$ptr, o:$ptr) returns (bool);
axiom (forall S : $state, c : $ptr, o : $ptr :: { $account_claim(S, c, o) } $account_claim(S, c, o) == ($good_state(S) && $closed(S, c) && $claims_obj(c, o)));
function $claim_no(S:$state, o:$ptr, idx:int) returns ($ptr);
function $claim_idx(o:$ptr, c:$ptr) returns (int);
axiom (forall S : $state, c : $ptr, o : $ptr :: { $account_claim(S, c, o) } $account_claim(S, c, o) ==> $claim_no(S, o, $claim_idx(o, c)) == c && 0 <= $claim_idx(o, c) && $claim_idx(o, c) < $ref_cnt(S, o));
function $frame_level($pure_function) returns (int);
const $current_frame_level : int;
function $reads_check_pre(s:$state) returns (bool);
function $reads_check_post(s:$state) returns (bool);
procedure $reads_havoc() returns ();
    modifies $s;
    requires $reads_check_pre($s);
    ensures $reads_check_post($s);
    ensures $call_transition(old($s), $s);

function $start_here() returns (bool);
function $ptrset_to_int($ptrset) returns (int);
function $int_to_ptrset(int) returns ($ptrset);
axiom (forall p : $ptrset :: $int_to_ptrset($ptrset_to_int(p)) == p);
function $version_to_int($version) returns (int);
function $int_to_version(int) returns ($version);
axiom (forall p : $version :: $int_to_version($version_to_int(p)) == p);
function $vol_version_to_int($vol_version) returns (int);
function $int_to_vol_version(int) returns ($vol_version);
axiom (forall p : $vol_version :: $int_to_vol_version($vol_version_to_int(p)) == p);
function $ptr_to_int($ptr) returns (int);
function $int_to_ptr(int) returns ($ptr);
axiom (forall p : $ptr :: $int_to_ptr($ptr_to_int(p)) == p);
function $precise_test($ptr) returns (bool);
function $updated_only_values(S1:$state, S2:$state, W:$ptrset) returns (bool);
function $updated_only_domains(S1:$state, S2:$state, W:$ptrset) returns (bool);
axiom (forall S1 : $state, S2 : $state, W : $ptrset :: { $updated_only_values(S1, S2, W) } (forall p : $ptr :: { $dont_instantiate(p) } $is_primitive($typ(p)) || $is_non_primitive($typ(p)) ==> $typed(S1, p) && !($owner(S1, p) != $me() || ($kind_of($typ(p)) == $kind_primitive && $closed(S1, p))) ==> $select.mem($memory(S1), p) == $select.mem($memory(S2), p) || $set_in(p, W)) ==> $updated_only_values(S1, S2, W));
axiom (forall S1 : $state, S2 : $state, W : $ptrset :: { $updated_only_domains(S1, S2, W) } (forall p : $ptr :: { $dont_instantiate(p) } $set_in(p, W) && !($kind_of($typ(p)) == $kind_primitive) ==> $select.mem($memory(S1), p) == $select.mem($memory(S2), p) || $domain_updated_at(S1, S2, p, W)) ==> $updated_only_domains(S1, S2, W));
function $domain_updated_at(S1:$state, S2:$state, p:$ptr, W:$ptrset) returns (bool);
axiom (forall S1 : $state, S2 : $state, p : $ptr, W : $ptrset :: { $domain_updated_at(S1, S2, p, W) } $domain_updated_at(S1, S2, p, W) == ((forall q : $ptr :: { $fetch_from_domain($read_version(S2, p), q) } $kind_of($typ(q)) == $kind_primitive && !$set_in(q, W) ==> $fetch_from_domain($read_version(S1, p), q) == $fetch_from_domain($read_version(S2, p), q)) && $domain(S1, p) == $domain(S2, p)));
function $add_f4(x:$primitive, y:$primitive) returns ($primitive);
function $sub_f4(x:$primitive, y:$primitive) returns ($primitive);
function $mul_f4(x:$primitive, y:$primitive) returns ($primitive);
function $div_f4(x:$primitive, y:$primitive) returns ($primitive);
function $neg_f4(x:$primitive) returns ($primitive);
function $lt_f4(x:$primitive, y:$primitive) returns (bool);
function $leq_f4(x:$primitive, y:$primitive) returns (bool);
function $gt_f4(x:$primitive, y:$primitive) returns (bool);
function $geq_f4(x:$primitive, y:$primitive) returns (bool);
function $add_f8(x:$primitive, y:$primitive) returns ($primitive);
function $sub_f8(x:$primitive, y:$primitive) returns ($primitive);
function $mul_f8(x:$primitive, y:$primitive) returns ($primitive);
function $div_f8(x:$primitive, y:$primitive) returns ($primitive);
function $neg_f8(x:$primitive) returns ($primitive);
function $lt_f8(x:$primitive, y:$primitive) returns (bool);
function $leq_f8(x:$primitive, y:$primitive) returns (bool);
function $gt_f8(x:$primitive, y:$primitive) returns (bool);
function $geq_f8(x:$primitive, y:$primitive) returns (bool);
type cf_event;
type var_locglob;
const conditional_moment : cf_event;
const took_then_branch : cf_event;
const took_else_branch : cf_event;
const loop_register : cf_event;
const loop_entered : cf_event;
const loop_exited : cf_event;
const cev_local : var_locglob;
const cev_global : var_locglob;
const cev_parameter : var_locglob;
const cev_implicit : var_locglob;
function #cev_init(n:int) returns (bool);
function #cev_save_position(n:int) returns ($token);
function #cev_var_intro(n:int, locorglob:var_locglob, name:$token, val:int, typ:$ctype) returns (bool);
function #cev_var_update(n:int, locorglob:var_locglob, name:$token, val:int) returns (bool);
function #cev_control_flow_event(n:int, tag:cf_event) returns (bool);
function #cev_function_call(n:int) returns (bool);
var $cev_pc : int;
procedure $cev_step(pos:$token) returns ();
    modifies $cev_pc;
    ensures #cev_save_position(old($cev_pc)) == pos;
    ensures $cev_pc == old($cev_pc) + 1;

procedure $cev_pre_loop(pos:$token) returns (oldPC:int);
    modifies $cev_pc;
    ensures #cev_control_flow_event(old($cev_pc), conditional_moment);
    ensures #cev_save_position(old($cev_pc)) == pos;
    ensures oldPC == old($cev_pc) && $cev_pc == old($cev_pc) + 1;

procedure three_times(P#n:int) returns ($result:int);
    requires P#n >= 0;
    requires $_mul(3, P#n) < 2147483647;
    modifies $s;
    ensures $result == $_mul(3, P#n);
    free ensures $min.i4 <= $result && $result <= $max.i4;
    free ensures (forall p : $ptr :: { $select.sm($statusmap($s), p) } $kind_of($typ($owner($s, p))) != $kind_thread ==> $kind_of($typ($owner(old($s), p))) != $kind_thread) && (forall p : $ptr :: { $select.mem($memory($s), p) } $thread_local(old($s), p) ==> $select.mem($memory(old($s)), p) == $select.mem($memory($s), p) && $thread_local($s, p)) && (forall p : $ptr :: { $select.sm($statusmap($s), p) } $thread_local(old($s), p) ==> $select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p) && $thread_local($s, p)) && (forall p : $ptr :: { $select.tm($typemap($s), p) } $thread_local(old($s), p) ==> $select.tm($typemap(old($s)), p) == $select.tm($typemap($s), p) && $thread_local($s, p)) && $current_timestamp(old($s)) <= $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    free ensures $call_transition(old($s), $s);

implementation three_times(P#n:int) returns ($result:int)
{
    var loopState#0 : $state;
    var L#s : int where $min.i4 <= L#s && L#s <= $max.i4;
    var L#i : int where $min.i4 <= L#i && L#i <= $max.i4;
    var #wrTime$1^4.1 : int;
    var #stackframe : int;

  $Ultimate##0:
  anon4:
    assume $function_entry($s);
    assume $good_state_ext(#tok$1^4.1, $s) && $full_stop($s);
    assume (forall f : $pure_function :: { $frame_level(f) } $frame_level(f) < $current_frame_level);
    assume $local_value_is($s, #tok$1^4.1, #loc.n, P#n, ^^i4);
    assume #wrTime$1^4.1 == $current_timestamp($s);
    assume (forall #p : $ptr :: { $in_writes_at(#wrTime$1^4.1, #p) } $in_writes_at(#wrTime$1^4.1, #p) == false);
    assume $min.i4 <= P#n && P#n <= $max.i4;
    L#s := 0;
    assume $local_value_is($s, #tok$1^9.2, #loc.s, L#s, ^^i4);
    L#i := 0;
    assume $local_value_is($s, #tok$1^10.2, #loc.i, L#i, ^^i4);
    loopState#0 := $s;
    goto $Ultimate##1;
  $Ultimate##1:
    assert L#s == $_mul(L#i, 3);
    assert L#i <= P#n;
    goto $Ultimate##2, $Ultimate##3;
  $Ultimate##2:
    assume true;
    goto anon3;
  anon3:
    assume (forall p : $ptr :: { $select.sm($statusmap($s), p) } $kind_of($typ($owner($s, p))) != $kind_thread ==> $kind_of($typ($owner(old($s), p))) != $kind_thread) && (forall p : $ptr :: { $select.mem($memory($s), p) } $thread_local(old($s), p) ==> $select.mem($memory(old($s)), p) == $select.mem($memory($s), p) && $thread_local($s, p)) && (forall p : $ptr :: { $select.sm($statusmap($s), p) } $thread_local(old($s), p) ==> $select.sm($statusmap(old($s)), p) == $select.sm($statusmap($s), p) && $thread_local($s, p)) && (forall p : $ptr :: { $select.tm($typemap($s), p) } $thread_local(old($s), p) ==> $select.tm($typemap(old($s)), p) == $select.tm($typemap($s), p) && $thread_local($s, p)) && $current_timestamp(old($s)) <= $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(old($s), p) <= $timestamp($s, p)) && $call_transition(old($s), $s);
    assume $current_timestamp(loopState#0) <= $current_timestamp($s) && (forall p : $ptr :: { :weight 0 } { $timestamp($s, p) } $timestamp(loopState#0, p) <= $timestamp($s, p)) && $call_transition(loopState#0, $s);
    assume $good_state_ext(#tok$1^12.2, $s) && $full_stop($s);
    assume $local_value_is($s, #tok$1^12.2, #loc.i, L#i, ^^i4);
    assume $local_value_is($s, #tok$1^12.2, #loc.s, L#s, ^^i4);
    assume $local_value_is($s, #tok$1^12.2, #loc.n, P#n, ^^i4);
    assume $typemap(loopState#0) == $typemap($s) && $statusmap(loopState#0) == $statusmap($s);
    goto $Ultimate##4, $Ultimate##5;
  $Ultimate##4:
    assume L#i < P#n;
    goto anon1;
  anon1:
    assert $min.i4 <= L#s + 3 && L#s + 3 <= $max.i4;
    L#s := L#s + 3;
    assume $local_value_is($s, #tok$1^16.3, #loc.s, L#s, ^^i4);
    assert $min.i4 <= L#i + 1 && L#i + 1 <= $max.i4;
    L#i := L#i + 1;
    assume $local_value_is($s, #tok$1^17.3, #loc.i, L#i, ^^i4);
    goto #continue_1;
  $Ultimate##5:
    assume !(L#i < P#n);
    goto anon2;
  anon2:
    goto #break_1;
  #continue_1:
    goto $Ultimate##1;
  $Ultimate##3:
    assume !true;
    goto anon5;
  anon5:
    assume $good_state_ext(#tok$1^12.2, $s) && $full_stop($s);
    goto #break_1;
  #break_1:
    assert L#i == P#n;
    assume L#i == P#n;
    $result := L#s;
    assert $position_marker();
    goto #exit;
  anon6:
  #exit:
    return;
}

const #tok$1^17.3 : $token;
const #tok$1^16.3 : $token;
const #tok$1^12.2 : $token;
const #loc.i : $token;
const #tok$1^10.2 : $token;
const #loc.s : $token;
const #tok$1^9.2 : $token;
const #loc.n : $token;
const #tok$1^4.1 : $token;
const #file^C?3A?5CUsers?5Cmaus?5CDocuments?5CUltimate?5Ctrunk?5Cexamples?5CVCC?5Cthree_times.cpp : $token;
axiom $file_name_is(1, #file^C?3A?5CUsers?5Cmaus?5CDocuments?5CUltimate?5Ctrunk?5Cexamples?5CVCC?5Cthree_times.cpp);
axiom ^^i1 != ^^i2;
axiom ^^i1 != ^^i4;
axiom ^^i1 != ^^i8;
axiom ^^i1 != ^^u1;
axiom ^^i1 != ^^u2;
axiom ^^i1 != ^^u4;
axiom ^^i1 != ^^u8;
axiom ^^i1 != ^^void;
axiom ^^i1 != ^^bool;
axiom ^^i1 != ^^f4;
axiom ^^i1 != ^^f8;
axiom ^^i1 != ^^claim;
axiom ^^i1 != ^^root_emb;
axiom ^^i1 != ^^mathint;
axiom ^^i1 != ^$#thread_id_t;
axiom ^^i1 != ^$#ptrset;
axiom ^^i1 != ^$#state_t;
axiom ^^i1 != ^$#struct;
axiom ^^i1 != $memory_allocator_type;
axiom ^^i2 != ^^i4;
axiom ^^i2 != ^^i8;
axiom ^^i2 != ^^u1;
axiom ^^i2 != ^^u2;
axiom ^^i2 != ^^u4;
axiom ^^i2 != ^^u8;
axiom ^^i2 != ^^void;
axiom ^^i2 != ^^bool;
axiom ^^i2 != ^^f4;
axiom ^^i2 != ^^f8;
axiom ^^i2 != ^^claim;
axiom ^^i2 != ^^root_emb;
axiom ^^i2 != ^^mathint;
axiom ^^i2 != ^$#thread_id_t;
axiom ^^i2 != ^$#ptrset;
axiom ^^i2 != ^$#state_t;
axiom ^^i2 != ^$#struct;
axiom ^^i2 != $memory_allocator_type;
axiom ^^i4 != ^^i8;
axiom ^^i4 != ^^u1;
axiom ^^i4 != ^^u2;
axiom ^^i4 != ^^u4;
axiom ^^i4 != ^^u8;
axiom ^^i4 != ^^void;
axiom ^^i4 != ^^bool;
axiom ^^i4 != ^^f4;
axiom ^^i4 != ^^f8;
axiom ^^i4 != ^^claim;
axiom ^^i4 != ^^root_emb;
axiom ^^i4 != ^^mathint;
axiom ^^i4 != ^$#thread_id_t;
axiom ^^i4 != ^$#ptrset;
axiom ^^i4 != ^$#state_t;
axiom ^^i4 != ^$#struct;
axiom ^^i4 != $memory_allocator_type;
axiom ^^i8 != ^^u1;
axiom ^^i8 != ^^u2;
axiom ^^i8 != ^^u4;
axiom ^^i8 != ^^u8;
axiom ^^i8 != ^^void;
axiom ^^i8 != ^^bool;
axiom ^^i8 != ^^f4;
axiom ^^i8 != ^^f8;
axiom ^^i8 != ^^claim;
axiom ^^i8 != ^^root_emb;
axiom ^^i8 != ^^mathint;
axiom ^^i8 != ^$#thread_id_t;
axiom ^^i8 != ^$#ptrset;
axiom ^^i8 != ^$#state_t;
axiom ^^i8 != ^$#struct;
axiom ^^i8 != $memory_allocator_type;
axiom ^^u1 != ^^u2;
axiom ^^u1 != ^^u4;
axiom ^^u1 != ^^u8;
axiom ^^u1 != ^^void;
axiom ^^u1 != ^^bool;
axiom ^^u1 != ^^f4;
axiom ^^u1 != ^^f8;
axiom ^^u1 != ^^claim;
axiom ^^u1 != ^^root_emb;
axiom ^^u1 != ^^mathint;
axiom ^^u1 != ^$#thread_id_t;
axiom ^^u1 != ^$#ptrset;
axiom ^^u1 != ^$#state_t;
axiom ^^u1 != ^$#struct;
axiom ^^u1 != $memory_allocator_type;
axiom ^^u2 != ^^u4;
axiom ^^u2 != ^^u8;
axiom ^^u2 != ^^void;
axiom ^^u2 != ^^bool;
axiom ^^u2 != ^^f4;
axiom ^^u2 != ^^f8;
axiom ^^u2 != ^^claim;
axiom ^^u2 != ^^root_emb;
axiom ^^u2 != ^^mathint;
axiom ^^u2 != ^$#thread_id_t;
axiom ^^u2 != ^$#ptrset;
axiom ^^u2 != ^$#state_t;
axiom ^^u2 != ^$#struct;
axiom ^^u2 != $memory_allocator_type;
axiom ^^u4 != ^^u8;
axiom ^^u4 != ^^void;
axiom ^^u4 != ^^bool;
axiom ^^u4 != ^^f4;
axiom ^^u4 != ^^f8;
axiom ^^u4 != ^^claim;
axiom ^^u4 != ^^root_emb;
axiom ^^u4 != ^^mathint;
axiom ^^u4 != ^$#thread_id_t;
axiom ^^u4 != ^$#ptrset;
axiom ^^u4 != ^$#state_t;
axiom ^^u4 != ^$#struct;
axiom ^^u4 != $memory_allocator_type;
axiom ^^u8 != ^^void;
axiom ^^u8 != ^^bool;
axiom ^^u8 != ^^f4;
axiom ^^u8 != ^^f8;
axiom ^^u8 != ^^claim;
axiom ^^u8 != ^^root_emb;
axiom ^^u8 != ^^mathint;
axiom ^^u8 != ^$#thread_id_t;
axiom ^^u8 != ^$#ptrset;
axiom ^^u8 != ^$#state_t;
axiom ^^u8 != ^$#struct;
axiom ^^u8 != $memory_allocator_type;
axiom ^^void != ^^bool;
axiom ^^void != ^^f4;
axiom ^^void != ^^f8;
axiom ^^void != ^^claim;
axiom ^^void != ^^root_emb;
axiom ^^void != ^^mathint;
axiom ^^void != ^$#thread_id_t;
axiom ^^void != ^$#ptrset;
axiom ^^void != ^$#state_t;
axiom ^^void != ^$#struct;
axiom ^^void != $memory_allocator_type;
axiom ^^bool != ^^f4;
axiom ^^bool != ^^f8;
axiom ^^bool != ^^claim;
axiom ^^bool != ^^root_emb;
axiom ^^bool != ^^mathint;
axiom ^^bool != ^$#thread_id_t;
axiom ^^bool != ^$#ptrset;
axiom ^^bool != ^$#state_t;
axiom ^^bool != ^$#struct;
axiom ^^bool != $memory_allocator_type;
axiom ^^f4 != ^^f8;
axiom ^^f4 != ^^claim;
axiom ^^f4 != ^^root_emb;
axiom ^^f4 != ^^mathint;
axiom ^^f4 != ^$#thread_id_t;
axiom ^^f4 != ^$#ptrset;
axiom ^^f4 != ^$#state_t;
axiom ^^f4 != ^$#struct;
axiom ^^f4 != $memory_allocator_type;
axiom ^^f8 != ^^claim;
axiom ^^f8 != ^^root_emb;
axiom ^^f8 != ^^mathint;
axiom ^^f8 != ^$#thread_id_t;
axiom ^^f8 != ^$#ptrset;
axiom ^^f8 != ^$#state_t;
axiom ^^f8 != ^$#struct;
axiom ^^f8 != $memory_allocator_type;
axiom ^^claim != ^^root_emb;
axiom ^^claim != ^^mathint;
axiom ^^claim != ^$#thread_id_t;
axiom ^^claim != ^$#ptrset;
axiom ^^claim != ^$#state_t;
axiom ^^claim != ^$#struct;
axiom ^^claim != $memory_allocator_type;
axiom ^^root_emb != ^^mathint;
axiom ^^root_emb != ^$#thread_id_t;
axiom ^^root_emb != ^$#ptrset;
axiom ^^root_emb != ^$#state_t;
axiom ^^root_emb != ^$#struct;
axiom ^^root_emb != $memory_allocator_type;
axiom ^^mathint != ^$#thread_id_t;
axiom ^^mathint != ^$#ptrset;
axiom ^^mathint != ^$#state_t;
axiom ^^mathint != ^$#struct;
axiom ^^mathint != $memory_allocator_type;
axiom ^$#thread_id_t != ^$#ptrset;
axiom ^$#thread_id_t != ^$#state_t;
axiom ^$#thread_id_t != ^$#struct;
axiom ^$#thread_id_t != $memory_allocator_type;
axiom ^$#ptrset != ^$#state_t;
axiom ^$#ptrset != ^$#struct;
axiom ^$#ptrset != $memory_allocator_type;
axiom ^$#state_t != ^$#struct;
axiom ^$#state_t != $memory_allocator_type;
axiom ^$#struct != $memory_allocator_type;
axiom conditional_moment != took_then_branch;
axiom conditional_moment != took_else_branch;
axiom conditional_moment != loop_register;
axiom conditional_moment != loop_entered;
axiom conditional_moment != loop_exited;
axiom took_then_branch != took_else_branch;
axiom took_then_branch != loop_register;
axiom took_then_branch != loop_entered;
axiom took_then_branch != loop_exited;
axiom took_else_branch != loop_register;
axiom took_else_branch != loop_entered;
axiom took_else_branch != loop_exited;
axiom loop_register != loop_entered;
axiom loop_register != loop_exited;
axiom loop_entered != loop_exited;
axiom $kind_composite != $kind_primitive;
axiom $kind_composite != $kind_array;
axiom $kind_composite != $kind_thread;
axiom $kind_primitive != $kind_array;
axiom $kind_primitive != $kind_thread;
axiom $kind_array != $kind_thread;
axiom #tok$1^17.3 != #tok$1^16.3;
axiom #tok$1^17.3 != #tok$1^12.2;
axiom #tok$1^17.3 != #loc.i;
axiom #tok$1^17.3 != #tok$1^10.2;
axiom #tok$1^17.3 != #loc.s;
axiom #tok$1^17.3 != #tok$1^9.2;
axiom #tok$1^17.3 != #loc.n;
axiom #tok$1^17.3 != #tok$1^4.1;
axiom #tok$1^17.3 != #file^C?3A?5CUsers?5Cmaus?5CDocuments?5CUltimate?5Ctrunk?5Cexamples?5CVCC?5Cthree_times.cpp;
axiom #tok$1^16.3 != #tok$1^12.2;
axiom #tok$1^16.3 != #loc.i;
axiom #tok$1^16.3 != #tok$1^10.2;
axiom #tok$1^16.3 != #loc.s;
axiom #tok$1^16.3 != #tok$1^9.2;
axiom #tok$1^16.3 != #loc.n;
axiom #tok$1^16.3 != #tok$1^4.1;
axiom #tok$1^16.3 != #file^C?3A?5CUsers?5Cmaus?5CDocuments?5CUltimate?5Ctrunk?5Cexamples?5CVCC?5Cthree_times.cpp;
axiom #tok$1^12.2 != #loc.i;
axiom #tok$1^12.2 != #tok$1^10.2;
axiom #tok$1^12.2 != #loc.s;
axiom #tok$1^12.2 != #tok$1^9.2;
axiom #tok$1^12.2 != #loc.n;
axiom #tok$1^12.2 != #tok$1^4.1;
axiom #tok$1^12.2 != #file^C?3A?5CUsers?5Cmaus?5CDocuments?5CUltimate?5Ctrunk?5Cexamples?5CVCC?5Cthree_times.cpp;
axiom #loc.i != #tok$1^10.2;
axiom #loc.i != #loc.s;
axiom #loc.i != #tok$1^9.2;
axiom #loc.i != #loc.n;
axiom #loc.i != #tok$1^4.1;
axiom #loc.i != #file^C?3A?5CUsers?5Cmaus?5CDocuments?5CUltimate?5Ctrunk?5Cexamples?5CVCC?5Cthree_times.cpp;
axiom #tok$1^10.2 != #loc.s;
axiom #tok$1^10.2 != #tok$1^9.2;
axiom #tok$1^10.2 != #loc.n;
axiom #tok$1^10.2 != #tok$1^4.1;
axiom #tok$1^10.2 != #file^C?3A?5CUsers?5Cmaus?5CDocuments?5CUltimate?5Ctrunk?5Cexamples?5CVCC?5Cthree_times.cpp;
axiom #loc.s != #tok$1^9.2;
axiom #loc.s != #loc.n;
axiom #loc.s != #tok$1^4.1;
axiom #loc.s != #file^C?3A?5CUsers?5Cmaus?5CDocuments?5CUltimate?5Ctrunk?5Cexamples?5CVCC?5Cthree_times.cpp;
axiom #tok$1^9.2 != #loc.n;
axiom #tok$1^9.2 != #tok$1^4.1;
axiom #tok$1^9.2 != #file^C?3A?5CUsers?5Cmaus?5CDocuments?5CUltimate?5Ctrunk?5Cexamples?5CVCC?5Cthree_times.cpp;
axiom #loc.n != #tok$1^4.1;
axiom #loc.n != #file^C?3A?5CUsers?5Cmaus?5CDocuments?5CUltimate?5Ctrunk?5Cexamples?5CVCC?5Cthree_times.cpp;
axiom #tok$1^4.1 != #file^C?3A?5CUsers?5Cmaus?5CDocuments?5CUltimate?5Ctrunk?5Cexamples?5CVCC?5Cthree_times.cpp;
axiom cev_local != cev_global;
axiom cev_local != cev_parameter;
axiom cev_local != cev_implicit;
axiom cev_global != cev_parameter;
axiom cev_global != cev_implicit;
axiom cev_parameter != cev_implicit;