src/HOL/SMT_Examples/VCC_Max.b2i
author haftmann
Sat Jul 05 11:01:53 2014 +0200 (2014-07-05)
changeset 57514 bdc2c6b40bf2
parent 52722 2c81f7baf8c4
permissions -rw-r--r--
prefer ac_simps collections over separate name bindings for add and mult
     1 type-decl $ctype 0 0
     2 type-decl $ptr 0 0
     3 type-decl $field 0 0
     4 type-decl $kind 0 0
     5 type-decl $type_state 0 0
     6 type-decl $status 0 0
     7 type-decl $primitive 0 0
     8 type-decl $struct 0 0
     9 type-decl $token 0 0
    10 type-decl $state 0 0
    11 type-decl $pure_function 0 0
    12 type-decl $label 0 0
    13 type-decl $memory_t 0 0
    14 type-decl $typemap_t 0 0
    15 type-decl $statusmap_t 0 0
    16 type-decl $record 0 0
    17 type-decl $version 0 0
    18 type-decl $vol_version 0 0
    19 type-decl $ptrset 0 0
    20 fun-decl $kind_of 2 0
    21     type-con $ctype 0
    22     type-con $kind 0
    23 fun-decl $kind_composite 1 1
    24     type-con $kind 0
    25   attribute unique 0
    26 fun-decl $kind_primitive 1 1
    27     type-con $kind 0
    28   attribute unique 0
    29 fun-decl $kind_array 1 1
    30     type-con $kind 0
    31   attribute unique 0
    32 fun-decl $kind_thread 1 1
    33     type-con $kind 0
    34   attribute unique 0
    35 fun-decl $sizeof 2 0
    36     type-con $ctype 0
    37     int
    38 fun-decl ^^i1 1 1
    39     type-con $ctype 0
    40   attribute unique 0
    41 fun-decl ^^i2 1 1
    42     type-con $ctype 0
    43   attribute unique 0
    44 fun-decl ^^i4 1 1
    45     type-con $ctype 0
    46   attribute unique 0
    47 fun-decl ^^i8 1 1
    48     type-con $ctype 0
    49   attribute unique 0
    50 fun-decl ^^u1 1 1
    51     type-con $ctype 0
    52   attribute unique 0
    53 fun-decl ^^u2 1 1
    54     type-con $ctype 0
    55   attribute unique 0
    56 fun-decl ^^u4 1 1
    57     type-con $ctype 0
    58   attribute unique 0
    59 fun-decl ^^u8 1 1
    60     type-con $ctype 0
    61   attribute unique 0
    62 fun-decl ^^void 1 1
    63     type-con $ctype 0
    64   attribute unique 0
    65 fun-decl ^^bool 1 1
    66     type-con $ctype 0
    67   attribute unique 0
    68 fun-decl ^^f4 1 1
    69     type-con $ctype 0
    70   attribute unique 0
    71 fun-decl ^^f8 1 1
    72     type-con $ctype 0
    73   attribute unique 0
    74 fun-decl ^^claim 1 1
    75     type-con $ctype 0
    76   attribute unique 0
    77 fun-decl ^^root_emb 1 1
    78     type-con $ctype 0
    79   attribute unique 0
    80 fun-decl ^^mathint 1 1
    81     type-con $ctype 0
    82   attribute unique 0
    83 fun-decl ^$#thread_id_t 1 1
    84     type-con $ctype 0
    85   attribute unique 0
    86 fun-decl ^$#ptrset 1 1
    87     type-con $ctype 0
    88   attribute unique 0
    89 fun-decl ^$#state_t 1 1
    90     type-con $ctype 0
    91   attribute unique 0
    92 fun-decl ^$#struct 1 1
    93     type-con $ctype 0
    94   attribute unique 0
    95 fun-decl $ptr_to 2 0
    96     type-con $ctype 0
    97     type-con $ctype 0
    98 fun-decl $unptr_to 2 0
    99     type-con $ctype 0
   100     type-con $ctype 0
   101 fun-decl $ptr_level 2 0
   102     type-con $ctype 0
   103     int
   104 fun-decl $map_t 3 0
   105     type-con $ctype 0
   106     type-con $ctype 0
   107     type-con $ctype 0
   108 fun-decl $map_domain 2 0
   109     type-con $ctype 0
   110     type-con $ctype 0
   111 fun-decl $map_range 2 0
   112     type-con $ctype 0
   113     type-con $ctype 0
   114 fun-decl $is_primitive 2 1
   115     type-con $ctype 0
   116     bool
   117   attribute weight 1
   118     expr-attr
   119       int-num 0
   120 fun-decl $is_primitive_ch 2 1
   121     type-con $ctype 0
   122     bool
   123   attribute inline 1
   124     expr-attr
   125       true
   126 fun-decl $is_composite 2 1
   127     type-con $ctype 0
   128     bool
   129   attribute weight 1
   130     expr-attr
   131       int-num 0
   132 fun-decl $is_composite_ch 2 1
   133     type-con $ctype 0
   134     bool
   135   attribute inline 1
   136     expr-attr
   137       true
   138 fun-decl $is_arraytype 2 1
   139     type-con $ctype 0
   140     bool
   141   attribute weight 1
   142     expr-attr
   143       int-num 0
   144 fun-decl $is_arraytype_ch 2 1
   145     type-con $ctype 0
   146     bool
   147   attribute inline 1
   148     expr-attr
   149       true
   150 fun-decl $is_threadtype 2 1
   151     type-con $ctype 0
   152     bool
   153   attribute weight 1
   154     expr-attr
   155       int-num 0
   156 fun-decl $is_thread 2 1
   157     type-con $ptr 0
   158     bool
   159   attribute inline 1
   160     expr-attr
   161       true
   162 fun-decl $is_ptr_to_composite 2 1
   163     type-con $ptr 0
   164     bool
   165   attribute inline 1
   166     expr-attr
   167       true
   168 fun-decl $field_offset 2 0
   169     type-con $field 0
   170     int
   171 fun-decl $field_parent_type 2 0
   172     type-con $field 0
   173     type-con $ctype 0
   174 fun-decl $is_non_primitive 2 0
   175     type-con $ctype 0
   176     bool
   177 fun-decl $is_non_primitive_ch 2 1
   178     type-con $ctype 0
   179     bool
   180   attribute inline 1
   181     expr-attr
   182       true
   183 fun-decl $is_non_primitive_ptr 2 1
   184     type-con $ptr 0
   185     bool
   186   attribute inline 1
   187     expr-attr
   188       true
   189 fun-decl $me_ref 1 0
   190     int
   191 fun-decl $me 1 0
   192     type-con $ptr 0
   193 fun-decl $current_state 2 1
   194     type-con $state 0
   195     type-con $state 0
   196   attribute inline 1
   197     expr-attr
   198       true
   199 fun-decl $select.mem 3 0
   200     type-con $memory_t 0
   201     type-con $ptr 0
   202     int
   203 fun-decl $store.mem 4 0
   204     type-con $memory_t 0
   205     type-con $ptr 0
   206     int
   207     type-con $memory_t 0
   208 fun-decl $select.tm 3 0
   209     type-con $typemap_t 0
   210     type-con $ptr 0
   211     type-con $type_state 0
   212 fun-decl $store.tm 4 0
   213     type-con $typemap_t 0
   214     type-con $ptr 0
   215     type-con $type_state 0
   216     type-con $typemap_t 0
   217 fun-decl $select.sm 3 0
   218     type-con $statusmap_t 0
   219     type-con $ptr 0
   220     type-con $status 0
   221 fun-decl $store.sm 4 0
   222     type-con $statusmap_t 0
   223     type-con $ptr 0
   224     type-con $status 0
   225     type-con $statusmap_t 0
   226 fun-decl $memory 2 0
   227     type-con $state 0
   228     type-con $memory_t 0
   229 fun-decl $typemap 2 0
   230     type-con $state 0
   231     type-con $typemap_t 0
   232 fun-decl $statusmap 2 0
   233     type-con $state 0
   234     type-con $statusmap_t 0
   235 fun-decl $mem 3 1
   236     type-con $state 0
   237     type-con $ptr 0
   238     int
   239   attribute inline 1
   240     expr-attr
   241       true
   242 fun-decl $read_any 3 1
   243     type-con $state 0
   244     type-con $ptr 0
   245     int
   246   attribute inline 1
   247     expr-attr
   248       true
   249 fun-decl $mem_eq 4 1
   250     type-con $state 0
   251     type-con $state 0
   252     type-con $ptr 0
   253     bool
   254   attribute inline 1
   255     expr-attr
   256       true
   257 fun-decl $st_eq 4 1
   258     type-con $state 0
   259     type-con $state 0
   260     type-con $ptr 0
   261     bool
   262   attribute inline 1
   263     expr-attr
   264       true
   265 fun-decl $ts_eq 4 1
   266     type-con $state 0
   267     type-con $state 0
   268     type-con $ptr 0
   269     bool
   270   attribute inline 1
   271     expr-attr
   272       true
   273 fun-decl $extent_hint 3 0
   274     type-con $ptr 0
   275     type-con $ptr 0
   276     bool
   277 fun-decl $nesting_level 2 0
   278     type-con $ctype 0
   279     int
   280 fun-decl $is_nested 3 0
   281     type-con $ctype 0
   282     type-con $ctype 0
   283     bool
   284 fun-decl $nesting_min 3 0
   285     type-con $ctype 0
   286     type-con $ctype 0
   287     int
   288 fun-decl $nesting_max 3 0
   289     type-con $ctype 0
   290     type-con $ctype 0
   291     int
   292 fun-decl $is_nested_range 5 0
   293     type-con $ctype 0
   294     type-con $ctype 0
   295     int
   296     int
   297     bool
   298 fun-decl $typ 2 0
   299     type-con $ptr 0
   300     type-con $ctype 0
   301 fun-decl $ref 2 0
   302     type-con $ptr 0
   303     int
   304 fun-decl $ptr 3 0
   305     type-con $ctype 0
   306     int
   307     type-con $ptr 0
   308 fun-decl $ghost_ref 3 0
   309     type-con $ptr 0
   310     type-con $field 0
   311     int
   312 fun-decl $ghost_emb 2 0
   313     int
   314     type-con $ptr 0
   315 fun-decl $ghost_path 2 0
   316     int
   317     type-con $field 0
   318 fun-decl $physical_ref 3 0
   319     type-con $ptr 0
   320     type-con $field 0
   321     int
   322 fun-decl $array_path 3 0
   323     type-con $field 0
   324     int
   325     type-con $field 0
   326 fun-decl $is_base_field 2 0
   327     type-con $field 0
   328     bool
   329 fun-decl $array_path_1 2 0
   330     type-con $field 0
   331     type-con $field 0
   332 fun-decl $array_path_2 2 0
   333     type-con $field 0
   334     int
   335 fun-decl $null 1 0
   336     type-con $ptr 0
   337 fun-decl $is 3 0
   338     type-con $ptr 0
   339     type-con $ctype 0
   340     bool
   341 fun-decl $ptr_cast 3 1
   342     type-con $ptr 0
   343     type-con $ctype 0
   344     type-con $ptr 0
   345   attribute inline 1
   346     expr-attr
   347       true
   348 fun-decl $read_ptr 4 1
   349     type-con $state 0
   350     type-con $ptr 0
   351     type-con $ctype 0
   352     type-con $ptr 0
   353   attribute inline 1
   354     expr-attr
   355       true
   356 fun-decl $dot 3 0
   357     type-con $ptr 0
   358     type-con $field 0
   359     type-con $ptr 0
   360 fun-decl $emb 3 1
   361     type-con $state 0
   362     type-con $ptr 0
   363     type-con $ptr 0
   364   attribute inline 1
   365     expr-attr
   366       true
   367 fun-decl $path 3 1
   368     type-con $state 0
   369     type-con $ptr 0
   370     type-con $field 0
   371   attribute inline 1
   372     expr-attr
   373       true
   374 fun-decl $containing_struct 3 0
   375     type-con $ptr 0
   376     type-con $field 0
   377     type-con $ptr 0
   378 fun-decl $containing_struct_ref 3 0
   379     type-con $ptr 0
   380     type-con $field 0
   381     int
   382 fun-decl $is_primitive_non_volatile_field 2 0
   383     type-con $field 0
   384     bool
   385 fun-decl $is_primitive_volatile_field 2 0
   386     type-con $field 0
   387     bool
   388 fun-decl $is_primitive_embedded_array 3 0
   389     type-con $field 0
   390     int
   391     bool
   392 fun-decl $is_primitive_embedded_volatile_array 4 0
   393     type-con $field 0
   394     int
   395     type-con $ctype 0
   396     bool
   397 fun-decl $static_field_properties 3 1
   398     type-con $field 0
   399     type-con $ctype 0
   400     bool
   401   attribute inline 1
   402     expr-attr
   403       true
   404 fun-decl $field_properties 6 1
   405     type-con $state 0
   406     type-con $ptr 0
   407     type-con $field 0
   408     type-con $ctype 0
   409     bool
   410     bool
   411   attribute inline 1
   412     expr-attr
   413       true
   414 fun-decl $ts_typed 2 0
   415     type-con $type_state 0
   416     bool
   417 fun-decl $ts_emb 2 0
   418     type-con $type_state 0
   419     type-con $ptr 0
   420 fun-decl $ts_path 2 0
   421     type-con $type_state 0
   422     type-con $field 0
   423 fun-decl $ts_is_array_elt 2 0
   424     type-con $type_state 0
   425     bool
   426 fun-decl $ts_is_volatile 2 0
   427     type-con $type_state 0
   428     bool
   429 fun-decl $is_object_root 3 1
   430     type-con $state 0
   431     type-con $ptr 0
   432     bool
   433   attribute inline 1
   434     expr-attr
   435       true
   436 fun-decl $is_volatile 3 1
   437     type-con $state 0
   438     type-con $ptr 0
   439     bool
   440   attribute inline 1
   441     expr-attr
   442       true
   443 fun-decl $is_malloc_root 3 1
   444     type-con $state 0
   445     type-con $ptr 0
   446     bool
   447   attribute inline 1
   448     expr-attr
   449       true
   450 fun-decl $current_timestamp 2 0
   451     type-con $state 0
   452     int
   453 fun-decl $is_fresh 4 1
   454     type-con $state 0
   455     type-con $state 0
   456     type-con $ptr 0
   457     bool
   458   attribute inline 1
   459     expr-attr
   460       true
   461 fun-decl $in_writes_at 3 0
   462     int
   463     type-con $ptr 0
   464     bool
   465 fun-decl $writable 4 1
   466     type-con $state 0
   467     int
   468     type-con $ptr 0
   469     bool
   470   attribute inline 1
   471     expr-attr
   472       true
   473 fun-decl $top_writable 4 1
   474     type-con $state 0
   475     int
   476     type-con $ptr 0
   477     bool
   478   attribute inline 1
   479     expr-attr
   480       true
   481 fun-decl $struct_zero 1 0
   482     type-con $struct 0
   483 fun-decl $vs_base 3 1
   484     type-con $struct 0
   485     type-con $ctype 0
   486     type-con $ptr 0
   487   attribute inline 1
   488     expr-attr
   489       true
   490 fun-decl $vs_base_ref 2 0
   491     type-con $struct 0
   492     int
   493 fun-decl $vs_state 2 0
   494     type-con $struct 0
   495     type-con $state 0
   496 fun-decl $vs_ctor 3 0
   497     type-con $state 0
   498     type-con $ptr 0
   499     type-con $struct 0
   500 fun-decl $rec_zero 1 0
   501     type-con $record 0
   502 fun-decl $rec_update 4 0
   503     type-con $record 0
   504     type-con $field 0
   505     int
   506     type-con $record 0
   507 fun-decl $rec_fetch 3 0
   508     type-con $record 0
   509     type-con $field 0
   510     int
   511 fun-decl $rec_update_bv 7 0
   512     type-con $record 0
   513     type-con $field 0
   514     int
   515     int
   516     int
   517     int
   518     type-con $record 0
   519 fun-decl $is_record_type 2 0
   520     type-con $ctype 0
   521     bool
   522 fun-decl $is_record_field 4 0
   523     type-con $ctype 0
   524     type-con $field 0
   525     type-con $ctype 0
   526     bool
   527 fun-decl $as_record_record_field 2 0
   528     type-con $field 0
   529     type-con $field 0
   530 fun-decl $rec_eq 3 0
   531     type-con $record 0
   532     type-con $record 0
   533     bool
   534 fun-decl $rec_base_eq 3 0
   535     int
   536     int
   537     bool
   538 fun-decl $int_to_record 2 0
   539     int
   540     type-con $record 0
   541 fun-decl $record_to_int 2 0
   542     type-con $record 0
   543     int
   544 fun-decl $good_state 2 0
   545     type-con $state 0
   546     bool
   547 fun-decl $invok_state 2 0
   548     type-con $state 0
   549     bool
   550 fun-decl $has_volatile_owns_set 2 0
   551     type-con $ctype 0
   552     bool
   553 fun-decl $owns_set_field 2 0
   554     type-con $ctype 0
   555     type-con $field 0
   556 fun-decl $st_owner 2 0
   557     type-con $status 0
   558     type-con $ptr 0
   559 fun-decl $st_closed 2 0
   560     type-con $status 0
   561     bool
   562 fun-decl $st_timestamp 2 0
   563     type-con $status 0
   564     int
   565 fun-decl $st_ref_cnt 2 0
   566     type-con $status 0
   567     int
   568 fun-decl $owner 3 0
   569     type-con $state 0
   570     type-con $ptr 0
   571     type-con $ptr 0
   572 fun-decl $closed 3 0
   573     type-con $state 0
   574     type-con $ptr 0
   575     bool
   576 fun-decl $timestamp 3 0
   577     type-con $state 0
   578     type-con $ptr 0
   579     int
   580 fun-decl $position_marker 1 0
   581     bool
   582 fun-decl $st 3 1
   583     type-con $state 0
   584     type-con $ptr 0
   585     type-con $status 0
   586   attribute inline 1
   587     expr-attr
   588       true
   589 fun-decl $ts 3 1
   590     type-con $state 0
   591     type-con $ptr 0
   592     type-con $type_state 0
   593   attribute inline 1
   594     expr-attr
   595       true
   596 fun-decl $owns 3 1
   597     type-con $state 0
   598     type-con $ptr 0
   599     type-con $ptrset 0
   600   attribute weight 1
   601     expr-attr
   602       int-num 0
   603 fun-decl $nested 3 1
   604     type-con $state 0
   605     type-con $ptr 0
   606     bool
   607   attribute inline 1
   608     expr-attr
   609       true
   610 fun-decl $nested_in 4 1
   611     type-con $state 0
   612     type-con $ptr 0
   613     type-con $ptr 0
   614     bool
   615   attribute inline 1
   616     expr-attr
   617       true
   618 fun-decl $wrapped 4 1
   619     type-con $state 0
   620     type-con $ptr 0
   621     type-con $ctype 0
   622     bool
   623   attribute inline 1
   624     expr-attr
   625       true
   626 fun-decl $irrelevant 3 1
   627     type-con $state 0
   628     type-con $ptr 0
   629     bool
   630   attribute inline 1
   631     expr-attr
   632       true
   633 fun-decl $mutable 3 1
   634     type-con $state 0
   635     type-con $ptr 0
   636     bool
   637   attribute weight 1
   638     expr-attr
   639       int-num 0
   640 fun-decl $thread_owned 3 1
   641     type-con $state 0
   642     type-con $ptr 0
   643     bool
   644   attribute inline 1
   645     expr-attr
   646       true
   647 fun-decl $thread_owned_or_even_mutable 3 1
   648     type-con $state 0
   649     type-con $ptr 0
   650     bool
   651   attribute inline 1
   652     expr-attr
   653       true
   654 fun-decl $typed 3 0
   655     type-con $state 0
   656     type-con $ptr 0
   657     bool
   658 fun-decl $typed2 4 1
   659     type-con $state 0
   660     type-con $ptr 0
   661     type-con $ctype 0
   662     bool
   663   attribute inline 1
   664     expr-attr
   665       true
   666 fun-decl $ptr_eq 3 1
   667     type-con $ptr 0
   668     type-con $ptr 0
   669     bool
   670   attribute inline 1
   671     expr-attr
   672       true
   673 fun-decl $ptr_neq 3 1
   674     type-con $ptr 0
   675     type-con $ptr 0
   676     bool
   677   attribute inline 1
   678     expr-attr
   679       true
   680 fun-decl $is_primitive_field_of 4 1
   681     type-con $state 0
   682     type-con $ptr 0
   683     type-con $ptr 0
   684     bool
   685   attribute inline 1
   686     expr-attr
   687       true
   688 fun-decl $instantiate_st 2 0
   689     type-con $status 0
   690     bool
   691 fun-decl $is_domain_root 3 0
   692     type-con $state 0
   693     type-con $ptr 0
   694     bool
   695 fun-decl $in_wrapped_domain 3 0
   696     type-con $state 0
   697     type-con $ptr 0
   698     bool
   699 fun-decl $thread_local_np 3 1
   700     type-con $state 0
   701     type-con $ptr 0
   702     bool
   703   attribute inline 1
   704     expr-attr
   705       true
   706 fun-decl $thread_local 3 0
   707     type-con $state 0
   708     type-con $ptr 0
   709     bool
   710 fun-decl $thread_local2 4 1
   711     type-con $state 0
   712     type-con $ptr 0
   713     type-con $ctype 0
   714     bool
   715   attribute inline 1
   716     expr-attr
   717       true
   718 fun-decl $dont_instantiate 2 0
   719     type-con $ptr 0
   720     bool
   721 fun-decl $dont_instantiate_int 2 0
   722     int
   723     bool
   724 fun-decl $dont_instantiate_state 2 0
   725     type-con $state 0
   726     bool
   727 fun-decl $instantiate_int 2 0
   728     int
   729     bool
   730 fun-decl $instantiate_bool 2 0
   731     bool
   732     bool
   733 fun-decl $instantiate_ptr 2 0
   734     type-con $ptr 0
   735     bool
   736 fun-decl $instantiate_ptrset 2 0
   737     type-con $ptrset 0
   738     bool
   739 fun-decl $inv 4 1
   740     type-con $state 0
   741     type-con $ptr 0
   742     type-con $ctype 0
   743     bool
   744   attribute inline 1
   745     expr-attr
   746       true
   747 fun-decl $inv2nt 4 1
   748     type-con $state 0
   749     type-con $state 0
   750     type-con $ptr 0
   751     bool
   752   attribute inline 1
   753     expr-attr
   754       true
   755 fun-decl $imply_inv 4 0
   756     type-con $state 0
   757     type-con $ptr 0
   758     type-con $ctype 0
   759     bool
   760 fun-decl $inv2 5 0
   761     type-con $state 0
   762     type-con $state 0
   763     type-con $ptr 0
   764     type-con $ctype 0
   765     bool
   766 fun-decl $inv2_when_closed 5 1
   767     type-con $state 0
   768     type-con $state 0
   769     type-con $ptr 0
   770     type-con $ctype 0
   771     bool
   772   attribute inline 1
   773     expr-attr
   774       true
   775 fun-decl $sequential 5 1
   776     type-con $state 0
   777     type-con $state 0
   778     type-con $ptr 0
   779     type-con $ctype 0
   780     bool
   781   attribute weight 1
   782     expr-attr
   783       int-num 0
   784 fun-decl $depends 5 1
   785     type-con $state 0
   786     type-con $state 0
   787     type-con $ptr 0
   788     type-con $ptr 0
   789     bool
   790   attribute weight 1
   791     expr-attr
   792       int-num 0
   793 fun-decl $spans_the_same 5 1
   794     type-con $state 0
   795     type-con $state 0
   796     type-con $ptr 0
   797     type-con $ctype 0
   798     bool
   799   attribute weight 1
   800     expr-attr
   801       int-num 0
   802 fun-decl $state_spans_the_same 5 0
   803     type-con $state 0
   804     type-con $state 0
   805     type-con $ptr 0
   806     type-con $ctype 0
   807     bool
   808 fun-decl $nonvolatile_spans_the_same 5 1
   809     type-con $state 0
   810     type-con $state 0
   811     type-con $ptr 0
   812     type-con $ctype 0
   813     bool
   814   attribute weight 1
   815     expr-attr
   816       int-num 0
   817 fun-decl $state_nonvolatile_spans_the_same 5 0
   818     type-con $state 0
   819     type-con $state 0
   820     type-con $ptr 0
   821     type-con $ctype 0
   822     bool
   823 fun-decl $in_extent_of 4 1
   824     type-con $state 0
   825     type-con $ptr 0
   826     type-con $ptr 0
   827     bool
   828   attribute inline 1
   829     expr-attr
   830       true
   831 fun-decl $in_full_extent_of 3 1
   832     type-con $ptr 0
   833     type-con $ptr 0
   834     bool
   835   attribute inline 1
   836     expr-attr
   837       true
   838 fun-decl $extent_mutable 3 0
   839     type-con $state 0
   840     type-con $ptr 0
   841     bool
   842 fun-decl $extent_is_fresh 4 0
   843     type-con $state 0
   844     type-con $state 0
   845     type-con $ptr 0
   846     bool
   847 fun-decl $forall_inv2_when_closed 3 1
   848     type-con $state 0
   849     type-con $state 0
   850     bool
   851   attribute inline 1
   852     expr-attr
   853       true
   854 fun-decl $function_entry 2 0
   855     type-con $state 0
   856     bool
   857 fun-decl $full_stop 2 0
   858     type-con $state 0
   859     bool
   860 fun-decl $full_stop_ext 3 1
   861     type-con $token 0
   862     type-con $state 0
   863     bool
   864   attribute inline 1
   865     expr-attr
   866       true
   867 fun-decl $file_name_is 3 0
   868     int
   869     type-con $token 0
   870     bool
   871 fun-decl $closed_is_transitive 2 1
   872     type-con $state 0
   873     bool
   874   attribute inline 1
   875     expr-attr
   876       true
   877 fun-decl $call_transition 3 0
   878     type-con $state 0
   879     type-con $state 0
   880     bool
   881 fun-decl $good_state_ext 3 0
   882     type-con $token 0
   883     type-con $state 0
   884     bool
   885 fun-decl $local_value_is 6 0
   886     type-con $state 0
   887     type-con $token 0
   888     type-con $token 0
   889     int
   890     type-con $ctype 0
   891     bool
   892 fun-decl $local_value_is_ptr 6 0
   893     type-con $state 0
   894     type-con $token 0
   895     type-con $token 0
   896     type-con $ptr 0
   897     type-con $ctype 0
   898     bool
   899 fun-decl $read_ptr_m 4 0
   900     type-con $state 0
   901     type-con $ptr 0
   902     type-con $ctype 0
   903     type-con $ptr 0
   904 fun-decl $type_code_is 3 0
   905     int
   906     type-con $ctype 0
   907     bool
   908 fun-decl $function_arg_type 4 0
   909     type-con $pure_function 0
   910     int
   911     type-con $ctype 0
   912     bool
   913 fun-decl $ver_domain 2 0
   914     type-con $version 0
   915     type-con $ptrset 0
   916 fun-decl $read_version 3 1
   917     type-con $state 0
   918     type-con $ptr 0
   919     type-con $version 0
   920   attribute weight 1
   921     expr-attr
   922       int-num 0
   923 fun-decl $domain 3 1
   924     type-con $state 0
   925     type-con $ptr 0
   926     type-con $ptrset 0
   927   attribute weight 1
   928     expr-attr
   929       int-num 0
   930 fun-decl $in_domain 4 0
   931     type-con $state 0
   932     type-con $ptr 0
   933     type-con $ptr 0
   934     bool
   935 fun-decl $in_vdomain 4 0
   936     type-con $state 0
   937     type-con $ptr 0
   938     type-con $ptr 0
   939     bool
   940 fun-decl $in_domain_lab 5 0
   941     type-con $state 0
   942     type-con $ptr 0
   943     type-con $ptr 0
   944     type-con $label 0
   945     bool
   946 fun-decl $in_vdomain_lab 5 0
   947     type-con $state 0
   948     type-con $ptr 0
   949     type-con $ptr 0
   950     type-con $label 0
   951     bool
   952 fun-decl $inv_lab 4 0
   953     type-con $state 0
   954     type-con $ptr 0
   955     type-con $label 0
   956     bool
   957 fun-decl $dom_thread_local 3 1
   958     type-con $state 0
   959     type-con $ptr 0
   960     bool
   961   attribute inline 1
   962     expr-attr
   963       true
   964 fun-decl $fetch_from_domain 3 0
   965     type-con $version 0
   966     type-con $ptr 0
   967     int
   968 fun-decl $in_claim_domain 3 0
   969     type-con $ptr 0
   970     type-con $ptr 0
   971     bool
   972 fun-decl $by_claim 5 1
   973     type-con $state 0
   974     type-con $ptr 0
   975     type-con $ptr 0
   976     type-con $ptr 0
   977     type-con $ptr 0
   978   attribute weight 1
   979     expr-attr
   980       int-num 0
   981 fun-decl $claim_version 2 0
   982     type-con $ptr 0
   983     type-con $version 0
   984 fun-decl $read_vol_version 3 1
   985     type-con $state 0
   986     type-con $ptr 0
   987     type-con $vol_version 0
   988   attribute weight 1
   989     expr-attr
   990       int-num 0
   991 fun-decl $fetch_from_vv 3 0
   992     type-con $vol_version 0
   993     type-con $ptr 0
   994     int
   995 fun-decl $fetch_vol_field 4 1
   996     type-con $state 0
   997     type-con $ptr 0
   998     type-con $field 0
   999     int
  1000   attribute inline 1
  1001     expr-attr
  1002       true
  1003 fun-decl $is_approved_by 4 0
  1004     type-con $ctype 0
  1005     type-con $field 0
  1006     type-con $field 0
  1007     bool
  1008 fun-decl $inv_is_approved_by_ptr 6 1
  1009     type-con $state 0
  1010     type-con $state 0
  1011     type-con $ptr 0
  1012     type-con $ptr 0
  1013     type-con $field 0
  1014     bool
  1015   attribute inline 1
  1016     expr-attr
  1017       true
  1018 fun-decl $inv_is_approved_by 6 1
  1019     type-con $state 0
  1020     type-con $state 0
  1021     type-con $ptr 0
  1022     type-con $field 0
  1023     type-con $field 0
  1024     bool
  1025   attribute inline 1
  1026     expr-attr
  1027       true
  1028 fun-decl $is_owner_approved 3 0
  1029     type-con $ctype 0
  1030     type-con $field 0
  1031     bool
  1032 fun-decl $inv_is_owner_approved 5 1
  1033     type-con $state 0
  1034     type-con $state 0
  1035     type-con $ptr 0
  1036     type-con $field 0
  1037     bool
  1038   attribute inline 1
  1039     expr-attr
  1040       true
  1041 fun-decl $good_for_admissibility 2 0
  1042     type-con $state 0
  1043     bool
  1044 fun-decl $good_for_post_admissibility 2 0
  1045     type-con $state 0
  1046     bool
  1047 fun-decl $stuttering_pre 3 1
  1048     type-con $state 0
  1049     type-con $ptr 0
  1050     bool
  1051   attribute inline 1
  1052     expr-attr
  1053       true
  1054 fun-decl $admissibility_pre 3 1
  1055     type-con $state 0
  1056     type-con $ptr 0
  1057     bool
  1058   attribute inline 1
  1059     expr-attr
  1060       true
  1061 fun-decl $mutable_increases 3 1
  1062     type-con $state 0
  1063     type-con $state 0
  1064     bool
  1065   attribute inline 1
  1066     expr-attr
  1067       true
  1068 fun-decl $meta_eq 3 1
  1069     type-con $state 0
  1070     type-con $state 0
  1071     bool
  1072   attribute inline 1
  1073     expr-attr
  1074       true
  1075 fun-decl $is_stuttering_check 1 0
  1076     bool
  1077 fun-decl $is_unwrap_check 1 0
  1078     bool
  1079 fun-decl $is_admissibility_check 1 1
  1080     bool
  1081   attribute inline 1
  1082     expr-attr
  1083       true
  1084 fun-decl $good_for_pre_can_unwrap 2 0
  1085     type-con $state 0
  1086     bool
  1087 fun-decl $good_for_post_can_unwrap 2 0
  1088     type-con $state 0
  1089     bool
  1090 fun-decl $unwrap_check_pre 3 1
  1091     type-con $state 0
  1092     type-con $ptr 0
  1093     bool
  1094   attribute inline 1
  1095     expr-attr
  1096       true
  1097 fun-decl $update_int 4 0
  1098     type-con $state 0
  1099     type-con $ptr 0
  1100     int
  1101     type-con $state 0
  1102 fun-decl $timestamp_is_now 3 1
  1103     type-con $state 0
  1104     type-con $ptr 0
  1105     bool
  1106   attribute inline 1
  1107     expr-attr
  1108       true
  1109 fun-decl $now_writable 3 1
  1110     type-con $state 0
  1111     type-con $ptr 0
  1112     bool
  1113   attribute inline 1
  1114     expr-attr
  1115       true
  1116 fun-decl $timestamp_post 3 1
  1117     type-con $state 0
  1118     type-con $state 0
  1119     bool
  1120   attribute inline 1
  1121     expr-attr
  1122       true
  1123 fun-decl $timestamp_post_strict 3 1
  1124     type-con $state 0
  1125     type-con $state 0
  1126     bool
  1127   attribute inline 1
  1128     expr-attr
  1129       true
  1130 fun-decl $pre_wrap 2 0
  1131     type-con $state 0
  1132     bool
  1133 fun-decl $pre_unwrap 2 0
  1134     type-con $state 0
  1135     bool
  1136 fun-decl $pre_static_wrap 2 0
  1137     type-con $state 0
  1138     bool
  1139 fun-decl $pre_static_unwrap 2 0
  1140     type-con $state 0
  1141     bool
  1142 fun-decl $unwrap_post 5 1
  1143     type-con $state 0
  1144     type-con $state 0
  1145     type-con $ptr 0
  1146     type-con $ptr 0
  1147     bool
  1148   attribute inline 1
  1149     expr-attr
  1150       true
  1151 fun-decl $unwrap_post_claimable 5 1
  1152     type-con $state 0
  1153     type-con $state 0
  1154     type-con $ptr 0
  1155     type-con $ptr 0
  1156     bool
  1157   attribute inline 1
  1158     expr-attr
  1159       true
  1160 fun-decl $keeps 4 2
  1161     type-con $state 0
  1162     type-con $ptr 0
  1163     type-con $ptr 0
  1164     bool
  1165   attribute inline 1
  1166     expr-attr
  1167       true
  1168   attribute expand 1
  1169     expr-attr
  1170       true
  1171 fun-decl $expect_unreachable 1 0
  1172     bool
  1173 fun-decl $taken_over 4 0
  1174     type-con $state 0
  1175     type-con $ptr 0
  1176     type-con $ptr 0
  1177     type-con $status 0
  1178 fun-decl $take_over 4 0
  1179     type-con $state 0
  1180     type-con $ptr 0
  1181     type-con $ptr 0
  1182     type-con $state 0
  1183 fun-decl $released 4 0
  1184     type-con $state 0
  1185     type-con $ptr 0
  1186     type-con $ptr 0
  1187     type-con $status 0
  1188 fun-decl $release 5 0
  1189     type-con $state 0
  1190     type-con $state 0
  1191     type-con $ptr 0
  1192     type-con $ptr 0
  1193     type-con $state 0
  1194 fun-decl $post_unwrap 3 0
  1195     type-con $state 0
  1196     type-con $state 0
  1197     bool
  1198 fun-decl $new_ownees 4 1
  1199     type-con $state 0
  1200     type-con $ptr 0
  1201     type-con $ptrset 0
  1202     type-con $ptrset 0
  1203   attribute inline 1
  1204     expr-attr
  1205       true
  1206 fun-decl $get_memory_allocator 1 0
  1207     type-con $ptr 0
  1208 fun-decl $memory_allocator_type 1 1
  1209     type-con $ctype 0
  1210   attribute unique 0
  1211 fun-decl $memory_allocator_ref 1 0
  1212     int
  1213 fun-decl $program_entry_point 2 0
  1214     type-con $state 0
  1215     bool
  1216 fun-decl $program_entry_point_ch 2 0
  1217     type-con $state 0
  1218     bool
  1219 fun-decl $is_global 3 1
  1220     type-con $ptr 0
  1221     type-con $ctype 0
  1222     bool
  1223   attribute inline 1
  1224     expr-attr
  1225       true
  1226 fun-decl $is_global_array 4 1
  1227     type-con $ptr 0
  1228     type-con $ctype 0
  1229     int
  1230     bool
  1231   attribute inline 1
  1232     expr-attr
  1233       true
  1234 fun-decl $active_option 3 1
  1235     type-con $state 0
  1236     type-con $ptr 0
  1237     type-con $field 0
  1238   attribute inline 1
  1239     expr-attr
  1240       true
  1241 fun-decl $ts_active_option 2 0
  1242     type-con $type_state 0
  1243     type-con $field 0
  1244 fun-decl $union_active 4 1
  1245     type-con $state 0
  1246     type-con $ptr 0
  1247     type-con $field 0
  1248     bool
  1249   attribute inline 1
  1250     expr-attr
  1251       true
  1252 fun-decl $is_union_field 3 0
  1253     type-con $ctype 0
  1254     type-con $field 0
  1255     bool
  1256 fun-decl $union_havoced 4 1
  1257     type-con $state 0
  1258     type-con $state 0
  1259     type-con $ptr 0
  1260     bool
  1261   attribute inline 1
  1262     expr-attr
  1263       true
  1264 fun-decl $full_extent 2 0
  1265     type-con $ptr 0
  1266     type-con $ptrset 0
  1267 fun-decl $extent 3 0
  1268     type-con $state 0
  1269     type-con $ptr 0
  1270     type-con $ptrset 0
  1271 fun-decl $span 2 0
  1272     type-con $ptr 0
  1273     type-con $ptrset 0
  1274 fun-decl $in_span_of 3 1
  1275     type-con $ptr 0
  1276     type-con $ptr 0
  1277     bool
  1278   attribute inline 1
  1279     expr-attr
  1280       true
  1281 fun-decl $first_option_typed 3 0
  1282     type-con $state 0
  1283     type-con $ptr 0
  1284     bool
  1285 fun-decl $struct_extent 2 1
  1286     type-con $ptr 0
  1287     type-con $ptrset 0
  1288   attribute inline 1
  1289     expr-attr
  1290       true
  1291 fun-decl $in_struct_extent_of 3 1
  1292     type-con $ptr 0
  1293     type-con $ptr 0
  1294     bool
  1295   attribute inline 1
  1296     expr-attr
  1297       true
  1298 fun-decl $volatile_span 3 0
  1299     type-con $state 0
  1300     type-con $ptr 0
  1301     type-con $ptrset 0
  1302 fun-decl $left_split 3 0
  1303     type-con $ptr 0
  1304     int
  1305     type-con $ptr 0
  1306 fun-decl $right_split 3 0
  1307     type-con $ptr 0
  1308     int
  1309     type-con $ptr 0
  1310 fun-decl $joined_array 3 0
  1311     type-con $ptr 0
  1312     type-con $ptr 0
  1313     type-con $ptr 0
  1314 fun-decl $mutable_root 3 1
  1315     type-con $state 0
  1316     type-con $ptr 0
  1317     bool
  1318   attribute inline 1
  1319     expr-attr
  1320       true
  1321 fun-decl $set_in 3 0
  1322     type-con $ptr 0
  1323     type-con $ptrset 0
  1324     bool
  1325 fun-decl $set_empty 1 0
  1326     type-con $ptrset 0
  1327 fun-decl $set_singleton 2 0
  1328     type-con $ptr 0
  1329     type-con $ptrset 0
  1330 fun-decl $non_null_set_singleton 2 0
  1331     type-con $ptr 0
  1332     type-con $ptrset 0
  1333 fun-decl $set_union 3 0
  1334     type-con $ptrset 0
  1335     type-con $ptrset 0
  1336     type-con $ptrset 0
  1337 fun-decl $set_difference 3 0
  1338     type-con $ptrset 0
  1339     type-con $ptrset 0
  1340     type-con $ptrset 0
  1341 fun-decl $set_intersection 3 0
  1342     type-con $ptrset 0
  1343     type-con $ptrset 0
  1344     type-con $ptrset 0
  1345 fun-decl $set_subset 3 0
  1346     type-con $ptrset 0
  1347     type-con $ptrset 0
  1348     bool
  1349 fun-decl $set_eq 3 0
  1350     type-con $ptrset 0
  1351     type-con $ptrset 0
  1352     bool
  1353 fun-decl $set_cardinality 2 0
  1354     type-con $ptrset 0
  1355     int
  1356 fun-decl $set_universe 1 0
  1357     type-con $ptrset 0
  1358 fun-decl $set_disjoint 3 0
  1359     type-con $ptrset 0
  1360     type-con $ptrset 0
  1361     bool
  1362 fun-decl $id_set_disjoint 4 0
  1363     type-con $ptr 0
  1364     type-con $ptrset 0
  1365     type-con $ptrset 0
  1366     int
  1367 fun-decl $set_in3 3 0
  1368     type-con $ptr 0
  1369     type-con $ptrset 0
  1370     bool
  1371 fun-decl $set_in2 3 0
  1372     type-con $ptr 0
  1373     type-con $ptrset 0
  1374     bool
  1375 fun-decl $in_some_owns 2 0
  1376     type-con $ptr 0
  1377     bool
  1378 fun-decl $set_in0 3 0
  1379     type-con $ptr 0
  1380     type-con $ptrset 0
  1381     bool
  1382 fun-decl sk_hack 2 0
  1383     bool
  1384     bool
  1385 fun-decl $writes_nothing 3 1
  1386     type-con $state 0
  1387     type-con $state 0
  1388     bool
  1389   attribute inline 1
  1390     expr-attr
  1391       true
  1392 fun-decl $array 3 0
  1393     type-con $ctype 0
  1394     int
  1395     type-con $ctype 0
  1396 fun-decl $element_type 2 0
  1397     type-con $ctype 0
  1398     type-con $ctype 0
  1399 fun-decl $array_length 2 0
  1400     type-con $ctype 0
  1401     int
  1402 fun-decl $is_array_elt 3 1
  1403     type-con $state 0
  1404     type-con $ptr 0
  1405     bool
  1406   attribute inline 1
  1407     expr-attr
  1408       true
  1409 fun-decl $inlined_array 3 1
  1410     type-con $ptr 0
  1411     type-con $ctype 0
  1412     type-con $ptr 0
  1413   attribute weight 1
  1414     expr-attr
  1415       int-num 0
  1416 fun-decl $idx 4 0
  1417     type-con $ptr 0
  1418     int
  1419     type-con $ctype 0
  1420     type-con $ptr 0
  1421 fun-decl $add.mul 4 2
  1422     int
  1423     int
  1424     int
  1425     int
  1426   attribute inline 1
  1427     expr-attr
  1428       true
  1429   attribute expand 1
  1430     expr-attr
  1431       true
  1432 fun-decl $add 3 2
  1433     int
  1434     int
  1435     int
  1436   attribute inline 1
  1437     expr-attr
  1438       true
  1439   attribute expand 1
  1440     expr-attr
  1441       true
  1442 fun-decl $is_array_vol_or_nonvol 6 1
  1443     type-con $state 0
  1444     type-con $ptr 0
  1445     type-con $ctype 0
  1446     int
  1447     bool
  1448     bool
  1449   attribute weight 1
  1450     expr-attr
  1451       int-num 0
  1452 fun-decl $is_array 5 1
  1453     type-con $state 0
  1454     type-con $ptr 0
  1455     type-con $ctype 0
  1456     int
  1457     bool
  1458   attribute weight 1
  1459     expr-attr
  1460       int-num 0
  1461 fun-decl $is_thread_local_array 5 1
  1462     type-con $state 0
  1463     type-con $ptr 0
  1464     type-con $ctype 0
  1465     int
  1466     bool
  1467   attribute inline 1
  1468     expr-attr
  1469       true
  1470 fun-decl $is_mutable_array 5 1
  1471     type-con $state 0
  1472     type-con $ptr 0
  1473     type-con $ctype 0
  1474     int
  1475     bool
  1476   attribute inline 1
  1477     expr-attr
  1478       true
  1479 fun-decl $is_array_emb 6 1
  1480     type-con $state 0
  1481     type-con $ptr 0
  1482     type-con $ctype 0
  1483     int
  1484     type-con $ptr 0
  1485     bool
  1486   attribute inline 1
  1487     expr-attr
  1488       true
  1489 fun-decl $is_array_emb_path 8 1
  1490     type-con $state 0
  1491     type-con $ptr 0
  1492     type-con $ctype 0
  1493     int
  1494     type-con $ptr 0
  1495     type-con $field 0
  1496     bool
  1497     bool
  1498   attribute inline 1
  1499     expr-attr
  1500       true
  1501 fun-decl $array_field_properties 6 1
  1502     type-con $field 0
  1503     type-con $ctype 0
  1504     int
  1505     bool
  1506     bool
  1507     bool
  1508   attribute inline 1
  1509     expr-attr
  1510       true
  1511 fun-decl $no_inline_array_field_properties 6 1
  1512     type-con $field 0
  1513     type-con $ctype 0
  1514     int
  1515     bool
  1516     bool
  1517     bool
  1518   attribute inline 1
  1519     expr-attr
  1520       true
  1521 fun-decl $array_elt_emb 4 1
  1522     type-con $state 0
  1523     type-con $ptr 0
  1524     type-con $ptr 0
  1525     bool
  1526   attribute inline 1
  1527     expr-attr
  1528       true
  1529 fun-decl $array_members 4 0
  1530     type-con $ptr 0
  1531     type-con $ctype 0
  1532     int
  1533     type-con $ptrset 0
  1534 fun-decl $array_range 4 0
  1535     type-con $ptr 0
  1536     type-con $ctype 0
  1537     int
  1538     type-con $ptrset 0
  1539 fun-decl $non_null_array_range 4 0
  1540     type-con $ptr 0
  1541     type-con $ctype 0
  1542     int
  1543     type-con $ptrset 0
  1544 fun-decl $non_null_extent 3 0
  1545     type-con $state 0
  1546     type-con $ptr 0
  1547     type-con $ptrset 0
  1548 fun-decl $as_array 4 1
  1549     type-con $ptr 0
  1550     type-con $ctype 0
  1551     int
  1552     type-con $ptr 0
  1553   attribute inline 1
  1554     expr-attr
  1555       true
  1556 fun-decl $array_eq 6 1
  1557     type-con $state 0
  1558     type-con $state 0
  1559     type-con $ptr 0
  1560     type-con $ctype 0
  1561     int
  1562     bool
  1563   attribute inline 1
  1564     expr-attr
  1565       true
  1566 fun-decl $index_within 3 0
  1567     type-con $ptr 0
  1568     type-con $ptr 0
  1569     int
  1570 fun-decl $in_array 5 1
  1571     type-con $ptr 0
  1572     type-con $ptr 0
  1573     type-con $ctype 0
  1574     int
  1575     bool
  1576   attribute inline 1
  1577     expr-attr
  1578       true
  1579 fun-decl $in_array_full_extent_of 5 1
  1580     type-con $ptr 0
  1581     type-con $ptr 0
  1582     type-con $ctype 0
  1583     int
  1584     bool
  1585   attribute inline 1
  1586     expr-attr
  1587       true
  1588 fun-decl $in_array_extent_of 6 1
  1589     type-con $state 0
  1590     type-con $ptr 0
  1591     type-con $ptr 0
  1592     type-con $ctype 0
  1593     int
  1594     bool
  1595   attribute inline 1
  1596     expr-attr
  1597       true
  1598 fun-decl $in_range 4 1
  1599     int
  1600     int
  1601     int
  1602     bool
  1603   attribute inline 1
  1604     expr-attr
  1605       true
  1606 fun-decl $bool_to_int 2 1
  1607     bool
  1608     int
  1609   attribute inline 1
  1610     expr-attr
  1611       true
  1612 fun-decl $int_to_bool 2 1
  1613     int
  1614     bool
  1615   attribute inline 1
  1616     expr-attr
  1617       true
  1618 fun-decl $read_bool 3 1
  1619     type-con $state 0
  1620     type-con $ptr 0
  1621     bool
  1622   attribute inline 1
  1623     expr-attr
  1624       true
  1625 fun-decl $ite.int 4 3
  1626     bool
  1627     int
  1628     int
  1629     int
  1630   attribute external 1
  1631     string-attr ITE
  1632   attribute bvz 1
  1633     string-attr ITE
  1634   attribute bvint 1
  1635     string-attr ITE
  1636 fun-decl $ite.bool 4 3
  1637     bool
  1638     bool
  1639     bool
  1640     bool
  1641   attribute external 1
  1642     string-attr ITE
  1643   attribute bvz 1
  1644     string-attr ITE
  1645   attribute bvint 1
  1646     string-attr ITE
  1647 fun-decl $ite.ptr 4 3
  1648     bool
  1649     type-con $ptr 0
  1650     type-con $ptr 0
  1651     type-con $ptr 0
  1652   attribute external 1
  1653     string-attr ITE
  1654   attribute bvz 1
  1655     string-attr ITE
  1656   attribute bvint 1
  1657     string-attr ITE
  1658 fun-decl $ite.struct 4 3
  1659     bool
  1660     type-con $struct 0
  1661     type-con $struct 0
  1662     type-con $struct 0
  1663   attribute external 1
  1664     string-attr ITE
  1665   attribute bvz 1
  1666     string-attr ITE
  1667   attribute bvint 1
  1668     string-attr ITE
  1669 fun-decl $ite.ptrset 4 3
  1670     bool
  1671     type-con $ptrset 0
  1672     type-con $ptrset 0
  1673     type-con $ptrset 0
  1674   attribute external 1
  1675     string-attr ITE
  1676   attribute bvz 1
  1677     string-attr ITE
  1678   attribute bvint 1
  1679     string-attr ITE
  1680 fun-decl $ite.primitive 4 3
  1681     bool
  1682     type-con $primitive 0
  1683     type-con $primitive 0
  1684     type-con $primitive 0
  1685   attribute external 1
  1686     string-attr ITE
  1687   attribute bvz 1
  1688     string-attr ITE
  1689   attribute bvint 1
  1690     string-attr ITE
  1691 fun-decl $ite.record 4 3
  1692     bool
  1693     type-con $record 0
  1694     type-con $record 0
  1695     type-con $record 0
  1696   attribute external 1
  1697     string-attr ITE
  1698   attribute bvz 1
  1699     string-attr ITE
  1700   attribute bvint 1
  1701     string-attr ITE
  1702 fun-decl $bool_id 2 1
  1703     bool
  1704     bool
  1705   attribute weight 1
  1706     expr-attr
  1707       int-num 0
  1708 fun-decl $min.i1 1 0
  1709     int
  1710 fun-decl $max.i1 1 0
  1711     int
  1712 fun-decl $min.i2 1 0
  1713     int
  1714 fun-decl $max.i2 1 0
  1715     int
  1716 fun-decl $min.i4 1 0
  1717     int
  1718 fun-decl $max.i4 1 0
  1719     int
  1720 fun-decl $min.i8 1 0
  1721     int
  1722 fun-decl $max.i8 1 0
  1723     int
  1724 fun-decl $max.u1 1 0
  1725     int
  1726 fun-decl $max.u2 1 0
  1727     int
  1728 fun-decl $max.u4 1 0
  1729     int
  1730 fun-decl $max.u8 1 0
  1731     int
  1732 fun-decl $in_range_i1 2 1
  1733     int
  1734     bool
  1735   attribute inline 1
  1736     expr-attr
  1737       true
  1738 fun-decl $in_range_i2 2 1
  1739     int
  1740     bool
  1741   attribute inline 1
  1742     expr-attr
  1743       true
  1744 fun-decl $in_range_i4 2 1
  1745     int
  1746     bool
  1747   attribute inline 1
  1748     expr-attr
  1749       true
  1750 fun-decl $in_range_i8 2 1
  1751     int
  1752     bool
  1753   attribute inline 1
  1754     expr-attr
  1755       true
  1756 fun-decl $in_range_u1 2 1
  1757     int
  1758     bool
  1759   attribute inline 1
  1760     expr-attr
  1761       true
  1762 fun-decl $in_range_u2 2 1
  1763     int
  1764     bool
  1765   attribute inline 1
  1766     expr-attr
  1767       true
  1768 fun-decl $in_range_u4 2 1
  1769     int
  1770     bool
  1771   attribute inline 1
  1772     expr-attr
  1773       true
  1774 fun-decl $in_range_u8 2 1
  1775     int
  1776     bool
  1777   attribute inline 1
  1778     expr-attr
  1779       true
  1780 fun-decl $in_range_div_i1 3 1
  1781     int
  1782     int
  1783     bool
  1784   attribute inline 1
  1785     expr-attr
  1786       true
  1787 fun-decl $in_range_div_i2 3 1
  1788     int
  1789     int
  1790     bool
  1791   attribute inline 1
  1792     expr-attr
  1793       true
  1794 fun-decl $in_range_div_i4 3 1
  1795     int
  1796     int
  1797     bool
  1798   attribute inline 1
  1799     expr-attr
  1800       true
  1801 fun-decl $in_range_div_i8 3 1
  1802     int
  1803     int
  1804     bool
  1805   attribute inline 1
  1806     expr-attr
  1807       true
  1808 fun-decl $read_i1 3 1
  1809     type-con $state 0
  1810     type-con $ptr 0
  1811     int
  1812   attribute weight 1
  1813     expr-attr
  1814       int-num 0
  1815 fun-decl $read_i2 3 1
  1816     type-con $state 0
  1817     type-con $ptr 0
  1818     int
  1819   attribute weight 1
  1820     expr-attr
  1821       int-num 0
  1822 fun-decl $read_i4 3 1
  1823     type-con $state 0
  1824     type-con $ptr 0
  1825     int
  1826   attribute weight 1
  1827     expr-attr
  1828       int-num 0
  1829 fun-decl $read_i8 3 1
  1830     type-con $state 0
  1831     type-con $ptr 0
  1832     int
  1833   attribute weight 1
  1834     expr-attr
  1835       int-num 0
  1836 fun-decl $read_u1 3 1
  1837     type-con $state 0
  1838     type-con $ptr 0
  1839     int
  1840   attribute weight 1
  1841     expr-attr
  1842       int-num 0
  1843 fun-decl $read_u2 3 1
  1844     type-con $state 0
  1845     type-con $ptr 0
  1846     int
  1847   attribute weight 1
  1848     expr-attr
  1849       int-num 0
  1850 fun-decl $read_u4 3 1
  1851     type-con $state 0
  1852     type-con $ptr 0
  1853     int
  1854   attribute weight 1
  1855     expr-attr
  1856       int-num 0
  1857 fun-decl $read_u8 3 1
  1858     type-con $state 0
  1859     type-con $ptr 0
  1860     int
  1861   attribute weight 1
  1862     expr-attr
  1863       int-num 0
  1864 fun-decl $ptr_to_u8 2 0
  1865     type-con $ptr 0
  1866     int
  1867 fun-decl $ptr_to_i8 2 0
  1868     type-con $ptr 0
  1869     int
  1870 fun-decl $ptr_to_u4 2 0
  1871     type-con $ptr 0
  1872     int
  1873 fun-decl $ptr_to_i4 2 0
  1874     type-con $ptr 0
  1875     int
  1876 fun-decl $u8_to_ptr 2 1
  1877     int
  1878     type-con $ptr 0
  1879   attribute inline 1
  1880     expr-attr
  1881       true
  1882 fun-decl $i8_to_ptr 2 1
  1883     int
  1884     type-con $ptr 0
  1885   attribute inline 1
  1886     expr-attr
  1887       true
  1888 fun-decl $u4_to_ptr 2 1
  1889     int
  1890     type-con $ptr 0
  1891   attribute inline 1
  1892     expr-attr
  1893       true
  1894 fun-decl $i4_to_ptr 2 1
  1895     int
  1896     type-con $ptr 0
  1897   attribute inline 1
  1898     expr-attr
  1899       true
  1900 fun-decl $byte_ptr_subtraction 3 1
  1901     type-con $ptr 0
  1902     type-con $ptr 0
  1903     int
  1904   attribute weight 1
  1905     expr-attr
  1906       int-num 0
  1907 fun-decl $_pow2 2 0
  1908     int
  1909     int
  1910 fun-decl $_or 4 0
  1911     type-con $ctype 0
  1912     int
  1913     int
  1914     int
  1915 fun-decl $_xor 4 0
  1916     type-con $ctype 0
  1917     int
  1918     int
  1919     int
  1920 fun-decl $_and 4 0
  1921     type-con $ctype 0
  1922     int
  1923     int
  1924     int
  1925 fun-decl $_not 3 0
  1926     type-con $ctype 0
  1927     int
  1928     int
  1929 fun-decl $unchk_add 4 1
  1930     type-con $ctype 0
  1931     int
  1932     int
  1933     int
  1934   attribute weight 1
  1935     expr-attr
  1936       int-num 0
  1937 fun-decl $unchk_sub 4 1
  1938     type-con $ctype 0
  1939     int
  1940     int
  1941     int
  1942   attribute weight 1
  1943     expr-attr
  1944       int-num 0
  1945 fun-decl $unchk_mul 4 1
  1946     type-con $ctype 0
  1947     int
  1948     int
  1949     int
  1950   attribute weight 1
  1951     expr-attr
  1952       int-num 0
  1953 fun-decl $unchk_div 4 1
  1954     type-con $ctype 0
  1955     int
  1956     int
  1957     int
  1958   attribute weight 1
  1959     expr-attr
  1960       int-num 0
  1961 fun-decl $unchk_mod 4 1
  1962     type-con $ctype 0
  1963     int
  1964     int
  1965     int
  1966   attribute weight 1
  1967     expr-attr
  1968       int-num 0
  1969 fun-decl $_shl 4 1
  1970     type-con $ctype 0
  1971     int
  1972     int
  1973     int
  1974   attribute weight 1
  1975     expr-attr
  1976       int-num 0
  1977 fun-decl $_shr 3 1
  1978     int
  1979     int
  1980     int
  1981   attribute weight 1
  1982     expr-attr
  1983       int-num 0
  1984 fun-decl $bv_extract_signed 5 0
  1985     int
  1986     int
  1987     int
  1988     int
  1989     int
  1990 fun-decl $bv_extract_unsigned 5 0
  1991     int
  1992     int
  1993     int
  1994     int
  1995     int
  1996 fun-decl $bv_update 6 0
  1997     int
  1998     int
  1999     int
  2000     int
  2001     int
  2002     int
  2003 fun-decl $unchecked 3 0
  2004     type-con $ctype 0
  2005     int
  2006     int
  2007 fun-decl $in_range_t 3 0
  2008     type-con $ctype 0
  2009     int
  2010     bool
  2011 fun-decl $_mul 3 1
  2012     int
  2013     int
  2014     int
  2015   attribute weight 1
  2016     expr-attr
  2017       int-num 0
  2018 fun-decl $get_string_literal 3 0
  2019     int
  2020     int
  2021     type-con $ptr 0
  2022 fun-decl $get_fnptr 3 0
  2023     int
  2024     type-con $ctype 0
  2025     type-con $ptr 0
  2026 fun-decl $get_fnptr_ref 2 0
  2027     int
  2028     int
  2029 fun-decl $get_fnptr_inv 2 0
  2030     int
  2031     int
  2032 fun-decl $is_fnptr_type 2 0
  2033     type-con $ctype 0
  2034     bool
  2035 fun-decl $is_math_type 2 0
  2036     type-con $ctype 0
  2037     bool
  2038 fun-decl $claims_obj 3 0
  2039     type-con $ptr 0
  2040     type-con $ptr 0
  2041     bool
  2042 fun-decl $valid_claim 3 0
  2043     type-con $state 0
  2044     type-con $ptr 0
  2045     bool
  2046 fun-decl $claim_initial_assumptions 4 1
  2047     type-con $state 0
  2048     type-con $ptr 0
  2049     type-con $token 0
  2050     bool
  2051   attribute inline 1
  2052     expr-attr
  2053       true
  2054 fun-decl $claim_transitivity_assumptions 5 1
  2055     type-con $state 0
  2056     type-con $state 0
  2057     type-con $ptr 0
  2058     type-con $token 0
  2059     bool
  2060   attribute inline 1
  2061     expr-attr
  2062       true
  2063 fun-decl $valid_claim_impl 3 1
  2064     type-con $state 0
  2065     type-con $state 0
  2066     bool
  2067   attribute inline 1
  2068     expr-attr
  2069       true
  2070 fun-decl $claims_claim 3 0
  2071     type-con $ptr 0
  2072     type-con $ptr 0
  2073     bool
  2074 fun-decl $not_shared 3 1
  2075     type-con $state 0
  2076     type-con $ptr 0
  2077     bool
  2078   attribute weight 1
  2079     expr-attr
  2080       int-num 0
  2081 fun-decl $claimed_closed 3 1
  2082     type-con $state 0
  2083     type-con $ptr 0
  2084     bool
  2085   attribute weight 1
  2086     expr-attr
  2087       int-num 0
  2088 fun-decl $no_claim 1 1
  2089     type-con $ptr 0
  2090   attribute unique 0
  2091 fun-decl $ref_cnt 3 1
  2092     type-con $state 0
  2093     type-con $ptr 0
  2094     int
  2095   attribute weight 1
  2096     expr-attr
  2097       int-num 0
  2098 fun-decl $is_claimable 2 0
  2099     type-con $ctype 0
  2100     bool
  2101 fun-decl $is_thread_local_storage 2 0
  2102     type-con $ctype 0
  2103     bool
  2104 fun-decl $frame_level 2 0
  2105     type-con $pure_function 0
  2106     int
  2107 fun-decl $current_frame_level 1 0
  2108     int
  2109 fun-decl $can_use_all_frame_axioms 2 1
  2110     type-con $state 0
  2111     bool
  2112   attribute inline 1
  2113     expr-attr
  2114       true
  2115 fun-decl $can_use_frame_axiom_of 2 1
  2116     type-con $pure_function 0
  2117     bool
  2118   attribute inline 1
  2119     expr-attr
  2120       true
  2121 fun-decl $reads_check_pre 2 0
  2122     type-con $state 0
  2123     bool
  2124 fun-decl $reads_check_post 2 0
  2125     type-con $state 0
  2126     bool
  2127 fun-decl $start_here 1 0
  2128     bool
  2129 fun-decl $ptrset_to_int 2 0
  2130     type-con $ptrset 0
  2131     int
  2132 fun-decl $int_to_ptrset 2 0
  2133     int
  2134     type-con $ptrset 0
  2135 fun-decl $version_to_int 2 0
  2136     type-con $version 0
  2137     int
  2138 fun-decl $int_to_version 2 0
  2139     int
  2140     type-con $version 0
  2141 fun-decl $vol_version_to_int 2 0
  2142     type-con $vol_version 0
  2143     int
  2144 fun-decl $int_to_vol_version 2 0
  2145     int
  2146     type-con $vol_version 0
  2147 fun-decl $ptr_to_int 2 0
  2148     type-con $ptr 0
  2149     int
  2150 fun-decl $int_to_ptr 2 0
  2151     int
  2152     type-con $ptr 0
  2153 fun-decl $precise_test 2 0
  2154     type-con $ptr 0
  2155     bool
  2156 fun-decl $updated_only_values 4 0
  2157     type-con $state 0
  2158     type-con $state 0
  2159     type-con $ptrset 0
  2160     bool
  2161 fun-decl $updated_only_domains 4 0
  2162     type-con $state 0
  2163     type-con $state 0
  2164     type-con $ptrset 0
  2165     bool
  2166 fun-decl $domain_updated_at 5 0
  2167     type-con $state 0
  2168     type-con $state 0
  2169     type-con $ptr 0
  2170     type-con $ptrset 0
  2171     bool
  2172 fun-decl l#public 1 1
  2173     type-con $label 0
  2174   attribute unique 0
  2175 fun-decl #tok$1^16.24 1 1
  2176     type-con $token 0
  2177   attribute unique 0
  2178 fun-decl #tok$1^24.47 1 1
  2179     type-con $token 0
  2180   attribute unique 0
  2181 fun-decl #tok$1^23.7 1 1
  2182     type-con $token 0
  2183   attribute unique 0
  2184 fun-decl #tok$1^16.3 1 1
  2185     type-con $token 0
  2186   attribute unique 0
  2187 fun-decl #loc.p 1 1
  2188     type-con $token 0
  2189   attribute unique 0
  2190 fun-decl #tok$1^16.8 1 1
  2191     type-con $token 0
  2192   attribute unique 0
  2193 fun-decl #loc.witness 1 1
  2194     type-con $token 0
  2195   attribute unique 0
  2196 fun-decl #tok$1^14.3 1 1
  2197     type-con $token 0
  2198   attribute unique 0
  2199 fun-decl #loc.max 1 1
  2200     type-con $token 0
  2201   attribute unique 0
  2202 fun-decl #tok$1^12.3 1 1
  2203     type-con $token 0
  2204   attribute unique 0
  2205 fun-decl #loc.len 1 1
  2206     type-con $token 0
  2207   attribute unique 0
  2208 fun-decl #distTp1 1 1
  2209     type-con $ctype 0
  2210   attribute unique 0
  2211 fun-decl #loc.arr 1 1
  2212     type-con $token 0
  2213   attribute unique 0
  2214 fun-decl #tok$1^6.1 1 1
  2215     type-con $token 0
  2216   attribute unique 0
  2217 fun-decl #file^Z?3A?5CC?5Cmax.c 1 1
  2218     type-con $token 0
  2219   attribute unique 0
  2220 axiom 0
  2221     =
  2222     fun $sizeof 1
  2223     fun ^^i1 0
  2224     int-num 1
  2225 axiom 0
  2226     =
  2227     fun $sizeof 1
  2228     fun ^^i2 0
  2229     int-num 2
  2230 axiom 0
  2231     =
  2232     fun $sizeof 1
  2233     fun ^^i4 0
  2234     int-num 4
  2235 axiom 0
  2236     =
  2237     fun $sizeof 1
  2238     fun ^^i8 0
  2239     int-num 8
  2240 axiom 0
  2241     =
  2242     fun $sizeof 1
  2243     fun ^^u1 0
  2244     int-num 1
  2245 axiom 0
  2246     =
  2247     fun $sizeof 1
  2248     fun ^^u2 0
  2249     int-num 2
  2250 axiom 0
  2251     =
  2252     fun $sizeof 1
  2253     fun ^^u4 0
  2254     int-num 4
  2255 axiom 0
  2256     =
  2257     fun $sizeof 1
  2258     fun ^^u8 0
  2259     int-num 8
  2260 axiom 0
  2261     =
  2262     fun $sizeof 1
  2263     fun ^^f4 0
  2264     int-num 4
  2265 axiom 0
  2266     =
  2267     fun $sizeof 1
  2268     fun ^^f8 0
  2269     int-num 8
  2270 axiom 0
  2271     =
  2272     fun $sizeof 1
  2273     fun ^$#thread_id_t 0
  2274     int-num 1
  2275 axiom 0
  2276     =
  2277     fun $sizeof 1
  2278     fun ^$#ptrset 0
  2279     int-num 1
  2280 axiom 0
  2281     =
  2282     fun $ptr_level 1
  2283     fun ^^i1 0
  2284     int-num 0
  2285 axiom 0
  2286     =
  2287     fun $ptr_level 1
  2288     fun ^^i2 0
  2289     int-num 0
  2290 axiom 0
  2291     =
  2292     fun $ptr_level 1
  2293     fun ^^i4 0
  2294     int-num 0
  2295 axiom 0
  2296     =
  2297     fun $ptr_level 1
  2298     fun ^^i8 0
  2299     int-num 0
  2300 axiom 0
  2301     =
  2302     fun $ptr_level 1
  2303     fun ^^u1 0
  2304     int-num 0
  2305 axiom 0
  2306     =
  2307     fun $ptr_level 1
  2308     fun ^^u2 0
  2309     int-num 0
  2310 axiom 0
  2311     =
  2312     fun $ptr_level 1
  2313     fun ^^u4 0
  2314     int-num 0
  2315 axiom 0
  2316     =
  2317     fun $ptr_level 1
  2318     fun ^^u8 0
  2319     int-num 0
  2320 axiom 0
  2321     =
  2322     fun $ptr_level 1
  2323     fun ^^f4 0
  2324     int-num 0
  2325 axiom 0
  2326     =
  2327     fun $ptr_level 1
  2328     fun ^^f8 0
  2329     int-num 0
  2330 axiom 0
  2331     =
  2332     fun $ptr_level 1
  2333     fun ^^mathint 0
  2334     int-num 0
  2335 axiom 0
  2336     =
  2337     fun $ptr_level 1
  2338     fun ^^bool 0
  2339     int-num 0
  2340 axiom 0
  2341     =
  2342     fun $ptr_level 1
  2343     fun ^^void 0
  2344     int-num 0
  2345 axiom 0
  2346     =
  2347     fun $ptr_level 1
  2348     fun ^^claim 0
  2349     int-num 0
  2350 axiom 0
  2351     =
  2352     fun $ptr_level 1
  2353     fun ^^root_emb 0
  2354     int-num 0
  2355 axiom 0
  2356     =
  2357     fun $ptr_level 1
  2358     fun ^$#ptrset 0
  2359     int-num 0
  2360 axiom 0
  2361     =
  2362     fun $ptr_level 1
  2363     fun ^$#thread_id_t 0
  2364     int-num 0
  2365 axiom 0
  2366     =
  2367     fun $ptr_level 1
  2368     fun ^$#state_t 0
  2369     int-num 0
  2370 axiom 0
  2371     =
  2372     fun $ptr_level 1
  2373     fun ^$#struct 0
  2374     int-num 0
  2375 axiom 0
  2376     fun $is_composite 1
  2377     fun ^^claim 0
  2378 axiom 0
  2379     fun $is_composite 1
  2380     fun ^^root_emb 0
  2381 axiom 0
  2382     forall 1 1 3
  2383       var #n
  2384         type-con $ctype 0
  2385       pat 1
  2386         fun $ptr_to 1
  2387         var #n
  2388           type-con $ctype 0
  2389       attribute qid 1
  2390         string-attr VccPrelu.145:15
  2391       attribute uniqueId 1
  2392         string-attr 4
  2393       attribute bvZ3Native 1
  2394         string-attr False
  2395     =
  2396     fun $unptr_to 1
  2397     fun $ptr_to 1
  2398     var #n
  2399       type-con $ctype 0
  2400     var #n
  2401       type-con $ctype 0
  2402 axiom 0
  2403     forall 1 1 3
  2404       var #n
  2405         type-con $ctype 0
  2406       pat 1
  2407         fun $ptr_to 1
  2408         var #n
  2409           type-con $ctype 0
  2410       attribute qid 1
  2411         string-attr VccPrelu.146:15
  2412       attribute uniqueId 1
  2413         string-attr 5
  2414       attribute bvZ3Native 1
  2415         string-attr False
  2416     =
  2417     fun $sizeof 1
  2418     fun $ptr_to 1
  2419     var #n
  2420       type-con $ctype 0
  2421     int-num 8
  2422 axiom 0
  2423     forall 2 1 3
  2424       var #r
  2425         type-con $ctype 0
  2426       var #d
  2427         type-con $ctype 0
  2428       pat 1
  2429         fun $map_t 2
  2430         var #r
  2431           type-con $ctype 0
  2432         var #d
  2433           type-con $ctype 0
  2434       attribute qid 1
  2435         string-attr VccPrelu.152:15
  2436       attribute uniqueId 1
  2437         string-attr 6
  2438       attribute bvZ3Native 1
  2439         string-attr False
  2440     =
  2441     fun $map_domain 1
  2442     fun $map_t 2
  2443     var #r
  2444       type-con $ctype 0
  2445     var #d
  2446       type-con $ctype 0
  2447     var #d
  2448       type-con $ctype 0
  2449 axiom 0
  2450     forall 2 1 3
  2451       var #r
  2452         type-con $ctype 0
  2453       var #d
  2454         type-con $ctype 0
  2455       pat 1
  2456         fun $map_t 2
  2457         var #r
  2458           type-con $ctype 0
  2459         var #d
  2460           type-con $ctype 0
  2461       attribute qid 1
  2462         string-attr VccPrelu.153:15
  2463       attribute uniqueId 1
  2464         string-attr 7
  2465       attribute bvZ3Native 1
  2466         string-attr False
  2467     =
  2468     fun $map_range 1
  2469     fun $map_t 2
  2470     var #r
  2471       type-con $ctype 0
  2472     var #d
  2473       type-con $ctype 0
  2474     var #r
  2475       type-con $ctype 0
  2476 axiom 0
  2477     forall 1 1 3
  2478       var #n
  2479         type-con $ctype 0
  2480       pat 1
  2481         fun $ptr_to 1
  2482         var #n
  2483           type-con $ctype 0
  2484       attribute qid 1
  2485         string-attr VccPrelu.158:15
  2486       attribute uniqueId 1
  2487         string-attr 8
  2488       attribute bvZ3Native 1
  2489         string-attr False
  2490     =
  2491     fun $ptr_level 1
  2492     fun $ptr_to 1
  2493     var #n
  2494       type-con $ctype 0
  2495     +
  2496     fun $ptr_level 1
  2497     var #n
  2498       type-con $ctype 0
  2499     int-num 17
  2500 axiom 0
  2501     forall 2 1 3
  2502       var #r
  2503         type-con $ctype 0
  2504       var #d
  2505         type-con $ctype 0
  2506       pat 1
  2507         fun $map_t 2
  2508         var #r
  2509           type-con $ctype 0
  2510         var #d
  2511           type-con $ctype 0
  2512       attribute qid 1
  2513         string-attr VccPrelu.159:15
  2514       attribute uniqueId 1
  2515         string-attr 9
  2516       attribute bvZ3Native 1
  2517         string-attr False
  2518     =
  2519     fun $ptr_level 1
  2520     fun $map_t 2
  2521     var #r
  2522       type-con $ctype 0
  2523     var #d
  2524       type-con $ctype 0
  2525     +
  2526     fun $ptr_level 1
  2527     var #r
  2528       type-con $ctype 0
  2529     int-num 23
  2530 axiom 0
  2531     forall 1 1 4
  2532       var t
  2533         type-con $ctype 0
  2534       pat 1
  2535         fun $is_primitive 1
  2536         var t
  2537           type-con $ctype 0
  2538       attribute qid 1
  2539         string-attr VccPrelu.167:36
  2540       attribute uniqueId 1
  2541         string-attr 10
  2542       attribute bvZ3Native 1
  2543         string-attr False
  2544       attribute weight 1
  2545         expr-attr
  2546           int-num 0
  2547     =
  2548     fun $is_primitive 1
  2549     var t
  2550       type-con $ctype 0
  2551     =
  2552     fun $kind_of 1
  2553     var t
  2554       type-con $ctype 0
  2555     fun $kind_primitive 0
  2556 axiom 0
  2557     forall 1 1 4
  2558       var t
  2559         type-con $ctype 0
  2560       pat 1
  2561         fun $is_composite 1
  2562         var t
  2563           type-con $ctype 0
  2564       attribute qid 1
  2565         string-attr VccPrelu.173:36
  2566       attribute uniqueId 1
  2567         string-attr 11
  2568       attribute bvZ3Native 1
  2569         string-attr False
  2570       attribute weight 1
  2571         expr-attr
  2572           int-num 0
  2573     =
  2574     fun $is_composite 1
  2575     var t
  2576       type-con $ctype 0
  2577     =
  2578     fun $kind_of 1
  2579     var t
  2580       type-con $ctype 0
  2581     fun $kind_composite 0
  2582 axiom 0
  2583     forall 1 1 4
  2584       var t
  2585         type-con $ctype 0
  2586       pat 1
  2587         fun $is_arraytype 1
  2588         var t
  2589           type-con $ctype 0
  2590       attribute qid 1
  2591         string-attr VccPrelu.179:36
  2592       attribute uniqueId 1
  2593         string-attr 12
  2594       attribute bvZ3Native 1
  2595         string-attr False
  2596       attribute weight 1
  2597         expr-attr
  2598           int-num 0
  2599     =
  2600     fun $is_arraytype 1
  2601     var t
  2602       type-con $ctype 0
  2603     =
  2604     fun $kind_of 1
  2605     var t
  2606       type-con $ctype 0
  2607     fun $kind_array 0
  2608 axiom 0
  2609     forall 1 1 4
  2610       var t
  2611         type-con $ctype 0
  2612       pat 1
  2613         fun $is_threadtype 1
  2614         var t
  2615           type-con $ctype 0
  2616       attribute qid 1
  2617         string-attr VccPrelu.185:37
  2618       attribute uniqueId 1
  2619         string-attr 13
  2620       attribute bvZ3Native 1
  2621         string-attr False
  2622       attribute weight 1
  2623         expr-attr
  2624           int-num 0
  2625     =
  2626     fun $is_threadtype 1
  2627     var t
  2628       type-con $ctype 0
  2629     =
  2630     fun $kind_of 1
  2631     var t
  2632       type-con $ctype 0
  2633     fun $kind_thread 0
  2634 axiom 0
  2635     forall 1 1 4
  2636       var t
  2637         type-con $ctype 0
  2638       pat 1
  2639         fun $is_composite 1
  2640         var t
  2641           type-con $ctype 0
  2642       attribute qid 1
  2643         string-attr VccPrelu.198:15
  2644       attribute uniqueId 1
  2645         string-attr 14
  2646       attribute bvZ3Native 1
  2647         string-attr False
  2648       attribute weight 1
  2649         expr-attr
  2650           int-num 0
  2651     implies
  2652     fun $is_composite 1
  2653     var t
  2654       type-con $ctype 0
  2655     fun $is_non_primitive 1
  2656     var t
  2657       type-con $ctype 0
  2658 axiom 0
  2659     forall 1 1 4
  2660       var t
  2661         type-con $ctype 0
  2662       pat 1
  2663         fun $is_arraytype 1
  2664         var t
  2665           type-con $ctype 0
  2666       attribute qid 1
  2667         string-attr VccPrelu.199:15
  2668       attribute uniqueId 1
  2669         string-attr 15
  2670       attribute bvZ3Native 1
  2671         string-attr False
  2672       attribute weight 1
  2673         expr-attr
  2674           int-num 0
  2675     implies
  2676     fun $is_arraytype 1
  2677     var t
  2678       type-con $ctype 0
  2679     fun $is_non_primitive 1
  2680     var t
  2681       type-con $ctype 0
  2682 axiom 0
  2683     forall 1 1 4
  2684       var t
  2685         type-con $ctype 0
  2686       pat 1
  2687         fun $is_threadtype 1
  2688         var t
  2689           type-con $ctype 0
  2690       attribute qid 1
  2691         string-attr VccPrelu.200:15
  2692       attribute uniqueId 1
  2693         string-attr 16
  2694       attribute bvZ3Native 1
  2695         string-attr False
  2696       attribute weight 1
  2697         expr-attr
  2698           int-num 0
  2699     implies
  2700     fun $is_threadtype 1
  2701     var t
  2702       type-con $ctype 0
  2703     fun $is_non_primitive 1
  2704     var t
  2705       type-con $ctype 0
  2706 axiom 0
  2707     forall 2 1 3
  2708       var #r
  2709         type-con $ctype 0
  2710       var #d
  2711         type-con $ctype 0
  2712       pat 1
  2713         fun $map_t 2
  2714         var #r
  2715           type-con $ctype 0
  2716         var #d
  2717           type-con $ctype 0
  2718       attribute qid 1
  2719         string-attr VccPrelu.208:15
  2720       attribute uniqueId 1
  2721         string-attr 17
  2722       attribute bvZ3Native 1
  2723         string-attr False
  2724     fun $is_primitive 1
  2725     fun $map_t 2
  2726     var #r
  2727       type-con $ctype 0
  2728     var #d
  2729       type-con $ctype 0
  2730 axiom 0
  2731     forall 1 1 3
  2732       var #n
  2733         type-con $ctype 0
  2734       pat 1
  2735         fun $ptr_to 1
  2736         var #n
  2737           type-con $ctype 0
  2738       attribute qid 1
  2739         string-attr VccPrelu.209:15
  2740       attribute uniqueId 1
  2741         string-attr 18
  2742       attribute bvZ3Native 1
  2743         string-attr False
  2744     fun $is_primitive 1
  2745     fun $ptr_to 1
  2746     var #n
  2747       type-con $ctype 0
  2748 axiom 0
  2749     forall 1 1 3
  2750       var #n
  2751         type-con $ctype 0
  2752       pat 1
  2753         fun $is_primitive 1
  2754         var #n
  2755           type-con $ctype 0
  2756       attribute qid 1
  2757         string-attr VccPrelu.210:15
  2758       attribute uniqueId 1
  2759         string-attr 19
  2760       attribute bvZ3Native 1
  2761         string-attr False
  2762     implies
  2763     fun $is_primitive 1
  2764     var #n
  2765       type-con $ctype 0
  2766     not
  2767     fun $is_claimable 1
  2768     var #n
  2769       type-con $ctype 0
  2770 axiom 0
  2771     fun $is_primitive 1
  2772     fun ^^void 0
  2773 axiom 0
  2774     fun $is_primitive 1
  2775     fun ^^bool 0
  2776 axiom 0
  2777     fun $is_primitive 1
  2778     fun ^^mathint 0
  2779 axiom 0
  2780     fun $is_primitive 1
  2781     fun ^$#ptrset 0
  2782 axiom 0
  2783     fun $is_primitive 1
  2784     fun ^$#state_t 0
  2785 axiom 0
  2786     fun $is_threadtype 1
  2787     fun ^$#thread_id_t 0
  2788 axiom 0
  2789     fun $is_primitive 1
  2790     fun ^^i1 0
  2791 axiom 0
  2792     fun $is_primitive 1
  2793     fun ^^i2 0
  2794 axiom 0
  2795     fun $is_primitive 1
  2796     fun ^^i4 0
  2797 axiom 0
  2798     fun $is_primitive 1
  2799     fun ^^i8 0
  2800 axiom 0
  2801     fun $is_primitive 1
  2802     fun ^^u1 0
  2803 axiom 0
  2804     fun $is_primitive 1
  2805     fun ^^u2 0
  2806 axiom 0
  2807     fun $is_primitive 1
  2808     fun ^^u4 0
  2809 axiom 0
  2810     fun $is_primitive 1
  2811     fun ^^u8 0
  2812 axiom 0
  2813     fun $is_primitive 1
  2814     fun ^^f4 0
  2815 axiom 0
  2816     fun $is_primitive 1
  2817     fun ^^f8 0
  2818 axiom 0
  2819     =
  2820     fun $me 0
  2821     fun $ptr 2
  2822     fun ^$#thread_id_t 0
  2823     fun $me_ref 0
  2824 axiom 0
  2825     forall 3 0 4
  2826       var M
  2827         type-con $memory_t 0
  2828       var p
  2829         type-con $ptr 0
  2830       var v
  2831         int
  2832       attribute qid 1
  2833         string-attr VccPrelu.238:15
  2834       attribute uniqueId 1
  2835         string-attr 20
  2836       attribute bvZ3Native 1
  2837         string-attr False
  2838       attribute weight 1
  2839         expr-attr
  2840           int-num 0
  2841     =
  2842     fun $select.mem 2
  2843     fun $store.mem 3
  2844     var M
  2845       type-con $memory_t 0
  2846     var p
  2847       type-con $ptr 0
  2848     var v
  2849       int
  2850     var p
  2851       type-con $ptr 0
  2852     var v
  2853       int
  2854 axiom 0
  2855     forall 4 0 4
  2856       var M
  2857         type-con $memory_t 0
  2858       var p
  2859         type-con $ptr 0
  2860       var q
  2861         type-con $ptr 0
  2862       var v
  2863         int
  2864       attribute qid 1
  2865         string-attr VccPrelu.240:15
  2866       attribute uniqueId 1
  2867         string-attr 21
  2868       attribute bvZ3Native 1
  2869         string-attr False
  2870       attribute weight 1
  2871         expr-attr
  2872           int-num 0
  2873     or 2
  2874     =
  2875     var p
  2876       type-con $ptr 0
  2877     var q
  2878       type-con $ptr 0
  2879     =
  2880     fun $select.mem 2
  2881     fun $store.mem 3
  2882     var M
  2883       type-con $memory_t 0
  2884     var p
  2885       type-con $ptr 0
  2886     var v
  2887       int
  2888     var q
  2889       type-con $ptr 0
  2890     fun $select.mem 2
  2891     var M
  2892       type-con $memory_t 0
  2893     var q
  2894       type-con $ptr 0
  2895 axiom 0
  2896     forall 3 0 4
  2897       var M
  2898         type-con $typemap_t 0
  2899       var p
  2900         type-con $ptr 0
  2901       var v
  2902         type-con $type_state 0
  2903       attribute qid 1
  2904         string-attr VccPrelu.249:15
  2905       attribute uniqueId 1
  2906         string-attr 22
  2907       attribute bvZ3Native 1
  2908         string-attr False
  2909       attribute weight 1
  2910         expr-attr
  2911           int-num 0
  2912     =
  2913     fun $select.tm 2
  2914     fun $store.tm 3
  2915     var M
  2916       type-con $typemap_t 0
  2917     var p
  2918       type-con $ptr 0
  2919     var v
  2920       type-con $type_state 0
  2921     var p
  2922       type-con $ptr 0
  2923     var v
  2924       type-con $type_state 0
  2925 axiom 0
  2926     forall 4 0 4
  2927       var M
  2928         type-con $typemap_t 0
  2929       var p
  2930         type-con $ptr 0
  2931       var q
  2932         type-con $ptr 0
  2933       var v
  2934         type-con $type_state 0
  2935       attribute qid 1
  2936         string-attr VccPrelu.251:15
  2937       attribute uniqueId 1
  2938         string-attr 23
  2939       attribute bvZ3Native 1
  2940         string-attr False
  2941       attribute weight 1
  2942         expr-attr
  2943           int-num 0
  2944     or 2
  2945     =
  2946     var p
  2947       type-con $ptr 0
  2948     var q
  2949       type-con $ptr 0
  2950     =
  2951     fun $select.tm 2
  2952     fun $store.tm 3
  2953     var M
  2954       type-con $typemap_t 0
  2955     var p
  2956       type-con $ptr 0
  2957     var v
  2958       type-con $type_state 0
  2959     var q
  2960       type-con $ptr 0
  2961     fun $select.tm 2
  2962     var M
  2963       type-con $typemap_t 0
  2964     var q
  2965       type-con $ptr 0
  2966 axiom 0
  2967     forall 3 0 4
  2968       var M
  2969         type-con $statusmap_t 0
  2970       var p
  2971         type-con $ptr 0
  2972       var v
  2973         type-con $status 0
  2974       attribute qid 1
  2975         string-attr VccPrelu.260:15
  2976       attribute uniqueId 1
  2977         string-attr 24
  2978       attribute bvZ3Native 1
  2979         string-attr False
  2980       attribute weight 1
  2981         expr-attr
  2982           int-num 0
  2983     =
  2984     fun $select.sm 2
  2985     fun $store.sm 3
  2986     var M
  2987       type-con $statusmap_t 0
  2988     var p
  2989       type-con $ptr 0
  2990     var v
  2991       type-con $status 0
  2992     var p
  2993       type-con $ptr 0
  2994     var v
  2995       type-con $status 0
  2996 axiom 0
  2997     forall 4 0 4
  2998       var M
  2999         type-con $statusmap_t 0
  3000       var p
  3001         type-con $ptr 0
  3002       var q
  3003         type-con $ptr 0
  3004       var v
  3005         type-con $status 0
  3006       attribute qid 1
  3007         string-attr VccPrelu.262:15
  3008       attribute uniqueId 1
  3009         string-attr 25
  3010       attribute bvZ3Native 1
  3011         string-attr False
  3012       attribute weight 1
  3013         expr-attr
  3014           int-num 0
  3015     or 2
  3016     =
  3017     var p
  3018       type-con $ptr 0
  3019     var q
  3020       type-con $ptr 0
  3021     =
  3022     fun $select.sm 2
  3023     fun $store.sm 3
  3024     var M
  3025       type-con $statusmap_t 0
  3026     var p
  3027       type-con $ptr 0
  3028     var v
  3029       type-con $status 0
  3030     var q
  3031       type-con $ptr 0
  3032     fun $select.sm 2
  3033     var M
  3034       type-con $statusmap_t 0
  3035     var q
  3036       type-con $ptr 0
  3037 axiom 0
  3038     forall 3 1 3
  3039       var p
  3040         type-con $ptr 0
  3041       var q
  3042         type-con $ptr 0
  3043       var r
  3044         type-con $ptr 0
  3045       pat 2
  3046         fun $extent_hint 2
  3047         var p
  3048           type-con $ptr 0
  3049         var q
  3050           type-con $ptr 0
  3051         fun $extent_hint 2
  3052         var q
  3053           type-con $ptr 0
  3054         var r
  3055           type-con $ptr 0
  3056       attribute qid 1
  3057         string-attr VccPrelu.288:15
  3058       attribute uniqueId 1
  3059         string-attr 26
  3060       attribute bvZ3Native 1
  3061         string-attr False
  3062     implies
  3063     and 2
  3064     fun $extent_hint 2
  3065     var p
  3066       type-con $ptr 0
  3067     var q
  3068       type-con $ptr 0
  3069     fun $extent_hint 2
  3070     var q
  3071       type-con $ptr 0
  3072     var r
  3073       type-con $ptr 0
  3074     fun $extent_hint 2
  3075     var p
  3076       type-con $ptr 0
  3077     var r
  3078       type-con $ptr 0
  3079 axiom 0
  3080     forall 1 1 3
  3081       var p
  3082         type-con $ptr 0
  3083       pat 1
  3084         fun $typ 1
  3085         var p
  3086           type-con $ptr 0
  3087       attribute qid 1
  3088         string-attr VccPrelu.290:15
  3089       attribute uniqueId 1
  3090         string-attr 27
  3091       attribute bvZ3Native 1
  3092         string-attr False
  3093     fun $extent_hint 2
  3094     var p
  3095       type-con $ptr 0
  3096     var p
  3097       type-con $ptr 0
  3098 axiom 0
  3099     forall 4 1 3
  3100       var t
  3101         type-con $ctype 0
  3102       var s
  3103         type-con $ctype 0
  3104       var min
  3105         int
  3106       var max
  3107         int
  3108       pat 1
  3109         fun $is_nested_range 4
  3110         var t
  3111           type-con $ctype 0
  3112         var s
  3113           type-con $ctype 0
  3114         var min
  3115           int
  3116         var max
  3117           int
  3118       attribute qid 1
  3119         string-attr VccPrelu.297:27
  3120       attribute uniqueId 1
  3121         string-attr 28
  3122       attribute bvZ3Native 1
  3123         string-attr False
  3124     =
  3125     fun $is_nested_range 4
  3126     var t
  3127       type-con $ctype 0
  3128     var s
  3129       type-con $ctype 0
  3130     var min
  3131       int
  3132     var max
  3133       int
  3134     and 3
  3135     fun $is_nested 2
  3136     var t
  3137       type-con $ctype 0
  3138     var s
  3139       type-con $ctype 0
  3140     =
  3141     fun $nesting_min 2
  3142     var t
  3143       type-con $ctype 0
  3144     var s
  3145       type-con $ctype 0
  3146     var min
  3147       int
  3148     =
  3149     fun $nesting_max 2
  3150     var t
  3151       type-con $ctype 0
  3152     var s
  3153       type-con $ctype 0
  3154     var max
  3155       int
  3156 axiom 0
  3157     forall 2 0 4
  3158       var #t
  3159         type-con $ctype 0
  3160       var #b
  3161         int
  3162       attribute qid 1
  3163         string-attr VccPrelu.334:15
  3164       attribute uniqueId 1
  3165         string-attr 29
  3166       attribute bvZ3Native 1
  3167         string-attr False
  3168       attribute weight 1
  3169         expr-attr
  3170           int-num 0
  3171     =
  3172     fun $typ 1
  3173     fun $ptr 2
  3174     var #t
  3175       type-con $ctype 0
  3176     var #b
  3177       int
  3178     var #t
  3179       type-con $ctype 0
  3180 axiom 0
  3181     forall 2 0 4
  3182       var #t
  3183         type-con $ctype 0
  3184       var #b
  3185         int
  3186       attribute qid 1
  3187         string-attr VccPrelu.335:15
  3188       attribute uniqueId 1
  3189         string-attr 30
  3190       attribute bvZ3Native 1
  3191         string-attr False
  3192       attribute weight 1
  3193         expr-attr
  3194           int-num 0
  3195     =
  3196     fun $ref 1
  3197     fun $ptr 2
  3198     var #t
  3199       type-con $ctype 0
  3200     var #b
  3201       int
  3202     var #b
  3203       int
  3204 axiom 0
  3205     forall 2 1 4
  3206       var p
  3207         type-con $ptr 0
  3208       var f
  3209         type-con $field 0
  3210       pat 1
  3211         fun $ghost_ref 2
  3212         var p
  3213           type-con $ptr 0
  3214         var f
  3215           type-con $field 0
  3216       attribute qid 1
  3217         string-attr VccPrelu.344:15
  3218       attribute uniqueId 1
  3219         string-attr 31
  3220       attribute bvZ3Native 1
  3221         string-attr False
  3222       attribute weight 1
  3223         expr-attr
  3224           int-num 0
  3225     and 2
  3226     =
  3227     fun $ghost_emb 1
  3228     fun $ghost_ref 2
  3229     var p
  3230       type-con $ptr 0
  3231     var f
  3232       type-con $field 0
  3233     var p
  3234       type-con $ptr 0
  3235     =
  3236     fun $ghost_path 1
  3237     fun $ghost_ref 2
  3238     var p
  3239       type-con $ptr 0
  3240     var f
  3241       type-con $field 0
  3242     var f
  3243       type-con $field 0
  3244 axiom 0
  3245     forall 2 1 4
  3246       var fld
  3247         type-con $field 0
  3248       var off
  3249         int
  3250       pat 1
  3251         fun $array_path 2
  3252         var fld
  3253           type-con $field 0
  3254         var off
  3255           int
  3256       attribute qid 1
  3257         string-attr VccPrelu.355:15
  3258       attribute uniqueId 1
  3259         string-attr 32
  3260       attribute bvZ3Native 1
  3261         string-attr False
  3262       attribute weight 1
  3263         expr-attr
  3264           int-num 0
  3265     and 3
  3266     not
  3267     fun $is_base_field 1
  3268     fun $array_path 2
  3269     var fld
  3270       type-con $field 0
  3271     var off
  3272       int
  3273     =
  3274     fun $array_path_1 1
  3275     fun $array_path 2
  3276     var fld
  3277       type-con $field 0
  3278     var off
  3279       int
  3280     var fld
  3281       type-con $field 0
  3282     =
  3283     fun $array_path_2 1
  3284     fun $array_path 2
  3285     var fld
  3286       type-con $field 0
  3287     var off
  3288       int
  3289     var off
  3290       int
  3291 axiom 0
  3292     =
  3293     fun $null 0
  3294     fun $ptr 2
  3295     fun ^^void 0
  3296     int-num 0
  3297 axiom 0
  3298     forall 2 0 4
  3299       var #p
  3300         type-con $ptr 0
  3301       var #t
  3302         type-con $ctype 0
  3303       attribute qid 1
  3304         string-attr VccPrelu.368:15
  3305       attribute uniqueId 1
  3306         string-attr 33
  3307       attribute bvZ3Native 1
  3308         string-attr False
  3309       attribute weight 1
  3310         expr-attr
  3311           int-num 0
  3312     =
  3313     fun $is 2
  3314     var #p
  3315       type-con $ptr 0
  3316     var #t
  3317       type-con $ctype 0
  3318     =
  3319     fun $typ 1
  3320     var #p
  3321       type-con $ptr 0
  3322     var #t
  3323       type-con $ctype 0
  3324 axiom 0
  3325     forall 2 1 3
  3326       var #p
  3327         type-con $ptr 0
  3328       var #t
  3329         type-con $ctype 0
  3330       pat 1
  3331         fun $is 2
  3332         var #p
  3333           type-con $ptr 0
  3334         var #t
  3335           type-con $ctype 0
  3336       attribute qid 1
  3337         string-attr VccPrelu.370:15
  3338       attribute uniqueId 1
  3339         string-attr 34
  3340       attribute bvZ3Native 1
  3341         string-attr False
  3342     implies
  3343     fun $is 2
  3344     var #p
  3345       type-con $ptr 0
  3346     var #t
  3347       type-con $ctype 0
  3348     =
  3349     var #p
  3350       type-con $ptr 0
  3351     fun $ptr 2
  3352     var #t
  3353       type-con $ctype 0
  3354     fun $ref 1
  3355     var #p
  3356       type-con $ptr 0
  3357 axiom 0
  3358     forall 2 1 3
  3359       var r
  3360         int
  3361       var f
  3362         type-con $field 0
  3363       pat 1
  3364         fun $containing_struct 2
  3365         fun $dot 2
  3366         fun $ptr 2
  3367         fun $field_parent_type 1
  3368         var f
  3369           type-con $field 0
  3370         var r
  3371           int
  3372         var f
  3373           type-con $field 0
  3374         var f
  3375           type-con $field 0
  3376       attribute qid 1
  3377         string-attr VccPrelu.388:15
  3378       attribute uniqueId 1
  3379         string-attr 35
  3380       attribute bvZ3Native 1
  3381         string-attr False
  3382     =
  3383     fun $containing_struct 2
  3384     fun $dot 2
  3385     fun $ptr 2
  3386     fun $field_parent_type 1
  3387     var f
  3388       type-con $field 0
  3389     var r
  3390       int
  3391     var f
  3392       type-con $field 0
  3393     var f
  3394       type-con $field 0
  3395     fun $ptr 2
  3396     fun $field_parent_type 1
  3397     var f
  3398       type-con $field 0
  3399     var r
  3400       int
  3401 axiom 0
  3402     forall 2 1 3
  3403       var p
  3404         type-con $ptr 0
  3405       var f
  3406         type-con $field 0
  3407       pat 1
  3408         fun $containing_struct 2
  3409         var p
  3410           type-con $ptr 0
  3411         var f
  3412           type-con $field 0
  3413       attribute qid 1
  3414         string-attr VccPrelu.392:15
  3415       attribute uniqueId 1
  3416         string-attr 36
  3417       attribute bvZ3Native 1
  3418         string-attr False
  3419     =
  3420     fun $containing_struct 2
  3421     var p
  3422       type-con $ptr 0
  3423     var f
  3424       type-con $field 0
  3425     fun $ptr 2
  3426     fun $field_parent_type 1
  3427     var f
  3428       type-con $field 0
  3429     fun $containing_struct_ref 2
  3430     var p
  3431       type-con $ptr 0
  3432     var f
  3433       type-con $field 0
  3434 axiom 0
  3435     forall 2 1 3
  3436       var p
  3437         type-con $ptr 0
  3438       var f
  3439         type-con $field 0
  3440       pat 1
  3441         fun $dot 2
  3442         fun $containing_struct 2
  3443         var p
  3444           type-con $ptr 0
  3445         var f
  3446           type-con $field 0
  3447         var f
  3448           type-con $field 0
  3449       attribute qid 1
  3450         string-attr VccPrelu.396:15
  3451       attribute uniqueId 1
  3452         string-attr 37
  3453       attribute bvZ3Native 1
  3454         string-attr False
  3455     implies
  3456     >=
  3457     fun $field_offset 1
  3458     var f
  3459       type-con $field 0
  3460     int-num 0
  3461     =
  3462     fun $ref 1
  3463     fun $dot 2
  3464     fun $containing_struct 2
  3465     var p
  3466       type-con $ptr 0
  3467     var f
  3468       type-con $field 0
  3469     var f
  3470       type-con $field 0
  3471     fun $ref 1
  3472     var p
  3473       type-con $ptr 0
  3474 axiom 0
  3475     forall 1 1 3
  3476       var ts
  3477         type-con $type_state 0
  3478       pat 1
  3479         fun $ts_emb 1
  3480         var ts
  3481           type-con $type_state 0
  3482       attribute qid 1
  3483         string-attr VccPrelu.427:15
  3484       attribute uniqueId 1
  3485         string-attr 38
  3486       attribute bvZ3Native 1
  3487         string-attr False
  3488     and 2
  3489     not
  3490     =
  3491     fun $kind_of 1
  3492     fun $typ 1
  3493     fun $ts_emb 1
  3494     var ts
  3495       type-con $type_state 0
  3496     fun $kind_primitive 0
  3497     fun $is_non_primitive 1
  3498     fun $typ 1
  3499     fun $ts_emb 1
  3500     var ts
  3501       type-con $type_state 0
  3502 axiom 0
  3503     forall 2 1 3
  3504       var S
  3505         type-con $state 0
  3506       var p
  3507         type-con $ptr 0
  3508       pat 2
  3509         fun $typed 2
  3510         var S
  3511           type-con $state 0
  3512         var p
  3513           type-con $ptr 0
  3514         fun $select.tm 2
  3515         fun $typemap 1
  3516         var S
  3517           type-con $state 0
  3518         fun $ts_emb 1
  3519         fun $select.tm 2
  3520         fun $typemap 1
  3521         var S
  3522           type-con $state 0
  3523         var p
  3524           type-con $ptr 0
  3525       attribute qid 1
  3526         string-attr VccPrelu.430:15
  3527       attribute uniqueId 1
  3528         string-attr 39
  3529       attribute bvZ3Native 1
  3530         string-attr False
  3531     implies
  3532     fun $typed 2
  3533     var S
  3534       type-con $state 0
  3535     var p
  3536       type-con $ptr 0
  3537     fun $typed 2
  3538     var S
  3539       type-con $state 0
  3540     fun $ts_emb 1
  3541     fun $select.tm 2
  3542     fun $typemap 1
  3543     var S
  3544       type-con $state 0
  3545     var p
  3546       type-con $ptr 0
  3547 axiom 0
  3548     forall 2 1 3
  3549       var S
  3550         type-con $state 0
  3551       var p
  3552         type-con $ptr 0
  3553       pat 1
  3554         fun $ts_is_volatile 1
  3555         fun $select.tm 2
  3556         fun $typemap 1
  3557         var S
  3558           type-con $state 0
  3559         var p
  3560           type-con $ptr 0
  3561       attribute qid 1
  3562         string-attr VccPrelu.440:15
  3563       attribute uniqueId 1
  3564         string-attr 40
  3565       attribute bvZ3Native 1
  3566         string-attr False
  3567     implies
  3568     and 2
  3569     fun $good_state 1
  3570     var S
  3571       type-con $state 0
  3572     fun $ts_is_volatile 1
  3573     fun $select.tm 2
  3574     fun $typemap 1
  3575     var S
  3576       type-con $state 0
  3577     var p
  3578       type-con $ptr 0
  3579     =
  3580     fun $kind_of 1
  3581     fun $typ 1
  3582     var p
  3583       type-con $ptr 0
  3584     fun $kind_primitive 0
  3585 axiom 0
  3586     forall 2 1 4
  3587       var S
  3588         type-con $state 0
  3589       var p
  3590         type-con $ptr 0
  3591       pat 1
  3592         fun $select.sm 2
  3593         fun $statusmap 1
  3594         var S
  3595           type-con $state 0
  3596         var p
  3597           type-con $ptr 0
  3598       attribute qid 1
  3599         string-attr VccPrelu.456:15
  3600       attribute uniqueId 1
  3601         string-attr 41
  3602       attribute bvZ3Native 1
  3603         string-attr False
  3604       attribute weight 1
  3605         expr-attr
  3606           int-num 0
  3607     or 2
  3608     <=
  3609     fun $timestamp 2
  3610     var S
  3611       type-con $state 0
  3612     var p
  3613       type-con $ptr 0
  3614     fun $current_timestamp 1
  3615     var S
  3616       type-con $state 0
  3617     not
  3618     fun $ts_typed 1
  3619     fun $select.tm 2
  3620     fun $typemap 1
  3621     var S
  3622       type-con $state 0
  3623     var p
  3624       type-con $ptr 0
  3625 axiom 0
  3626     fun $good_state 1
  3627     fun $vs_state 1
  3628     fun $struct_zero 0
  3629 axiom 0
  3630     forall 1 0 3
  3631       var s
  3632         type-con $struct 0
  3633       attribute qid 1
  3634         string-attr VccPrelu.486:15
  3635       attribute uniqueId 1
  3636         string-attr 42
  3637       attribute bvZ3Native 1
  3638         string-attr False
  3639     fun $good_state 1
  3640     fun $vs_state 1
  3641     var s
  3642       type-con $struct 0
  3643 axiom 0
  3644     forall 2 1 3
  3645       var S
  3646         type-con $state 0
  3647       var p
  3648         type-con $ptr 0
  3649       pat 1
  3650         fun $vs_ctor 2
  3651         var S
  3652           type-con $state 0
  3653         var p
  3654           type-con $ptr 0
  3655       attribute qid 1
  3656         string-attr VccPrelu.489:15
  3657       attribute uniqueId 1
  3658         string-attr 43
  3659       attribute bvZ3Native 1
  3660         string-attr False
  3661     implies
  3662     fun $good_state 1
  3663     var S
  3664       type-con $state 0
  3665     and 2
  3666     =
  3667     fun $vs_base_ref 1
  3668     fun $vs_ctor 2
  3669     var S
  3670       type-con $state 0
  3671     var p
  3672       type-con $ptr 0
  3673     fun $ref 1
  3674     var p
  3675       type-con $ptr 0
  3676     =
  3677     fun $vs_state 1
  3678     fun $vs_ctor 2
  3679     var S
  3680       type-con $state 0
  3681     var p
  3682       type-con $ptr 0
  3683     var S
  3684       type-con $state 0
  3685 axiom 0
  3686     forall 6 1 3
  3687       var r
  3688         type-con $record 0
  3689       var f
  3690         type-con $field 0
  3691       var val_bitsize
  3692         int
  3693       var from
  3694         int
  3695       var to
  3696         int
  3697       var repl
  3698         int
  3699       pat 1
  3700         fun $rec_update_bv 6
  3701         var r
  3702           type-con $record 0
  3703         var f
  3704           type-con $field 0
  3705         var val_bitsize
  3706           int
  3707         var from
  3708           int
  3709         var to
  3710           int
  3711         var repl
  3712           int
  3713       attribute qid 1
  3714         string-attr VccPrelu.502:25
  3715       attribute uniqueId 1
  3716         string-attr 44
  3717       attribute bvZ3Native 1
  3718         string-attr False
  3719     =
  3720     fun $rec_update_bv 6
  3721     var r
  3722       type-con $record 0
  3723     var f
  3724       type-con $field 0
  3725     var val_bitsize
  3726       int
  3727     var from
  3728       int
  3729     var to
  3730       int
  3731     var repl
  3732       int
  3733     fun $rec_update 3
  3734     var r
  3735       type-con $record 0
  3736     var f
  3737       type-con $field 0
  3738     fun $bv_update 5
  3739     fun $rec_fetch 2
  3740     var r
  3741       type-con $record 0
  3742     var f
  3743       type-con $field 0
  3744     var val_bitsize
  3745       int
  3746     var from
  3747       int
  3748     var to
  3749       int
  3750     var repl
  3751       int
  3752 axiom 0
  3753     forall 1 0 3
  3754       var f
  3755         type-con $field 0
  3756       attribute qid 1
  3757         string-attr VccPrelu.505:15
  3758       attribute uniqueId 1
  3759         string-attr 45
  3760       attribute bvZ3Native 1
  3761         string-attr False
  3762     =
  3763     fun $rec_fetch 2
  3764     fun $rec_zero 0
  3765     var f
  3766       type-con $field 0
  3767     int-num 0
  3768 axiom 0
  3769     forall 3 1 3
  3770       var r
  3771         type-con $record 0
  3772       var f
  3773         type-con $field 0
  3774       var v
  3775         int
  3776       pat 1
  3777         fun $rec_fetch 2
  3778         fun $rec_update 3
  3779         var r
  3780           type-con $record 0
  3781         var f
  3782           type-con $field 0
  3783         var v
  3784           int
  3785         var f
  3786           type-con $field 0
  3787       attribute qid 1
  3788         string-attr VccPrelu.507:15
  3789       attribute uniqueId 1
  3790         string-attr 46
  3791       attribute bvZ3Native 1
  3792         string-attr False
  3793     =
  3794     fun $rec_fetch 2
  3795     fun $rec_update 3
  3796     var r
  3797       type-con $record 0
  3798     var f
  3799       type-con $field 0
  3800     var v
  3801       int
  3802     var f
  3803       type-con $field 0
  3804     var v
  3805       int
  3806 axiom 0
  3807     forall 4 1 3
  3808       var r
  3809         type-con $record 0
  3810       var f1
  3811         type-con $field 0
  3812       var f2
  3813         type-con $field 0
  3814       var v
  3815         int
  3816       pat 1
  3817         fun $rec_fetch 2
  3818         fun $rec_update 3
  3819         var r
  3820           type-con $record 0
  3821         var f1
  3822           type-con $field 0
  3823         var v
  3824           int
  3825         var f2
  3826           type-con $field 0
  3827       attribute qid 1
  3828         string-attr VccPrelu.510:15
  3829       attribute uniqueId 1
  3830         string-attr 47
  3831       attribute bvZ3Native 1
  3832         string-attr False
  3833     or 2
  3834     =
  3835     fun $rec_fetch 2
  3836     fun $rec_update 3
  3837     var r
  3838       type-con $record 0
  3839     var f1
  3840       type-con $field 0
  3841     var v
  3842       int
  3843     var f2
  3844       type-con $field 0
  3845     fun $rec_fetch 2
  3846     var r
  3847       type-con $record 0
  3848     var f2
  3849       type-con $field 0
  3850     =
  3851     var f1
  3852       type-con $field 0
  3853     var f2
  3854       type-con $field 0
  3855 axiom 0
  3856     forall 1 1 3
  3857       var t
  3858         type-con $ctype 0
  3859       pat 1
  3860         fun $is_record_type 1
  3861         var t
  3862           type-con $ctype 0
  3863       attribute qid 1
  3864         string-attr VccPrelu.516:15
  3865       attribute uniqueId 1
  3866         string-attr 48
  3867       attribute bvZ3Native 1
  3868         string-attr False
  3869     implies
  3870     fun $is_record_type 1
  3871     var t
  3872       type-con $ctype 0
  3873     fun $is_primitive 1
  3874     var t
  3875       type-con $ctype 0
  3876 axiom 0
  3877     forall 3 1 3
  3878       var p
  3879         type-con $ctype 0
  3880       var f
  3881         type-con $field 0
  3882       var ft
  3883         type-con $ctype 0
  3884       pat 2
  3885         fun $is_record_field 3
  3886         var p
  3887           type-con $ctype 0
  3888         var f
  3889           type-con $field 0
  3890         var ft
  3891           type-con $ctype 0
  3892         fun $is_record_type 1
  3893         var ft
  3894           type-con $ctype 0
  3895       attribute qid 1
  3896         string-attr VccPrelu.519:15
  3897       attribute uniqueId 1
  3898         string-attr 49
  3899       attribute bvZ3Native 1
  3900         string-attr False
  3901     implies
  3902     and 2
  3903     fun $is_record_field 3
  3904     var p
  3905       type-con $ctype 0
  3906     var f
  3907       type-con $field 0
  3908     var ft
  3909       type-con $ctype 0
  3910     fun $is_record_type 1
  3911     var ft
  3912       type-con $ctype 0
  3913     =
  3914     fun $as_record_record_field 1
  3915     var f
  3916       type-con $field 0
  3917     var f
  3918       type-con $field 0
  3919 axiom 0
  3920     forall 2 1 3
  3921       var r1
  3922         type-con $record 0
  3923       var r2
  3924         type-con $record 0
  3925       pat 1
  3926         fun $rec_eq 2
  3927         var r1
  3928           type-con $record 0
  3929         var r2
  3930           type-con $record 0
  3931       attribute qid 1
  3932         string-attr VccPrelu.522:18
  3933       attribute uniqueId 1
  3934         string-attr 50
  3935       attribute bvZ3Native 1
  3936         string-attr False
  3937     =
  3938     fun $rec_eq 2
  3939     var r1
  3940       type-con $record 0
  3941     var r2
  3942       type-con $record 0
  3943     =
  3944     var r1
  3945       type-con $record 0
  3946     var r2
  3947       type-con $record 0
  3948 axiom 0
  3949     forall 2 1 3
  3950       var x
  3951         int
  3952       var y
  3953         int
  3954       pat 1
  3955         fun $rec_base_eq 2
  3956         var x
  3957           int
  3958         var y
  3959           int
  3960       attribute qid 1
  3961         string-attr VccPrelu.524:23
  3962       attribute uniqueId 1
  3963         string-attr 51
  3964       attribute bvZ3Native 1
  3965         string-attr False
  3966     =
  3967     fun $rec_base_eq 2
  3968     var x
  3969       int
  3970     var y
  3971       int
  3972     =
  3973     var x
  3974       int
  3975     var y
  3976       int
  3977 axiom 0
  3978     forall 1 0 3
  3979       var r
  3980         type-con $record 0
  3981       attribute qid 1
  3982         string-attr VccPrelu.530:15
  3983       attribute uniqueId 1
  3984         string-attr 52
  3985       attribute bvZ3Native 1
  3986         string-attr False
  3987     =
  3988     fun $int_to_record 1
  3989     fun $record_to_int 1
  3990     var r
  3991       type-con $record 0
  3992     var r
  3993       type-con $record 0
  3994 axiom 0
  3995     forall 2 1 3
  3996       var r1
  3997         type-con $record 0
  3998       var r2
  3999         type-con $record 0
  4000       pat 1
  4001         fun $rec_eq 2
  4002         var r1
  4003           type-con $record 0
  4004         var r2
  4005           type-con $record 0
  4006       attribute qid 1
  4007         string-attr VccPrelu.532:15
  4008       attribute uniqueId 1
  4009         string-attr 54
  4010       attribute bvZ3Native 1
  4011         string-attr False
  4012     implies
  4013     forall 1 0 3
  4014       var f
  4015         type-con $field 0
  4016       attribute qid 1
  4017         string-attr VccPrelu.534:11
  4018       attribute uniqueId 1
  4019         string-attr 53
  4020       attribute bvZ3Native 1
  4021         string-attr False
  4022     fun $rec_base_eq 2
  4023     fun $rec_fetch 2
  4024     var r1
  4025       type-con $record 0
  4026     var f
  4027       type-con $field 0
  4028     fun $rec_fetch 2
  4029     var r2
  4030       type-con $record 0
  4031     var f
  4032       type-con $field 0
  4033     fun $rec_eq 2
  4034     var r1
  4035       type-con $record 0
  4036     var r2
  4037       type-con $record 0
  4038 axiom 0
  4039     forall 3 1 3
  4040       var r1
  4041         type-con $record 0
  4042       var r2
  4043         type-con $record 0
  4044       var f
  4045         type-con $field 0
  4046       pat 1
  4047         fun $rec_base_eq 2
  4048         fun $rec_fetch 2
  4049         var r1
  4050           type-con $record 0
  4051         var f
  4052           type-con $field 0
  4053         fun $rec_fetch 2
  4054         var r2
  4055           type-con $record 0
  4056         fun $as_record_record_field 1
  4057         var f
  4058           type-con $field 0
  4059       attribute qid 1
  4060         string-attr VccPrelu.536:15
  4061       attribute uniqueId 1
  4062         string-attr 55
  4063       attribute bvZ3Native 1
  4064         string-attr False
  4065     implies
  4066     fun $rec_eq 2
  4067     fun $int_to_record 1
  4068     fun $rec_fetch 2
  4069     var r1
  4070       type-con $record 0
  4071     var f
  4072       type-con $field 0
  4073     fun $int_to_record 1
  4074     fun $rec_fetch 2
  4075     var r2
  4076       type-con $record 0
  4077     var f
  4078       type-con $field 0
  4079     fun $rec_base_eq 2
  4080     fun $rec_fetch 2
  4081     var r1
  4082       type-con $record 0
  4083     var f
  4084       type-con $field 0
  4085     fun $rec_fetch 2
  4086     var r2
  4087       type-con $record 0
  4088     var f
  4089       type-con $field 0
  4090 axiom 0
  4091     fun $has_volatile_owns_set 1
  4092     fun ^^claim 0
  4093 axiom 0
  4094     forall 2 1 3
  4095       var #p
  4096         type-con $ptr 0
  4097       var t
  4098         type-con $ctype 0
  4099       pat 1
  4100         fun $dot 2
  4101         var #p
  4102           type-con $ptr 0
  4103         fun $owns_set_field 1
  4104         var t
  4105           type-con $ctype 0
  4106       attribute qid 1
  4107         string-attr VccPrelu.555:15
  4108       attribute uniqueId 1
  4109         string-attr 56
  4110       attribute bvZ3Native 1
  4111         string-attr False
  4112     =
  4113     fun $dot 2
  4114     var #p
  4115       type-con $ptr 0
  4116     fun $owns_set_field 1
  4117     var t
  4118       type-con $ctype 0
  4119     fun $ptr 2
  4120     fun ^$#ptrset 0
  4121     fun $ghost_ref 2
  4122     var #p
  4123       type-con $ptr 0
  4124     fun $owns_set_field 1
  4125     var t
  4126       type-con $ctype 0
  4127 axiom 0
  4128     forall 2 1 4
  4129       var S
  4130         type-con $state 0
  4131       var p
  4132         type-con $ptr 0
  4133       pat 2
  4134         fun $is_primitive 1
  4135         fun $typ 1
  4136         var p
  4137           type-con $ptr 0
  4138         fun $owner 2
  4139         var S
  4140           type-con $state 0
  4141         var p
  4142           type-con $ptr 0
  4143       attribute qid 1
  4144         string-attr VccPrelu.567:15
  4145       attribute uniqueId 1
  4146         string-attr 57
  4147       attribute bvZ3Native 1
  4148         string-attr False
  4149       attribute weight 1
  4150         expr-attr
  4151           int-num 0
  4152     implies
  4153     fun $is_primitive 1
  4154     fun $typ 1
  4155     var p
  4156       type-con $ptr 0
  4157     =
  4158     fun $owner 2
  4159     var S
  4160       type-con $state 0
  4161     var p
  4162       type-con $ptr 0
  4163     fun $owner 2
  4164     var S
  4165       type-con $state 0
  4166     fun $ts_emb 1
  4167     fun $select.tm 2
  4168     fun $typemap 1
  4169     var S
  4170       type-con $state 0
  4171     var p
  4172       type-con $ptr 0
  4173 axiom 0
  4174     forall 2 1 4
  4175       var S
  4176         type-con $state 0
  4177       var p
  4178         type-con $ptr 0
  4179       pat 2
  4180         fun $is_non_primitive 1
  4181         fun $typ 1
  4182         var p
  4183           type-con $ptr 0
  4184         fun $owner 2
  4185         var S
  4186           type-con $state 0
  4187         var p
  4188           type-con $ptr 0
  4189       attribute qid 1
  4190         string-attr VccPrelu.569:15
  4191       attribute uniqueId 1
  4192         string-attr 58
  4193       attribute bvZ3Native 1
  4194         string-attr False
  4195       attribute weight 1
  4196         expr-attr
  4197           int-num 0
  4198     implies
  4199     fun $is_non_primitive 1
  4200     fun $typ 1
  4201     var p
  4202       type-con $ptr 0
  4203     =
  4204     fun $owner 2
  4205     var S
  4206       type-con $state 0
  4207     var p
  4208       type-con $ptr 0
  4209     fun $st_owner 1
  4210     fun $select.sm 2
  4211     fun $statusmap 1
  4212     var S
  4213       type-con $state 0
  4214     var p
  4215       type-con $ptr 0
  4216 axiom 0
  4217     forall 2 1 4
  4218       var S
  4219         type-con $state 0
  4220       var p
  4221         type-con $ptr 0
  4222       pat 2
  4223         fun $is_primitive 1
  4224         fun $typ 1
  4225         var p
  4226           type-con $ptr 0
  4227         fun $closed 2
  4228         var S
  4229           type-con $state 0
  4230         var p
  4231           type-con $ptr 0
  4232       attribute qid 1
  4233         string-attr VccPrelu.572:15
  4234       attribute uniqueId 1
  4235         string-attr 59
  4236       attribute bvZ3Native 1
  4237         string-attr False
  4238       attribute weight 1
  4239         expr-attr
  4240           int-num 0
  4241     implies
  4242     fun $is_primitive 1
  4243     fun $typ 1
  4244     var p
  4245       type-con $ptr 0
  4246     =
  4247     fun $closed 2
  4248     var S
  4249       type-con $state 0
  4250     var p
  4251       type-con $ptr 0
  4252     fun $st_closed 1
  4253     fun $select.sm 2
  4254     fun $statusmap 1
  4255     var S
  4256       type-con $state 0
  4257     fun $ts_emb 1
  4258     fun $select.tm 2
  4259     fun $typemap 1
  4260     var S
  4261       type-con $state 0
  4262     var p
  4263       type-con $ptr 0
  4264 axiom 0
  4265     forall 2 1 4
  4266       var S
  4267         type-con $state 0
  4268       var p
  4269         type-con $ptr 0
  4270       pat 2
  4271         fun $is_non_primitive 1
  4272         fun $typ 1
  4273         var p
  4274           type-con $ptr 0
  4275         fun $closed 2
  4276         var S
  4277           type-con $state 0
  4278         var p
  4279           type-con $ptr 0
  4280       attribute qid 1
  4281         string-attr VccPrelu.574:15
  4282       attribute uniqueId 1
  4283         string-attr 60
  4284       attribute bvZ3Native 1
  4285         string-attr False
  4286       attribute weight 1
  4287         expr-attr
  4288           int-num 0
  4289     implies
  4290     fun $is_non_primitive 1
  4291     fun $typ 1
  4292     var p
  4293       type-con $ptr 0
  4294     =
  4295     fun $closed 2
  4296     var S
  4297       type-con $state 0
  4298     var p
  4299       type-con $ptr 0
  4300     fun $st_closed 1
  4301     fun $select.sm 2
  4302     fun $statusmap 1
  4303     var S
  4304       type-con $state 0
  4305     var p
  4306       type-con $ptr 0
  4307 axiom 0
  4308     forall 2 1 4
  4309       var S
  4310         type-con $state 0
  4311       var p
  4312         type-con $ptr 0
  4313       pat 2
  4314         fun $is_primitive 1
  4315         fun $typ 1
  4316         var p
  4317           type-con $ptr 0
  4318         fun $timestamp 2
  4319         var S
  4320           type-con $state 0
  4321         var p
  4322           type-con $ptr 0
  4323       attribute qid 1
  4324         string-attr VccPrelu.577:15
  4325       attribute uniqueId 1
  4326         string-attr 61
  4327       attribute bvZ3Native 1
  4328         string-attr False
  4329       attribute weight 1
  4330         expr-attr
  4331           int-num 0
  4332     implies
  4333     fun $is_primitive 1
  4334     fun $typ 1
  4335     var p
  4336       type-con $ptr 0
  4337     =
  4338     fun $timestamp 2
  4339     var S
  4340       type-con $state 0
  4341     var p
  4342       type-con $ptr 0
  4343     fun $st_timestamp 1
  4344     fun $select.sm 2
  4345     fun $statusmap 1
  4346     var S
  4347       type-con $state 0
  4348     fun $ts_emb 1
  4349     fun $select.tm 2
  4350     fun $typemap 1
  4351     var S
  4352       type-con $state 0
  4353     var p
  4354       type-con $ptr 0
  4355 axiom 0
  4356     forall 2 1 4
  4357       var S
  4358         type-con $state 0
  4359       var p
  4360         type-con $ptr 0
  4361       pat 2
  4362         fun $is_non_primitive 1
  4363         fun $typ 1
  4364         var p
  4365           type-con $ptr 0
  4366         fun $timestamp 2
  4367         var S
  4368           type-con $state 0
  4369         var p
  4370           type-con $ptr 0
  4371       attribute qid 1
  4372         string-attr VccPrelu.579:15
  4373       attribute uniqueId 1
  4374         string-attr 62
  4375       attribute bvZ3Native 1
  4376         string-attr False
  4377       attribute weight 1
  4378         expr-attr
  4379           int-num 0
  4380     implies
  4381     fun $is_non_primitive 1
  4382     fun $typ 1
  4383     var p
  4384       type-con $ptr 0
  4385     =
  4386     fun $timestamp 2
  4387     var S
  4388       type-con $state 0
  4389     var p
  4390       type-con $ptr 0
  4391     fun $st_timestamp 1
  4392     fun $select.sm 2
  4393     fun $statusmap 1
  4394     var S
  4395       type-con $state 0
  4396     var p
  4397       type-con $ptr 0
  4398 axiom 0
  4399     fun $position_marker 0
  4400 axiom 0
  4401     forall 1 1 3
  4402       var s
  4403         type-con $status 0
  4404       pat 1
  4405         fun $st_owner 1
  4406         var s
  4407           type-con $status 0
  4408       attribute qid 1
  4409         string-attr VccPrelu.585:15
  4410       attribute uniqueId 1
  4411         string-attr 63
  4412       attribute bvZ3Native 1
  4413         string-attr False
  4414     and 2
  4415     not
  4416     =
  4417     fun $kind_of 1
  4418     fun $typ 1
  4419     fun $st_owner 1
  4420     var s
  4421       type-con $status 0
  4422     fun $kind_primitive 0
  4423     fun $is_non_primitive 1
  4424     fun $typ 1
  4425     fun $st_owner 1
  4426     var s
  4427       type-con $status 0
  4428 axiom 0
  4429     forall 2 1 4
  4430       var S
  4431         type-con $state 0
  4432       var #p
  4433         type-con $ptr 0
  4434       pat 1
  4435         fun $owns 2
  4436         var S
  4437           type-con $state 0
  4438         var #p
  4439           type-con $ptr 0
  4440       attribute qid 1
  4441         string-attr VccPrelu.593:28
  4442       attribute uniqueId 1
  4443         string-attr 64
  4444       attribute bvZ3Native 1
  4445         string-attr False
  4446       attribute weight 1
  4447         expr-attr
  4448           int-num 0
  4449     =
  4450     fun $owns 2
  4451     var S
  4452       type-con $state 0
  4453     var #p
  4454       type-con $ptr 0
  4455     fun $int_to_ptrset 1
  4456     fun $select.mem 2
  4457     fun $memory 1
  4458     var S
  4459       type-con $state 0
  4460     fun $dot 2
  4461     var #p
  4462       type-con $ptr 0
  4463     fun $owns_set_field 1
  4464     fun $typ 1
  4465     var #p
  4466       type-con $ptr 0
  4467 axiom 0
  4468     forall 2 1 4
  4469       var S
  4470         type-con $state 0
  4471       var p
  4472         type-con $ptr 0
  4473       pat 1
  4474         fun $mutable 2
  4475         var S
  4476           type-con $state 0
  4477         var p
  4478           type-con $ptr 0
  4479       attribute qid 1
  4480         string-attr VccPrelu.608:31
  4481       attribute uniqueId 1
  4482         string-attr 65
  4483       attribute bvZ3Native 1
  4484         string-attr False
  4485       attribute weight 1
  4486         expr-attr
  4487           int-num 0
  4488     =
  4489     fun $mutable 2
  4490     var S
  4491       type-con $state 0
  4492     var p
  4493       type-con $ptr 0
  4494     and 3
  4495     fun $typed 2
  4496     var S
  4497       type-con $state 0
  4498     var p
  4499       type-con $ptr 0
  4500     =
  4501     fun $owner 2
  4502     var S
  4503       type-con $state 0
  4504     var p
  4505       type-con $ptr 0
  4506     fun $me 0
  4507     not
  4508     fun $closed 2
  4509     var S
  4510       type-con $state 0
  4511     var p
  4512       type-con $ptr 0
  4513 axiom 0
  4514     forall 2 1 4
  4515       var S
  4516         type-con $state 0
  4517       var #p
  4518         type-con $ptr 0
  4519       pat 1
  4520         fun $typed 2
  4521         var S
  4522           type-con $state 0
  4523         var #p
  4524           type-con $ptr 0
  4525       attribute qid 1
  4526         string-attr VccPrelu.619:11
  4527       attribute uniqueId 1
  4528         string-attr 66
  4529       attribute bvZ3Native 1
  4530         string-attr False
  4531       attribute weight 1
  4532         expr-attr
  4533           int-num 0
  4534     implies
  4535     fun $good_state 1
  4536     var S
  4537       type-con $state 0
  4538     =
  4539     fun $typed 2
  4540     var S
  4541       type-con $state 0
  4542     var #p
  4543       type-con $ptr 0
  4544     fun $ts_typed 1
  4545     fun $select.tm 2
  4546     fun $typemap 1
  4547     var S
  4548       type-con $state 0
  4549     var #p
  4550       type-con $ptr 0
  4551 axiom 0
  4552     forall 2 1 3
  4553       var S
  4554         type-con $state 0
  4555       var #p
  4556         type-con $ptr 0
  4557       pat 1
  4558         fun $typed 2
  4559         var S
  4560           type-con $state 0
  4561         var #p
  4562           type-con $ptr 0
  4563       attribute qid 1
  4564         string-attr VccPrelu.621:11
  4565       attribute uniqueId 1
  4566         string-attr 67
  4567       attribute bvZ3Native 1
  4568         string-attr False
  4569     implies
  4570     and 2
  4571     fun $good_state 1
  4572     var S
  4573       type-con $state 0
  4574     fun $typed 2
  4575     var S
  4576       type-con $state 0
  4577     var #p
  4578       type-con $ptr 0
  4579     >
  4580     fun $ref 1
  4581     var #p
  4582       type-con $ptr 0
  4583     int-num 0
  4584 axiom 0
  4585     forall 3 1 3
  4586       var S1
  4587         type-con $state 0
  4588       var S2
  4589         type-con $state 0
  4590       var p
  4591         type-con $ptr 0
  4592       pat 2
  4593         fun $select.sm 2
  4594         fun $statusmap 1
  4595         var S2
  4596           type-con $state 0
  4597         var p
  4598           type-con $ptr 0
  4599         fun $call_transition 2
  4600         var S1
  4601           type-con $state 0
  4602         var S2
  4603           type-con $state 0
  4604       attribute qid 1
  4605         string-attr VccPrelu.685:15
  4606       attribute uniqueId 1
  4607         string-attr 68
  4608       attribute bvZ3Native 1
  4609         string-attr False
  4610     implies
  4611     fun $call_transition 2
  4612     var S1
  4613       type-con $state 0
  4614     var S2
  4615       type-con $state 0
  4616     fun $instantiate_st 1
  4617     fun $select.sm 2
  4618     fun $statusmap 1
  4619     var S1
  4620       type-con $state 0
  4621     var p
  4622       type-con $ptr 0
  4623 axiom 0
  4624     forall 2 1 3
  4625       var S
  4626         type-con $state 0
  4627       var p
  4628         type-con $ptr 0
  4629       pat 1
  4630         fun $is_domain_root 2
  4631         var S
  4632           type-con $state 0
  4633         var p
  4634           type-con $ptr 0
  4635       attribute qid 1
  4636         string-attr VccPrelu.711:26
  4637       attribute uniqueId 1
  4638         string-attr 69
  4639       attribute bvZ3Native 1
  4640         string-attr False
  4641     =
  4642     fun $is_domain_root 2
  4643     var S
  4644       type-con $state 0
  4645     var p
  4646       type-con $ptr 0
  4647     true
  4648 axiom 0
  4649     forall 2 1 3
  4650       var S
  4651         type-con $state 0
  4652       var p
  4653         type-con $ptr 0
  4654       pat 1
  4655         fun $in_wrapped_domain 2
  4656         var S
  4657           type-con $state 0
  4658         var p
  4659           type-con $ptr 0
  4660       attribute qid 1
  4661         string-attr VccPrelu.714:29
  4662       attribute uniqueId 1
  4663         string-attr 71
  4664       attribute bvZ3Native 1
  4665         string-attr False
  4666     =
  4667     fun $in_wrapped_domain 2
  4668     var S
  4669       type-con $state 0
  4670     var p
  4671       type-con $ptr 0
  4672     exists 1 1 3
  4673       var q
  4674         type-con $ptr 0
  4675       pat 1
  4676         fun $set_in2 2
  4677         var p
  4678           type-con $ptr 0
  4679         fun $ver_domain 1
  4680         fun $read_version 2
  4681         var S
  4682           type-con $state 0
  4683         var q
  4684           type-con $ptr 0
  4685       attribute qid 1
  4686         string-attr VccPrelu.715:13
  4687       attribute uniqueId 1
  4688         string-attr 70
  4689       attribute bvZ3Native 1
  4690         string-attr False
  4691     and 8
  4692     fun $set_in 2
  4693     var p
  4694       type-con $ptr 0
  4695     fun $ver_domain 1
  4696     fun $read_version 2
  4697     var S
  4698       type-con $state 0
  4699     var q
  4700       type-con $ptr 0
  4701     fun $closed 2
  4702     var S
  4703       type-con $state 0
  4704     var q
  4705       type-con $ptr 0
  4706     =
  4707     fun $owner 2
  4708     var S
  4709       type-con $state 0
  4710     var q
  4711       type-con $ptr 0
  4712     fun $me 0
  4713     fun $is 2
  4714     var q
  4715       type-con $ptr 0
  4716     fun $typ 1
  4717     var q
  4718       type-con $ptr 0
  4719     fun $typed 2
  4720     var S
  4721       type-con $state 0
  4722     var q
  4723       type-con $ptr 0
  4724     not
  4725     =
  4726     fun $kind_of 1
  4727     fun $typ 1
  4728     var q
  4729       type-con $ptr 0
  4730     fun $kind_primitive 0
  4731     fun $is_non_primitive 1
  4732     fun $typ 1
  4733     var q
  4734       type-con $ptr 0
  4735     fun $is_domain_root 2
  4736     var S
  4737       type-con $state 0
  4738     var q
  4739       type-con $ptr 0
  4740 axiom 0
  4741     forall 2 1 3
  4742       var S
  4743         type-con $state 0
  4744       var p
  4745         type-con $ptr 0
  4746       pat 1
  4747         fun $thread_local 2
  4748         var S
  4749           type-con $state 0
  4750         var p
  4751           type-con $ptr 0
  4752       attribute qid 1
  4753         string-attr VccPrelu.728:24
  4754       attribute uniqueId 1
  4755         string-attr 72
  4756       attribute bvZ3Native 1
  4757         string-attr False
  4758     =
  4759     fun $thread_local 2
  4760     var S
  4761       type-con $state 0
  4762     var p
  4763       type-con $ptr 0
  4764     and 2
  4765     fun $typed 2
  4766     var S
  4767       type-con $state 0
  4768     var p
  4769       type-con $ptr 0
  4770     or 2
  4771     and 4
  4772     =
  4773     fun $kind_of 1
  4774     fun $typ 1
  4775     var p
  4776       type-con $ptr 0
  4777     fun $kind_primitive 0
  4778     or 2
  4779     not
  4780     fun $ts_is_volatile 1
  4781     fun $select.tm 2
  4782     fun $typemap 1
  4783     var S
  4784       type-con $state 0
  4785     var p
  4786       type-con $ptr 0
  4787     not
  4788     fun $closed 2
  4789     var S
  4790       type-con $state 0
  4791     fun $ts_emb 1
  4792     fun $select.tm 2
  4793     fun $typemap 1
  4794     var S
  4795       type-con $state 0
  4796     var p
  4797       type-con $ptr 0
  4798     not
  4799     =
  4800     fun $kind_of 1
  4801     fun $typ 1
  4802     fun $ts_emb 1
  4803     fun $select.tm 2
  4804     fun $typemap 1
  4805     var S
  4806       type-con $state 0
  4807     var p
  4808       type-con $ptr 0
  4809     fun $kind_primitive 0
  4810     or 2
  4811     =
  4812     fun $owner 2
  4813     var S
  4814       type-con $state 0
  4815     fun $ts_emb 1
  4816     fun $select.tm 2
  4817     fun $typemap 1
  4818     var S
  4819       type-con $state 0
  4820     var p
  4821       type-con $ptr 0
  4822     fun $me 0
  4823     fun $in_wrapped_domain 2
  4824     var S
  4825       type-con $state 0
  4826     fun $ts_emb 1
  4827     fun $select.tm 2
  4828     fun $typemap 1
  4829     var S
  4830       type-con $state 0
  4831     var p
  4832       type-con $ptr 0
  4833     and 2
  4834     not
  4835     =
  4836     fun $kind_of 1
  4837     fun $typ 1
  4838     var p
  4839       type-con $ptr 0
  4840     fun $kind_primitive 0
  4841     or 2
  4842     =
  4843     fun $owner 2
  4844     var S
  4845       type-con $state 0
  4846     var p
  4847       type-con $ptr 0
  4848     fun $me 0
  4849     fun $in_wrapped_domain 2
  4850     var S
  4851       type-con $state 0
  4852     var p
  4853       type-con $ptr 0
  4854 axiom 0
  4855     forall 3 1 3
  4856       var #s1
  4857         type-con $state 0
  4858       var #p
  4859         type-con $ptr 0
  4860       var typ
  4861         type-con $ctype 0
  4862       pat 1
  4863         fun $inv2 4
  4864         var #s1
  4865           type-con $state 0
  4866         var #s1
  4867           type-con $state 0
  4868         var #p
  4869           type-con $ptr 0
  4870         var typ
  4871           type-con $ctype 0
  4872       attribute qid 1
  4873         string-attr VccPrelu.766:15
  4874       attribute uniqueId 1
  4875         string-attr 73
  4876       attribute bvZ3Native 1
  4877         string-attr False
  4878     implies
  4879     fun $imply_inv 3
  4880     var #s1
  4881       type-con $state 0
  4882     var #p
  4883       type-con $ptr 0
  4884     var typ
  4885       type-con $ctype 0
  4886     fun $inv2 4
  4887     var #s1
  4888       type-con $state 0
  4889     var #s1
  4890       type-con $state 0
  4891     var #p
  4892       type-con $ptr 0
  4893     var typ
  4894       type-con $ctype 0
  4895 axiom 0
  4896     forall 4 1 4
  4897       var #s1
  4898         type-con $state 0
  4899       var #s2
  4900         type-con $state 0
  4901       var #p
  4902         type-con $ptr 0
  4903       var #t
  4904         type-con $ctype 0
  4905       pat 1
  4906         fun $sequential 4
  4907         var #s1
  4908           type-con $state 0
  4909         var #s2
  4910           type-con $state 0
  4911         var #p
  4912           type-con $ptr 0
  4913         var #t
  4914           type-con $ctype 0
  4915       attribute qid 1
  4916         string-attr VccPrelu.778:34
  4917       attribute uniqueId 1
  4918         string-attr 74
  4919       attribute bvZ3Native 1
  4920         string-attr False
  4921       attribute weight 1
  4922         expr-attr
  4923           int-num 0
  4924     =
  4925     fun $sequential 4
  4926     var #s1
  4927       type-con $state 0
  4928     var #s2
  4929       type-con $state 0
  4930     var #p
  4931       type-con $ptr 0
  4932     var #t
  4933       type-con $ctype 0
  4934     implies
  4935     and 2
  4936     fun $closed 2
  4937     var #s1
  4938       type-con $state 0
  4939     var #p
  4940       type-con $ptr 0
  4941     fun $closed 2
  4942     var #s2
  4943       type-con $state 0
  4944     var #p
  4945       type-con $ptr 0
  4946     fun $spans_the_same 4
  4947     var #s1
  4948       type-con $state 0
  4949     var #s2
  4950       type-con $state 0
  4951     var #p
  4952       type-con $ptr 0
  4953     var #t
  4954       type-con $ctype 0
  4955 axiom 0
  4956     forall 4 1 4
  4957       var #s1
  4958         type-con $state 0
  4959       var #s2
  4960         type-con $state 0
  4961       var #dependant
  4962         type-con $ptr 0
  4963       var #this
  4964         type-con $ptr 0
  4965       pat 1
  4966         fun $depends 4
  4967         var #s1
  4968           type-con $state 0
  4969         var #s2
  4970           type-con $state 0
  4971         var #dependant
  4972           type-con $ptr 0
  4973         var #this
  4974           type-con $ptr 0
  4975       attribute qid 1
  4976         string-attr VccPrelu.781:31
  4977       attribute uniqueId 1
  4978         string-attr 75
  4979       attribute bvZ3Native 1
  4980         string-attr False
  4981       attribute weight 1
  4982         expr-attr
  4983           int-num 0
  4984     =
  4985     fun $depends 4
  4986     var #s1
  4987       type-con $state 0
  4988     var #s2
  4989       type-con $state 0
  4990     var #dependant
  4991       type-con $ptr 0
  4992     var #this
  4993       type-con $ptr 0
  4994     or 4
  4995     fun $spans_the_same 4
  4996     var #s1
  4997       type-con $state 0
  4998     var #s2
  4999       type-con $state 0
  5000     var #this
  5001       type-con $ptr 0
  5002     fun $typ 1
  5003     var #this
  5004       type-con $ptr 0
  5005     and 2
  5006     not
  5007     fun $closed 2
  5008     var #s1
  5009       type-con $state 0
  5010     var #dependant
  5011       type-con $ptr 0
  5012     not
  5013     fun $closed 2
  5014     var #s2
  5015       type-con $state 0
  5016     var #dependant
  5017       type-con $ptr 0
  5018     and 2
  5019     fun $inv2 4
  5020     var #s1
  5021       type-con $state 0
  5022     var #s2
  5023       type-con $state 0
  5024     var #dependant
  5025       type-con $ptr 0
  5026     fun $typ 1
  5027     var #dependant
  5028       type-con $ptr 0
  5029     fun $nonvolatile_spans_the_same 4
  5030     var #s1
  5031       type-con $state 0
  5032     var #s2
  5033       type-con $state 0
  5034     var #dependant
  5035       type-con $ptr 0
  5036     fun $typ 1
  5037     var #dependant
  5038       type-con $ptr 0
  5039     fun $is_threadtype 1
  5040     fun $typ 1
  5041     var #dependant
  5042       type-con $ptr 0
  5043 axiom 0
  5044     forall 4 1 4
  5045       var #s1
  5046         type-con $state 0
  5047       var #s2
  5048         type-con $state 0
  5049       var #p
  5050         type-con $ptr 0
  5051       var #t
  5052         type-con $ctype 0
  5053       pat 1
  5054         fun $spans_the_same 4
  5055         var #s1
  5056           type-con $state 0
  5057         var #s2
  5058           type-con $state 0
  5059         var #p
  5060           type-con $ptr 0
  5061         var #t
  5062           type-con $ctype 0
  5063       attribute qid 1
  5064         string-attr VccPrelu.786:38
  5065       attribute uniqueId 1
  5066         string-attr 76
  5067       attribute bvZ3Native 1
  5068         string-attr False
  5069       attribute weight 1
  5070         expr-attr
  5071           int-num 0
  5072     =
  5073     fun $spans_the_same 4
  5074     var #s1
  5075       type-con $state 0
  5076     var #s2
  5077       type-con $state 0
  5078     var #p
  5079       type-con $ptr 0
  5080     var #t
  5081       type-con $ctype 0
  5082     and 4
  5083     =
  5084     fun $read_version 2
  5085     var #s1
  5086       type-con $state 0
  5087     var #p
  5088       type-con $ptr 0
  5089     fun $read_version 2
  5090     var #s2
  5091       type-con $state 0
  5092     var #p
  5093       type-con $ptr 0
  5094     =
  5095     fun $owns 2
  5096     var #s1
  5097       type-con $state 0
  5098     var #p
  5099       type-con $ptr 0
  5100     fun $owns 2
  5101     var #s2
  5102       type-con $state 0
  5103     var #p
  5104       type-con $ptr 0
  5105     =
  5106     fun $select.tm 2
  5107     fun $typemap 1
  5108     var #s1
  5109       type-con $state 0
  5110     var #p
  5111       type-con $ptr 0
  5112     fun $select.tm 2
  5113     fun $typemap 1
  5114     var #s2
  5115       type-con $state 0
  5116     var #p
  5117       type-con $ptr 0
  5118     fun $state_spans_the_same 4
  5119     var #s1
  5120       type-con $state 0
  5121     var #s2
  5122       type-con $state 0
  5123     var #p
  5124       type-con $ptr 0
  5125     var #t
  5126       type-con $ctype 0
  5127 axiom 0
  5128     forall 4 1 4
  5129       var #s1
  5130         type-con $state 0
  5131       var #s2
  5132         type-con $state 0
  5133       var #p
  5134         type-con $ptr 0
  5135       var #t
  5136         type-con $ctype 0
  5137       pat 1
  5138         fun $nonvolatile_spans_the_same 4
  5139         var #s1
  5140           type-con $state 0
  5141         var #s2
  5142           type-con $state 0
  5143         var #p
  5144           type-con $ptr 0
  5145         var #t
  5146           type-con $ctype 0
  5147       attribute qid 1
  5148         string-attr VccPrelu.795:50
  5149       attribute uniqueId 1
  5150         string-attr 77
  5151       attribute bvZ3Native 1
  5152         string-attr False
  5153       attribute weight 1
  5154         expr-attr
  5155           int-num 0
  5156     =
  5157     fun $nonvolatile_spans_the_same 4
  5158     var #s1
  5159       type-con $state 0
  5160     var #s2
  5161       type-con $state 0
  5162     var #p
  5163       type-con $ptr 0
  5164     var #t
  5165       type-con $ctype 0
  5166     and 3
  5167     =
  5168     fun $read_version 2
  5169     var #s1
  5170       type-con $state 0
  5171     var #p
  5172       type-con $ptr 0
  5173     fun $read_version 2
  5174     var #s2
  5175       type-con $state 0
  5176     var #p
  5177       type-con $ptr 0
  5178     =
  5179     fun $select.tm 2
  5180     fun $typemap 1
  5181     var #s1
  5182       type-con $state 0
  5183     var #p
  5184       type-con $ptr 0
  5185     fun $select.tm 2
  5186     fun $typemap 1
  5187     var #s2
  5188       type-con $state 0
  5189     var #p
  5190       type-con $ptr 0
  5191     fun $state_nonvolatile_spans_the_same 4
  5192     var #s1
  5193       type-con $state 0
  5194     var #s2
  5195       type-con $state 0
  5196     var #p
  5197       type-con $ptr 0
  5198     var #t
  5199       type-con $ctype 0
  5200 axiom 0
  5201     forall 1 1 3
  5202       var T
  5203         type-con $ctype 0
  5204       pat 1
  5205         fun $is_primitive 1
  5206         var T
  5207           type-con $ctype 0
  5208       attribute qid 1
  5209         string-attr VccPrelu.813:15
  5210       attribute uniqueId 1
  5211         string-attr 79
  5212       attribute bvZ3Native 1
  5213         string-attr False
  5214     implies
  5215     fun $is_primitive 1
  5216     var T
  5217       type-con $ctype 0
  5218     forall 2 1 3
  5219       var r
  5220         int
  5221       var p
  5222         type-con $ptr 0
  5223       pat 1
  5224         fun $set_in 2
  5225         var p
  5226           type-con $ptr 0
  5227         fun $full_extent 1
  5228         fun $ptr 2
  5229         var T
  5230           type-con $ctype 0
  5231         var r
  5232           int
  5233       attribute qid 1
  5234         string-attr VccPrelu.815:13
  5235       attribute uniqueId 1
  5236         string-attr 78
  5237       attribute bvZ3Native 1
  5238         string-attr False
  5239     =
  5240     fun $set_in 2
  5241     var p
  5242       type-con $ptr 0
  5243     fun $full_extent 1
  5244     fun $ptr 2
  5245     var T
  5246       type-con $ctype 0
  5247     var r
  5248       int
  5249     =
  5250     var p
  5251       type-con $ptr 0
  5252     fun $ptr 2
  5253     var T
  5254       type-con $ctype 0
  5255     var r
  5256       int
  5257 axiom 0
  5258     forall 1 1 3
  5259       var T
  5260         type-con $ctype 0
  5261       pat 1
  5262         fun $is_primitive 1
  5263         var T
  5264           type-con $ctype 0
  5265       attribute qid 1
  5266         string-attr VccPrelu.818:15
  5267       attribute uniqueId 1
  5268         string-attr 81
  5269       attribute bvZ3Native 1
  5270         string-attr False
  5271     implies
  5272     fun $is_primitive 1
  5273     var T
  5274       type-con $ctype 0
  5275     forall 3 1 3
  5276       var S
  5277         type-con $state 0
  5278       var r
  5279         int
  5280       var p
  5281         type-con $ptr 0
  5282       pat 1
  5283         fun $set_in 2
  5284         var p
  5285           type-con $ptr 0
  5286         fun $extent 2
  5287         var S
  5288           type-con $state 0
  5289         fun $ptr 2
  5290         var T
  5291           type-con $ctype 0
  5292         var r
  5293           int
  5294       attribute qid 1
  5295         string-attr VccPrelu.820:13
  5296       attribute uniqueId 1
  5297         string-attr 80
  5298       attribute bvZ3Native 1
  5299         string-attr False
  5300     =
  5301     fun $set_in 2
  5302     var p
  5303       type-con $ptr 0
  5304     fun $extent 2
  5305     var S
  5306       type-con $state 0
  5307     fun $ptr 2
  5308     var T
  5309       type-con $ctype 0
  5310     var r
  5311       int
  5312     =
  5313     var p
  5314       type-con $ptr 0
  5315     fun $ptr 2
  5316     var T
  5317       type-con $ctype 0
  5318     var r
  5319       int
  5320 axiom 0
  5321     forall 1 1 3
  5322       var S
  5323         type-con $state 0
  5324       pat 1
  5325         fun $function_entry 1
  5326         var S
  5327           type-con $state 0
  5328       attribute qid 1
  5329         string-attr VccPrelu.835:15
  5330       attribute uniqueId 1
  5331         string-attr 83
  5332       attribute bvZ3Native 1
  5333         string-attr False
  5334     implies
  5335     fun $function_entry 1
  5336     var S
  5337       type-con $state 0
  5338     and 2
  5339     fun $full_stop 1
  5340     var S
  5341       type-con $state 0
  5342     >=
  5343     fun $current_timestamp 1
  5344     var S
  5345       type-con $state 0
  5346     int-num 0
  5347 axiom 0
  5348     forall 1 1 3
  5349       var S
  5350         type-con $state 0
  5351       pat 1
  5352         fun $full_stop 1
  5353         var S
  5354           type-con $state 0
  5355       attribute qid 1
  5356         string-attr VccPrelu.838:15
  5357       attribute uniqueId 1
  5358         string-attr 84
  5359       attribute bvZ3Native 1
  5360         string-attr False
  5361     implies
  5362     fun $full_stop 1
  5363     var S
  5364       type-con $state 0
  5365     and 2
  5366     fun $good_state 1
  5367     var S
  5368       type-con $state 0
  5369     fun $invok_state 1
  5370     var S
  5371       type-con $state 0
  5372 axiom 0
  5373     forall 1 1 3
  5374       var S
  5375         type-con $state 0
  5376       pat 1
  5377         fun $invok_state 1
  5378         var S
  5379           type-con $state 0
  5380       attribute qid 1
  5381         string-attr VccPrelu.841:15
  5382       attribute uniqueId 1
  5383         string-attr 85
  5384       attribute bvZ3Native 1
  5385         string-attr False
  5386     implies
  5387     fun $invok_state 1
  5388     var S
  5389       type-con $state 0
  5390     fun $good_state 1
  5391     var S
  5392       type-con $state 0
  5393 axiom 0
  5394     forall 2 1 3
  5395       var id
  5396         type-con $token 0
  5397       var S
  5398         type-con $state 0
  5399       pat 1
  5400         fun $good_state_ext 2
  5401         var id
  5402           type-con $token 0
  5403         var S
  5404           type-con $state 0
  5405       attribute qid 1
  5406         string-attr VccPrelu.860:15
  5407       attribute uniqueId 1
  5408         string-attr 87
  5409       attribute bvZ3Native 1
  5410         string-attr False
  5411     implies
  5412     fun $good_state_ext 2
  5413     var id
  5414       type-con $token 0
  5415     var S
  5416       type-con $state 0
  5417     fun $good_state 1
  5418     var S
  5419       type-con $state 0
  5420 axiom 0
  5421     forall 3 1 3
  5422       var S
  5423         type-con $state 0
  5424       var r
  5425         int
  5426       var t
  5427         type-con $ctype 0
  5428       pat 1
  5429         fun $ptr 2
  5430         var t
  5431           type-con $ctype 0
  5432         fun $select.mem 2
  5433         fun $memory 1
  5434         var S
  5435           type-con $state 0
  5436         fun $ptr 2
  5437         fun $ptr_to 1
  5438         var t
  5439           type-con $ctype 0
  5440         var r
  5441           int
  5442       attribute qid 1
  5443         string-attr VccPrelu.872:15
  5444       attribute uniqueId 1
  5445         string-attr 88
  5446       attribute bvZ3Native 1
  5447         string-attr False
  5448     =
  5449     fun $ptr 2
  5450     var t
  5451       type-con $ctype 0
  5452     fun $select.mem 2
  5453     fun $memory 1
  5454     var S
  5455       type-con $state 0
  5456     fun $ptr 2
  5457     fun $ptr_to 1
  5458     var t
  5459       type-con $ctype 0
  5460     var r
  5461       int
  5462     fun $read_ptr_m 3
  5463     var S
  5464       type-con $state 0
  5465     fun $ptr 2
  5466     fun $ptr_to 1
  5467     var t
  5468       type-con $ctype 0
  5469     var r
  5470       int
  5471     var t
  5472       type-con $ctype 0
  5473 axiom 0
  5474     forall 2 1 4
  5475       var S
  5476         type-con $state 0
  5477       var p
  5478         type-con $ptr 0
  5479       pat 1
  5480         fun $read_version 2
  5481         var S
  5482           type-con $state 0
  5483         var p
  5484           type-con $ptr 0
  5485       attribute qid 1
  5486         string-attr VccPrelu.886:36
  5487       attribute uniqueId 1
  5488         string-attr 89
  5489       attribute bvZ3Native 1
  5490         string-attr False
  5491       attribute weight 1
  5492         expr-attr
  5493           int-num 0
  5494     =
  5495     fun $read_version 2
  5496     var S
  5497       type-con $state 0
  5498     var p
  5499       type-con $ptr 0
  5500     fun $int_to_version 1
  5501     fun $select.mem 2
  5502     fun $memory 1
  5503     var S
  5504       type-con $state 0
  5505     var p
  5506       type-con $ptr 0
  5507 axiom 0
  5508     forall 2 1 4
  5509       var S
  5510         type-con $state 0
  5511       var p
  5512         type-con $ptr 0
  5513       pat 1
  5514         fun $domain 2
  5515         var S
  5516           type-con $state 0
  5517         var p
  5518           type-con $ptr 0
  5519       attribute qid 1
  5520         string-attr VccPrelu.889:30
  5521       attribute uniqueId 1
  5522         string-attr 90
  5523       attribute bvZ3Native 1
  5524         string-attr False
  5525       attribute weight 1
  5526         expr-attr
  5527           int-num 0
  5528     =
  5529     fun $domain 2
  5530     var S
  5531       type-con $state 0
  5532     var p
  5533       type-con $ptr 0
  5534     fun $ver_domain 1
  5535     fun $read_version 2
  5536     var S
  5537       type-con $state 0
  5538     var p
  5539       type-con $ptr 0
  5540 axiom 0
  5541     forall 4 1 4
  5542       var S
  5543         type-con $state 0
  5544       var p
  5545         type-con $ptr 0
  5546       var q
  5547         type-con $ptr 0
  5548       var l
  5549         type-con $label 0
  5550       pat 1
  5551         fun $in_domain_lab 4
  5552         var S
  5553           type-con $state 0
  5554         var p
  5555           type-con $ptr 0
  5556         var q
  5557           type-con $ptr 0
  5558         var l
  5559           type-con $label 0
  5560       attribute qid 1
  5561         string-attr VccPrelu.899:15
  5562       attribute uniqueId 1
  5563         string-attr 91
  5564       attribute bvZ3Native 1
  5565         string-attr False
  5566       attribute weight 1
  5567         expr-attr
  5568           int-num 0
  5569     implies
  5570     fun $in_domain_lab 4
  5571     var S
  5572       type-con $state 0
  5573     var p
  5574       type-con $ptr 0
  5575     var q
  5576       type-con $ptr 0
  5577     var l
  5578       type-con $label 0
  5579     fun $inv_lab 3
  5580     var S
  5581       type-con $state 0
  5582     var p
  5583       type-con $ptr 0
  5584     var l
  5585       type-con $label 0
  5586 axiom 0
  5587     forall 4 1 4
  5588       var S
  5589         type-con $state 0
  5590       var p
  5591         type-con $ptr 0
  5592       var q
  5593         type-con $ptr 0
  5594       var l
  5595         type-con $label 0
  5596       pat 1
  5597         fun $in_domain_lab 4
  5598         var S
  5599           type-con $state 0
  5600         var p
  5601           type-con $ptr 0
  5602         var q
  5603           type-con $ptr 0
  5604         var l
  5605           type-con $label 0
  5606       attribute qid 1
  5607         string-attr VccPrelu.902:15
  5608       attribute uniqueId 1
  5609         string-attr 92
  5610       attribute bvZ3Native 1
  5611         string-attr False
  5612       attribute weight 1
  5613         expr-attr
  5614           int-num 0
  5615     =
  5616     fun $in_domain_lab 4
  5617     var S
  5618       type-con $state 0
  5619     var p
  5620       type-con $ptr 0
  5621     var q
  5622       type-con $ptr 0
  5623     var l
  5624       type-con $label 0
  5625     fun $in_domain 3
  5626     var S
  5627       type-con $state 0
  5628     var p
  5629       type-con $ptr 0
  5630     var q
  5631       type-con $ptr 0
  5632 axiom 0
  5633     forall 4 1 4
  5634       var S
  5635         type-con $state 0
  5636       var p
  5637         type-con $ptr 0
  5638       var q
  5639         type-con $ptr 0
  5640       var l
  5641         type-con $label 0
  5642       pat 1
  5643         fun $in_vdomain_lab 4
  5644         var S
  5645           type-con $state 0
  5646         var p
  5647           type-con $ptr 0
  5648         var q
  5649           type-con $ptr 0
  5650         var l
  5651           type-con $label 0
  5652       attribute qid 1
  5653         string-attr VccPrelu.905:15
  5654       attribute uniqueId 1
  5655         string-attr 93
  5656       attribute bvZ3Native 1
  5657         string-attr False
  5658       attribute weight 1
  5659         expr-attr
  5660           int-num 0
  5661     implies
  5662     fun $in_vdomain_lab 4
  5663     var S
  5664       type-con $state 0
  5665     var p
  5666       type-con $ptr 0
  5667     var q
  5668       type-con $ptr 0
  5669     var l
  5670       type-con $label 0
  5671     fun $inv_lab 3
  5672     var S
  5673       type-con $state 0
  5674     var p
  5675       type-con $ptr 0
  5676     var l
  5677       type-con $label 0
  5678 axiom 0
  5679     forall 4 1 4
  5680       var S
  5681         type-con $state 0
  5682       var p
  5683         type-con $ptr 0
  5684       var q
  5685         type-con $ptr 0
  5686       var l
  5687         type-con $label 0
  5688       pat 1
  5689         fun $in_vdomain_lab 4
  5690         var S
  5691           type-con $state 0
  5692         var p
  5693           type-con $ptr 0
  5694         var q
  5695           type-con $ptr 0
  5696         var l
  5697           type-con $label 0
  5698       attribute qid 1
  5699         string-attr VccPrelu.908:15
  5700       attribute uniqueId 1
  5701         string-attr 94
  5702       attribute bvZ3Native 1
  5703         string-attr False
  5704       attribute weight 1
  5705         expr-attr
  5706           int-num 0
  5707     =
  5708     fun $in_vdomain_lab 4
  5709     var S
  5710       type-con $state 0
  5711     var p
  5712       type-con $ptr 0
  5713     var q
  5714       type-con $ptr 0
  5715     var l
  5716       type-con $label 0
  5717     fun $in_vdomain 3
  5718     var S
  5719       type-con $state 0
  5720     var p
  5721       type-con $ptr 0
  5722     var q
  5723       type-con $ptr 0
  5724 axiom 0
  5725     forall 3 1 4
  5726       var S
  5727         type-con $state 0
  5728       var p
  5729         type-con $ptr 0
  5730       var q
  5731         type-con $ptr 0
  5732       pat 1
  5733         fun $in_domain 3
  5734         var S
  5735           type-con $state 0
  5736         var p
  5737           type-con $ptr 0
  5738         var q
  5739           type-con $ptr 0
  5740       attribute qid 1
  5741         string-attr VccPrelu.914:15
  5742       attribute uniqueId 1
  5743         string-attr 96
  5744       attribute bvZ3Native 1
  5745         string-attr False
  5746       attribute weight 1
  5747         expr-attr
  5748           int-num 0
  5749     implies
  5750     fun $in_domain 3
  5751     var S
  5752       type-con $state 0
  5753     var p
  5754       type-con $ptr 0
  5755     var q
  5756       type-con $ptr 0
  5757     and 3
  5758     fun $set_in 2
  5759     var p
  5760       type-con $ptr 0
  5761     fun $domain 2
  5762     var S
  5763       type-con $state 0
  5764     var q
  5765       type-con $ptr 0
  5766     fun $closed 2
  5767     var S
  5768       type-con $state 0
  5769     var p
  5770       type-con $ptr 0
  5771     forall 1 1 3
  5772       var r
  5773         type-con $ptr 0
  5774       pat 1
  5775         fun $set_in 2
  5776         var r
  5777           type-con $ptr 0
  5778         fun $owns 2
  5779         var S
  5780           type-con $state 0
  5781         var p
  5782           type-con $ptr 0
  5783       attribute qid 1
  5784         string-attr VccPrelu.918:16
  5785       attribute uniqueId 1
  5786         string-attr 95
  5787       attribute bvZ3Native 1
  5788         string-attr False
  5789     implies
  5790     and 2
  5791     not
  5792     fun $has_volatile_owns_set 1
  5793     fun $typ 1
  5794     var p
  5795       type-con $ptr 0
  5796     fun $set_in 2
  5797     var r
  5798       type-con $ptr 0
  5799     fun $owns 2
  5800     var S
  5801       type-con $state 0
  5802     var p
  5803       type-con $ptr 0
  5804     fun $set_in2 2
  5805     var r
  5806       type-con $ptr 0
  5807     fun $ver_domain 1
  5808     fun $read_version 2
  5809     var S
  5810       type-con $state 0
  5811     var q
  5812       type-con $ptr 0
  5813 axiom 0
  5814     forall 2 1 3
  5815       var S
  5816         type-con $state 0
  5817       var p
  5818         type-con $ptr 0
  5819       pat 1
  5820         fun $in_domain 3
  5821         var S
  5822           type-con $state 0
  5823         var p
  5824           type-con $ptr 0
  5825         var p
  5826           type-con $ptr 0
  5827       attribute qid 1
  5828         string-attr VccPrelu.923:15
  5829       attribute uniqueId 1
  5830         string-attr 97
  5831       attribute bvZ3Native 1
  5832         string-attr False
  5833     implies
  5834     and 7
  5835     fun $full_stop 1
  5836     var S
  5837       type-con $state 0
  5838     fun $closed 2
  5839     var S
  5840       type-con $state 0
  5841     var p
  5842       type-con $ptr 0
  5843     =
  5844     fun $owner 2
  5845     var S
  5846       type-con $state 0
  5847     var p
  5848       type-con $ptr 0
  5849     fun $me 0
  5850     fun $is 2
  5851     var p
  5852       type-con $ptr 0
  5853     fun $typ 1
  5854     var p
  5855       type-con $ptr 0
  5856     fun $typed 2
  5857     var S
  5858       type-con $state 0
  5859     var p
  5860       type-con $ptr 0
  5861     not
  5862     =
  5863     fun $kind_of 1
  5864     fun $typ 1
  5865     var p
  5866       type-con $ptr 0
  5867     fun $kind_primitive 0
  5868     fun $is_non_primitive 1
  5869     fun $typ 1
  5870     var p
  5871       type-con $ptr 0
  5872     fun $in_domain 3
  5873     var S
  5874       type-con $state 0
  5875     var p
  5876       type-con $ptr 0
  5877     var p
  5878       type-con $ptr 0
  5879 axiom 0
  5880     forall 3 1 4
  5881       var S
  5882         type-con $state 0
  5883       var p
  5884         type-con $ptr 0
  5885       var q
  5886         type-con $ptr 0
  5887       pat 1
  5888         fun $in_domain 3
  5889         var S
  5890           type-con $state 0
  5891         var q
  5892           type-con $ptr 0
  5893         var p
  5894           type-con $ptr 0
  5895       attribute qid 1
  5896         string-attr VccPrelu.932:15
  5897       attribute uniqueId 1
  5898         string-attr 98
  5899       attribute bvZ3Native 1
  5900         string-attr False
  5901       attribute weight 1
  5902         expr-attr
  5903           int-num 0
  5904     implies
  5905     and 2
  5906     fun $full_stop 1
  5907     var S
  5908       type-con $state 0
  5909     fun $set_in 2
  5910     var q
  5911       type-con $ptr 0
  5912     fun $domain 2
  5913     var S
  5914       type-con $state 0
  5915     var p
  5916       type-con $ptr 0
  5917     fun $in_domain 3
  5918     var S
  5919       type-con $state 0
  5920     var q
  5921       type-con $ptr 0
  5922     var p
  5923       type-con $ptr 0
  5924 axiom 0
  5925     forall 4 1 4
  5926       var S
  5927         type-con $state 0
  5928       var p
  5929         type-con $ptr 0
  5930       var q
  5931         type-con $ptr 0
  5932       var r
  5933         type-con $ptr 0
  5934       pat 2
  5935         fun $set_in 2
  5936         var q
  5937           type-con $ptr 0
  5938         fun $domain 2
  5939         var S
  5940           type-con $state 0
  5941         var p
  5942           type-con $ptr 0
  5943         fun $in_domain 3
  5944         var S
  5945           type-con $state 0
  5946         var r
  5947           type-con $ptr 0
  5948         var p
  5949           type-con $ptr 0
  5950       attribute qid 1
  5951         string-attr VccPrelu.936:15
  5952       attribute uniqueId 1
  5953         string-attr 99
  5954       attribute bvZ3Native 1
  5955         string-attr False
  5956       attribute weight 1
  5957         expr-attr
  5958           int-num 0
  5959     implies
  5960     and 3
  5961     not
  5962     fun $has_volatile_owns_set 1
  5963     fun $typ 1
  5964     var q
  5965       type-con $ptr 0
  5966     fun $set_in 2
  5967     var q
  5968       type-con $ptr 0
  5969     fun $domain 2
  5970     var S
  5971       type-con $state 0
  5972     var p
  5973       type-con $ptr 0
  5974     fun $set_in0 2
  5975     var r
  5976       type-con $ptr 0
  5977     fun $owns 2
  5978     var S
  5979       type-con $state 0
  5980     var q
  5981       type-con $ptr 0
  5982     and 2
  5983     fun $in_domain 3
  5984     var S
  5985       type-con $state 0
  5986     var r
  5987       type-con $ptr 0
  5988     var p
  5989       type-con $ptr 0
  5990     fun $set_in0 2
  5991     var r
  5992       type-con $ptr 0
  5993     fun $owns 2
  5994     var S
  5995       type-con $state 0
  5996     var q
  5997       type-con $ptr 0
  5998 axiom 0
  5999     forall 4 1 4
  6000       var S
  6001         type-con $state 0
  6002       var p
  6003         type-con $ptr 0
  6004       var q
  6005         type-con $ptr 0
  6006       var r
  6007         type-con $ptr 0
  6008       pat 2
  6009         fun $set_in 2
  6010         var q
  6011           type-con $ptr 0
  6012         fun $domain 2
  6013         var S
  6014           type-con $state 0
  6015         var p
  6016           type-con $ptr 0
  6017         fun $in_vdomain 3
  6018         var S
  6019           type-con $state 0
  6020         var r
  6021           type-con $ptr 0
  6022         var p
  6023           type-con $ptr 0
  6024       attribute qid 1
  6025         string-attr VccPrelu.941:15
  6026       attribute uniqueId 1
  6027         string-attr 101
  6028       attribute bvZ3Native 1
  6029         string-attr False
  6030       attribute weight 1
  6031         expr-attr
  6032           int-num 0
  6033     implies
  6034     and 3
  6035     fun $has_volatile_owns_set 1
  6036     fun $typ 1
  6037     var q
  6038       type-con $ptr 0
  6039     fun $set_in 2
  6040     var q
  6041       type-con $ptr 0
  6042     fun $domain 2
  6043     var S
  6044       type-con $state 0
  6045     var p
  6046       type-con $ptr 0
  6047     forall 1 0 3
  6048       var S1
  6049         type-con $state 0
  6050       attribute qid 1
  6051         string-attr VccPrelu.945:11
  6052       attribute uniqueId 1
  6053         string-attr 100
  6054       attribute bvZ3Native 1
  6055         string-attr False
  6056     implies
  6057     and 3
  6058     fun $inv2 4
  6059     var S1
  6060       type-con $state 0
  6061     var S1
  6062       type-con $state 0
  6063     var q
  6064       type-con $ptr 0
  6065     fun $typ 1
  6066     var q
  6067       type-con $ptr 0
  6068     =
  6069     fun $read_version 2
  6070     var S1
  6071       type-con $state 0
  6072     var p
  6073       type-con $ptr 0
  6074     fun $read_version 2
  6075     var S
  6076       type-con $state 0
  6077     var p
  6078       type-con $ptr 0
  6079     =
  6080     fun $domain 2
  6081     var S1
  6082       type-con $state 0
  6083     var p
  6084       type-con $ptr 0
  6085     fun $domain 2
  6086     var S
  6087       type-con $state 0
  6088     var p
  6089       type-con $ptr 0
  6090     fun $set_in0 2
  6091     var r
  6092       type-con $ptr 0
  6093     fun $owns 2
  6094     var S1
  6095       type-con $state 0
  6096     var q
  6097       type-con $ptr 0
  6098     and 2
  6099     fun $in_vdomain 3
  6100     var S
  6101       type-con $state 0
  6102     var r
  6103       type-con $ptr 0
  6104     var p
  6105       type-con $ptr 0
  6106     fun $set_in0 2
  6107     var r
  6108       type-con $ptr 0
  6109     fun $owns 2
  6110     var S
  6111       type-con $state 0
  6112     var q
  6113       type-con $ptr 0
  6114 axiom 0
  6115     forall 3 1 4
  6116       var S
  6117         type-con $state 0
  6118       var p
  6119         type-con $ptr 0
  6120       var q
  6121         type-con $ptr 0
  6122       pat 1
  6123         fun $in_vdomain 3
  6124         var S
  6125           type-con $state 0
  6126         var p
  6127           type-con $ptr 0
  6128         var q
  6129           type-con $ptr 0
  6130       attribute qid 1
  6131         string-attr VccPrelu.952:15
  6132       attribute uniqueId 1
  6133         string-attr 102
  6134       attribute bvZ3Native 1
  6135         string-attr False
  6136       attribute weight 1
  6137         expr-attr
  6138           int-num 0
  6139     implies
  6140     fun $in_vdomain 3
  6141     var S
  6142       type-con $state 0
  6143     var p
  6144       type-con $ptr 0
  6145     var q
  6146       type-con $ptr 0
  6147     fun $in_domain 3
  6148     var S
  6149       type-con $state 0
  6150     var p
  6151       type-con $ptr 0
  6152     var q
  6153       type-con $ptr 0
  6154 axiom 0
  6155     forall 4 1 3
  6156       var S
  6157         type-con $state 0
  6158       var p
  6159         type-con $ptr 0
  6160       var d
  6161         type-con $ptr 0
  6162       var f
  6163         type-con $field 0
  6164       pat 3
  6165         fun $set_in 2
  6166         var p
  6167           type-con $ptr 0
  6168         fun $domain 2
  6169         var S
  6170           type-con $state 0
  6171         var d
  6172           type-con $ptr 0
  6173         fun $is_primitive_non_volatile_field 1
  6174         var f
  6175           type-con $field 0
  6176         fun $select.mem 2
  6177         fun $memory 1
  6178         var S
  6179           type-con $state 0
  6180         fun $dot 2
  6181         var p
  6182           type-con $ptr 0
  6183         var f
  6184           type-con $field 0
  6185       attribute qid 1
  6186         string-attr VccPrelu.957:15
  6187       attribute uniqueId 1
  6188         string-attr 103
  6189       attribute bvZ3Native 1
  6190         string-attr False
  6191     implies
  6192     and 2
  6193     fun $set_in 2
  6194     var p
  6195       type-con $ptr 0
  6196     fun $domain 2
  6197     var S
  6198       type-con $state 0
  6199     var d
  6200       type-con $ptr 0
  6201     fun $is_primitive_non_volatile_field 1
  6202     var f
  6203       type-con $field 0
  6204     =
  6205     fun $select.mem 2
  6206     fun $memory 1
  6207     var S
  6208       type-con $state 0
  6209     fun $dot 2
  6210     var p
  6211       type-con $ptr 0
  6212     var f
  6213       type-con $field 0
  6214     fun $fetch_from_domain 2
  6215     fun $read_version 2
  6216     var S
  6217       type-con $state 0
  6218     var d
  6219       type-con $ptr 0
  6220     fun $dot 2
  6221     var p
  6222       type-con $ptr 0
  6223     var f
  6224       type-con $field 0
  6225 axiom 0
  6226     forall 3 2 3
  6227       var S
  6228         type-con $state 0
  6229       var p
  6230         type-con $ptr 0
  6231       var d
  6232         type-con $ptr 0
  6233       pat 3
  6234         fun $full_stop 1
  6235         var S
  6236           type-con $state 0
  6237         fun $set_in 2
  6238         var p
  6239           type-con $ptr 0
  6240         fun $domain 2
  6241         var S
  6242           type-con $state 0
  6243         var d
  6244           type-con $ptr 0
  6245         fun $select.sm 2
  6246         fun $statusmap 1
  6247         var S
  6248           type-con $state 0
  6249         var p
  6250           type-con $ptr 0
  6251       pat 3
  6252         fun $full_stop 1
  6253         var S
  6254           type-con $state 0
  6255         fun $set_in 2
  6256         var p
  6257           type-con $ptr 0
  6258         fun $domain 2
  6259         var S
  6260           type-con $state 0
  6261         var d
  6262           type-con $ptr 0
  6263         fun $select.tm 2
  6264         fun $typemap 1
  6265         var S
  6266           type-con $state 0
  6267         var p
  6268           type-con $ptr 0
  6269       attribute qid 1
  6270         string-attr VccPrelu.962:15
  6271       attribute uniqueId 1
  6272         string-attr 104
  6273       attribute bvZ3Native 1
  6274         string-attr False
  6275     implies
  6276     and 2
  6277     fun $full_stop 1
  6278     var S
  6279       type-con $state 0
  6280     fun $set_in 2
  6281     var p
  6282       type-con $ptr 0
  6283     fun $domain 2
  6284     var S
  6285       type-con $state 0
  6286     var d
  6287       type-con $ptr 0
  6288     and 2
  6289     fun $typed 2
  6290     var S
  6291       type-con $state 0
  6292     var p
  6293       type-con $ptr 0
  6294     not
  6295     fun $ts_is_volatile 1
  6296     fun $select.tm 2
  6297     fun $typemap 1
  6298     var S
  6299       type-con $state 0
  6300     var p
  6301       type-con $ptr 0
  6302 axiom 0
  6303     forall 4 2 3
  6304       var S
  6305         type-con $state 0
  6306       var p
  6307         type-con $ptr 0
  6308       var d
  6309         type-con $ptr 0
  6310       var f
  6311         type-con $field 0
  6312       pat 3
  6313         fun $set_in 2
  6314         var p
  6315           type-con $ptr 0
  6316         fun $domain 2
  6317         var S
  6318           type-con $state 0
  6319         var d
  6320           type-con $ptr 0
  6321         fun $is_primitive_non_volatile_field 1
  6322         var f
  6323           type-con $field 0
  6324         fun $owner 2
  6325         var S
  6326           type-con $state 0
  6327         fun $dot 2
  6328         var p
  6329           type-con $ptr 0
  6330         var f
  6331           type-con $field 0
  6332       pat 3
  6333         fun $set_in 2
  6334         var p
  6335           type-con $ptr 0
  6336         fun $domain 2
  6337         var S
  6338           type-con $state 0
  6339         var d
  6340           type-con $ptr 0
  6341         fun $is_primitive_non_volatile_field 1
  6342         var f
  6343           type-con $field 0
  6344         fun $select.tm 2
  6345         fun $typemap 1
  6346         var S
  6347           type-con $state 0
  6348         fun $dot 2
  6349         var p
  6350           type-con $ptr 0
  6351         var f
  6352           type-con $field 0
  6353       attribute qid 1
  6354         string-attr VccPrelu.968:15
  6355       attribute uniqueId 1
  6356         string-attr 105
  6357       attribute bvZ3Native 1
  6358         string-attr False
  6359     implies
  6360     and 3
  6361     fun $full_stop 1
  6362     var S
  6363       type-con $state 0
  6364     fun $set_in 2
  6365     var p
  6366       type-con $ptr 0
  6367     fun $domain 2
  6368     var S
  6369       type-con $state 0
  6370     var d
  6371       type-con $ptr 0
  6372     fun $is_primitive_non_volatile_field 1
  6373     var f
  6374       type-con $field 0
  6375     and 2
  6376     fun $typed 2
  6377     var S
  6378       type-con $state 0
  6379     fun $dot 2
  6380     var p
  6381       type-con $ptr 0
  6382     var f
  6383       type-con $field 0
  6384     not
  6385     fun $ts_is_volatile 1
  6386     fun $select.tm 2
  6387     fun $typemap 1
  6388     var S
  6389       type-con $state 0
  6390     fun $dot 2
  6391     var p
  6392       type-con $ptr 0
  6393     var f
  6394       type-con $field 0
  6395 axiom 0
  6396     forall 7 1 3
  6397       var S
  6398         type-con $state 0
  6399       var p
  6400         type-con $ptr 0
  6401       var d
  6402         type-con $ptr 0
  6403       var f
  6404         type-con $field 0
  6405       var sz
  6406         int
  6407       var i
  6408         int
  6409       var t
  6410         type-con $ctype 0
  6411       pat 3
  6412         fun $set_in 2
  6413         var p
  6414           type-con $ptr 0
  6415         fun $domain 2
  6416         var S
  6417           type-con $state 0
  6418         var d
  6419           type-con $ptr 0
  6420         fun $is_primitive_embedded_array 2
  6421         var f
  6422           type-con $field 0
  6423         var sz
  6424           int
  6425         fun $select.mem 2
  6426         fun $memory 1
  6427         var S
  6428           type-con $state 0
  6429         fun $idx 3
  6430         fun $dot 2
  6431         var p
  6432           type-con $ptr 0
  6433         var f
  6434           type-con $field 0
  6435         var i
  6436           int
  6437         var t
  6438           type-con $ctype 0
  6439       attribute qid 1
  6440         string-attr VccPrelu.974:15
  6441       attribute uniqueId 1
  6442         string-attr 106
  6443       attribute bvZ3Native 1
  6444         string-attr False
  6445     implies
  6446     and 5
  6447     fun $full_stop 1
  6448     var S
  6449       type-con $state 0
  6450     fun $set_in 2
  6451     var p
  6452       type-con $ptr 0
  6453     fun $domain 2
  6454     var S
  6455       type-con $state 0
  6456     var d
  6457       type-con $ptr 0
  6458     fun $is_primitive_embedded_array 2
  6459     var f
  6460       type-con $field 0
  6461     var sz
  6462       int
  6463     <=
  6464     int-num 0
  6465     var i
  6466       int
  6467     <
  6468     var i
  6469       int
  6470     var sz
  6471       int
  6472     =
  6473     fun $select.mem 2
  6474     fun $memory 1
  6475     var S
  6476       type-con $state 0
  6477     fun $idx 3
  6478     fun $dot 2
  6479     var p
  6480       type-con $ptr 0
  6481     var f
  6482       type-con $field 0
  6483     var i
  6484       int
  6485     var t
  6486       type-con $ctype 0
  6487     fun $fetch_from_domain 2
  6488     fun $read_version 2
  6489     var S
  6490       type-con $state 0
  6491     var d
  6492       type-con $ptr 0
  6493     fun $idx 3
  6494     fun $dot 2
  6495     var p
  6496       type-con $ptr 0
  6497     var f
  6498       type-con $field 0
  6499     var i
  6500       int
  6501     var t
  6502       type-con $ctype 0
  6503 axiom 0
  6504     forall 7 2 3
  6505       var S
  6506         type-con $state 0
  6507       var p
  6508         type-con $ptr 0
  6509       var d
  6510         type-con $ptr 0
  6511       var f
  6512         type-con $field 0
  6513       var sz
  6514         int
  6515       var i
  6516         int
  6517       var t
  6518         type-con $ctype 0
  6519       pat 3
  6520         fun $set_in 2
  6521         var p
  6522           type-con $ptr 0
  6523         fun $domain 2
  6524         var S
  6525           type-con $state 0
  6526         var d
  6527           type-con $ptr 0
  6528         fun $is_primitive_embedded_array 2
  6529         var f
  6530           type-con $field 0
  6531         var sz
  6532           int
  6533         fun $select.tm 2
  6534         fun $typemap 1
  6535         var S
  6536           type-con $state 0
  6537         fun $idx 3
  6538         fun $dot 2
  6539         var p
  6540           type-con $ptr 0
  6541         var f
  6542           type-con $field 0
  6543         var i
  6544           int
  6545         var t
  6546           type-con $ctype 0
  6547       pat 3
  6548         fun $set_in 2
  6549         var p
  6550           type-con $ptr 0
  6551         fun $domain 2
  6552         var S
  6553           type-con $state 0
  6554         var d
  6555           type-con $ptr 0
  6556         fun $is_primitive_embedded_array 2
  6557         var f
  6558           type-con $field 0
  6559         var sz
  6560           int
  6561         fun $owner 2
  6562         var S
  6563           type-con $state 0
  6564         fun $idx 3
  6565         fun $dot 2
  6566         var p
  6567           type-con $ptr 0
  6568         var f
  6569           type-con $field 0
  6570         var i
  6571           int
  6572         var t
  6573           type-con $ctype 0
  6574       attribute qid 1
  6575         string-attr VccPrelu.979:15
  6576       attribute uniqueId 1
  6577         string-attr 107
  6578       attribute bvZ3Native 1
  6579         string-attr False
  6580     implies
  6581     and 5
  6582     fun $full_stop 1
  6583     var S
  6584       type-con $state 0
  6585     fun $set_in 2
  6586     var p
  6587       type-con $ptr 0
  6588     fun $domain 2
  6589     var S
  6590       type-con $state 0
  6591     var d
  6592       type-con $ptr 0
  6593     fun $is_primitive_embedded_array 2
  6594     var f
  6595       type-con $field 0
  6596     var sz
  6597       int
  6598     <=
  6599     int-num 0
  6600     var i
  6601       int
  6602     <
  6603     var i
  6604       int
  6605     var sz
  6606       int
  6607     and 2
  6608     fun $typed 2
  6609     var S
  6610       type-con $state 0
  6611     fun $idx 3
  6612     fun $dot 2
  6613     var p
  6614       type-con $ptr 0
  6615     var f
  6616       type-con $field 0
  6617     var i
  6618       int
  6619     var t
  6620       type-con $ctype 0
  6621     not
  6622     fun $ts_is_volatile 1
  6623     fun $select.tm 2
  6624     fun $typemap 1
  6625     var S
  6626       type-con $state 0
  6627     fun $idx 3
  6628     fun $dot 2
  6629     var p
  6630       type-con $ptr 0
  6631     var f
  6632       type-con $field 0
  6633     var i
  6634       int
  6635     var t
  6636       type-con $ctype 0
  6637 axiom 0
  6638     forall 6 2 3
  6639       var S
  6640         type-con $state 0
  6641       var r
  6642         int
  6643       var d
  6644         type-con $ptr 0
  6645       var sz
  6646         int
  6647       var i
  6648         int
  6649       var t
  6650         type-con $ctype 0
  6651       pat 3
  6652         fun $set_in 2
  6653         fun $ptr 2
  6654         fun $array 2
  6655         var t
  6656           type-con $ctype 0
  6657         var sz
  6658           int
  6659         var r
  6660           int
  6661         fun $domain 2
  6662         var S
  6663           type-con $state 0
  6664         var d
  6665           type-con $ptr 0
  6666         fun $select.tm 2
  6667         fun $typemap 1
  6668         var S
  6669           type-con $state 0
  6670         fun $idx 3
  6671         fun $ptr 2
  6672         var t
  6673           type-con $ctype 0
  6674         var r
  6675           int
  6676         var i
  6677           int
  6678         var t
  6679           type-con $ctype 0
  6680         fun $is_primitive 1
  6681         var t
  6682           type-con $ctype 0
  6683       pat 3
  6684         fun $set_in 2
  6685         fun $ptr 2
  6686         fun $array 2
  6687         var t
  6688           type-con $ctype 0
  6689         var sz
  6690           int
  6691         var r
  6692           int
  6693         fun $domain 2
  6694         var S
  6695           type-con $state 0
  6696         var d
  6697           type-con $ptr 0
  6698         fun $owner 2
  6699         var S
  6700           type-con $state 0
  6701         fun $idx 3
  6702         fun $ptr 2
  6703         var t
  6704           type-con $ctype 0
  6705         var r
  6706           int
  6707         var i
  6708           int
  6709         var t
  6710           type-con $ctype 0
  6711         fun $is_primitive 1
  6712         var t
  6713           type-con $ctype 0
  6714       attribute qid 1
  6715         string-attr VccPrelu.985:15
  6716       attribute uniqueId 1
  6717         string-attr 108
  6718       attribute bvZ3Native 1
  6719         string-attr False
  6720     implies
  6721     and 5
  6722     fun $full_stop 1
  6723     var S
  6724       type-con $state 0
  6725     fun $is_primitive 1
  6726     var t
  6727       type-con $ctype 0
  6728     fun $set_in 2
  6729     fun $ptr 2
  6730     fun $array 2
  6731     var t
  6732       type-con $ctype 0
  6733     var sz
  6734       int
  6735     var r
  6736       int
  6737     fun $domain 2
  6738     var S
  6739       type-con $state 0
  6740     var d
  6741       type-con $ptr 0
  6742     <=
  6743     int-num 0
  6744     var i
  6745       int
  6746     <
  6747     var i
  6748       int
  6749     var sz
  6750       int
  6751     and 2
  6752     fun $typed 2
  6753     var S
  6754       type-con $state 0
  6755     fun $idx 3
  6756     fun $ptr 2
  6757     var t
  6758       type-con $ctype 0
  6759     var r
  6760       int
  6761     var i
  6762       int
  6763     var t
  6764       type-con $ctype 0
  6765     not
  6766     fun $ts_is_volatile 1
  6767     fun $select.tm 2
  6768     fun $typemap 1
  6769     var S
  6770       type-con $state 0
  6771     fun $idx 3
  6772     fun $ptr 2
  6773     var t
  6774       type-con $ctype 0
  6775     var r
  6776       int
  6777     var i
  6778       int
  6779     var t
  6780       type-con $ctype 0
  6781 axiom 0
  6782     forall 6 1 3
  6783       var S
  6784         type-con $state 0
  6785       var r
  6786         int
  6787       var d
  6788         type-con $ptr 0
  6789       var sz
  6790         int
  6791       var i
  6792         int
  6793       var t
  6794         type-con $ctype 0
  6795       pat 3
  6796         fun $set_in 2
  6797         fun $ptr 2
  6798         fun $array 2
  6799         var t
  6800           type-con $ctype 0
  6801         var sz
  6802           int
  6803         var r
  6804           int
  6805         fun $domain 2
  6806         var S
  6807           type-con $state 0
  6808         var d
  6809           type-con $ptr 0
  6810         fun $select.mem 2
  6811         fun $memory 1
  6812         var S
  6813           type-con $state 0
  6814         fun $idx 3
  6815         fun $ptr 2
  6816         var t
  6817           type-con $ctype 0
  6818         var r
  6819           int
  6820         var i
  6821           int
  6822         var t
  6823           type-con $ctype 0
  6824         fun $is_primitive 1
  6825         var t
  6826           type-con $ctype 0
  6827       attribute qid 1
  6828         string-attr VccPrelu.994:15
  6829       attribute uniqueId 1
  6830         string-attr 109
  6831       attribute bvZ3Native 1
  6832         string-attr False
  6833     implies
  6834     and 5
  6835     fun $full_stop 1
  6836     var S
  6837       type-con $state 0
  6838     fun $is_primitive 1
  6839     var t
  6840       type-con $ctype 0
  6841     fun $set_in 2
  6842     fun $ptr 2
  6843     fun $array 2
  6844     var t
  6845       type-con $ctype 0
  6846     var sz
  6847       int
  6848     var r
  6849       int
  6850     fun $domain 2
  6851     var S
  6852       type-con $state 0
  6853     var d
  6854       type-con $ptr 0
  6855     <=
  6856     int-num 0
  6857     var i
  6858       int
  6859     <
  6860     var i
  6861       int
  6862     var sz
  6863       int
  6864     =
  6865     fun $select.mem 2
  6866     fun $memory 1
  6867     var S
  6868       type-con $state 0
  6869     fun $idx 3
  6870     fun $ptr 2
  6871     var t
  6872       type-con $ctype 0
  6873     var r
  6874       int
  6875     var i
  6876       int
  6877     var t
  6878       type-con $ctype 0
  6879     fun $fetch_from_domain 2
  6880     fun $read_version 2
  6881     var S
  6882       type-con $state 0
  6883     var d
  6884       type-con $ptr 0
  6885     fun $idx 3
  6886     fun $ptr 2
  6887     var t
  6888       type-con $ctype 0
  6889     var r
  6890       int
  6891     var i
  6892       int
  6893     var t
  6894       type-con $ctype 0
  6895 axiom 0
  6896     forall 6 1 3
  6897       var S
  6898         type-con $state 0
  6899       var p
  6900         type-con $ptr 0
  6901       var f
  6902         type-con $field 0
  6903       var sz
  6904         int
  6905       var i
  6906         int
  6907       var t
  6908         type-con $ctype 0
  6909       pat 2
  6910         fun $is_primitive_embedded_volatile_array 3
  6911         var f
  6912           type-con $field 0
  6913         var sz
  6914           int
  6915         var t
  6916           type-con $ctype 0
  6917         fun $ts_is_volatile 1
  6918         fun $select.tm 2
  6919         fun $typemap 1
  6920         var S
  6921           type-con $state 0
  6922         fun $idx 3
  6923         fun $dot 2
  6924         var p
  6925           type-con $ptr 0
  6926         var f
  6927           type-con $field 0
  6928         var i
  6929           int
  6930         var t
  6931           type-con $ctype 0
  6932       attribute qid 1
  6933         string-attr VccPrelu.1002:15
  6934       attribute uniqueId 1
  6935         string-attr 110
  6936       attribute bvZ3Native 1
  6937         string-attr False
  6938     implies
  6939     and 4
  6940     fun $good_state 1
  6941     var S
  6942       type-con $state 0
  6943     fun $is_primitive_embedded_volatile_array 3
  6944     var f
  6945       type-con $field 0
  6946     var sz
  6947       int
  6948     var t
  6949       type-con $ctype 0
  6950     <=
  6951     int-num 0
  6952     var i
  6953       int
  6954     <
  6955     var i
  6956       int
  6957     var sz
  6958       int
  6959     fun $ts_is_volatile 1
  6960     fun $select.tm 2
  6961     fun $typemap 1
  6962     var S
  6963       type-con $state 0
  6964     fun $idx 3
  6965     fun $dot 2
  6966     var p
  6967       type-con $ptr 0
  6968     var f
  6969       type-con $field 0
  6970     var i
  6971       int
  6972     var t
  6973       type-con $ctype 0
  6974 axiom 0
  6975     forall 4 1 4
  6976       var p
  6977         type-con $ptr 0
  6978       var S1
  6979         type-con $state 0
  6980       var S2
  6981         type-con $state 0
  6982       var q
  6983         type-con $ptr 0
  6984       pat 2
  6985         fun $set_in 2
  6986         var q
  6987           type-con $ptr 0
  6988         fun $domain 2
  6989         var S1
  6990           type-con $state 0
  6991         var p
  6992           type-con $ptr 0
  6993         fun $call_transition 2
  6994         var S1
  6995           type-con $state 0
  6996         var S2
  6997           type-con $state 0
  6998       attribute qid 1
  6999         string-attr VccPrelu.1013:15
  7000       attribute uniqueId 1
  7001         string-attr 111
  7002       attribute bvZ3Native 1
  7003         string-attr False
  7004       attribute weight 1
  7005         expr-attr
  7006           int-num 0
  7007     fun $instantiate_bool 1
  7008     fun $set_in 2
  7009     var q
  7010       type-con $ptr 0
  7011     fun $domain 2
  7012     var S2
  7013       type-con $state 0
  7014     var p
  7015       type-con $ptr 0
  7016 axiom 0
  7017     forall 4 1 4
  7018       var p
  7019         type-con $ptr 0
  7020       var S1
  7021         type-con $state 0
  7022       var S2
  7023         type-con $state 0
  7024       var q
  7025         type-con $ptr 0
  7026       pat 2
  7027         fun $set_in 2
  7028         var q
  7029           type-con $ptr 0
  7030         fun $ver_domain 1
  7031         fun $read_version 2
  7032         var S1
  7033           type-con $state 0
  7034         var p
  7035           type-con $ptr 0
  7036         fun $call_transition 2
  7037         var S1
  7038           type-con $state 0
  7039         var S2
  7040           type-con $state 0
  7041       attribute qid 1
  7042         string-attr VccPrelu.1017:15
  7043       attribute uniqueId 1
  7044         string-attr 112
  7045       attribute bvZ3Native 1
  7046         string-attr False
  7047       attribute weight 1
  7048         expr-attr
  7049           int-num 0
  7050     fun $instantiate_bool 1
  7051     fun $set_in 2
  7052     var q
  7053       type-con $ptr 0
  7054     fun $ver_domain 1
  7055     fun $read_version 2
  7056     var S2
  7057       type-con $state 0
  7058     var p
  7059       type-con $ptr 0
  7060 axiom 0
  7061     forall 2 1 3
  7062       var p
  7063         type-con $ptr 0
  7064       var c
  7065         type-con $ptr 0
  7066       pat 1
  7067         fun $in_claim_domain 2
  7068         var p
  7069           type-con $ptr 0
  7070         var c
  7071           type-con $ptr 0
  7072       attribute qid 1
  7073         string-attr VccPrelu.1022:15
  7074       attribute uniqueId 1
  7075         string-attr 114
  7076       attribute bvZ3Native 1
  7077         string-attr False
  7078     implies
  7079     forall 1 1 3
  7080       var s
  7081         type-con $state 0
  7082       pat 1
  7083         fun $dont_instantiate_state 1
  7084         var s
  7085           type-con $state 0
  7086       attribute qid 1
  7087         string-attr VccPrelu.1023:11
  7088       attribute uniqueId 1
  7089         string-attr 113
  7090       attribute bvZ3Native 1
  7091         string-attr False
  7092     implies
  7093     fun $valid_claim 2
  7094     var s
  7095       type-con $state 0
  7096     var c
  7097       type-con $ptr 0
  7098     fun $closed 2
  7099     var s
  7100       type-con $state 0
  7101     var p
  7102       type-con $ptr 0
  7103     fun $in_claim_domain 2
  7104     var p
  7105       type-con $ptr 0
  7106     var c
  7107       type-con $ptr 0
  7108 axiom 0
  7109     forall 4 1 4
  7110       var S
  7111         type-con $state 0
  7112       var c
  7113         type-con $ptr 0
  7114       var obj
  7115         type-con $ptr 0
  7116       var ptr
  7117         type-con $ptr 0
  7118       pat 1
  7119         fun $by_claim 4
  7120         var S
  7121           type-con $state 0
  7122         var c
  7123           type-con $ptr 0
  7124         var obj
  7125           type-con $ptr 0
  7126         var ptr
  7127           type-con $ptr 0
  7128       attribute qid 1
  7129         string-attr VccPrelu.1026:32
  7130       attribute uniqueId 1
  7131         string-attr 115
  7132       attribute bvZ3Native 1
  7133         string-attr False
  7134       attribute weight 1
  7135         expr-attr
  7136           int-num 0
  7137     =
  7138     fun $by_claim 4
  7139     var S
  7140       type-con $state 0
  7141     var c
  7142       type-con $ptr 0
  7143     var obj
  7144       type-con $ptr 0
  7145     var ptr
  7146       type-con $ptr 0
  7147     var ptr
  7148       type-con $ptr 0
  7149 axiom 0
  7150     forall 4 2 3
  7151       var S
  7152         type-con $state 0
  7153       var p
  7154         type-con $ptr 0
  7155       var c
  7156         type-con $ptr 0
  7157       var f
  7158         type-con $field 0
  7159       pat 2
  7160         fun $in_claim_domain 2
  7161         var p
  7162           type-con $ptr 0
  7163         var c
  7164           type-con $ptr 0
  7165         fun $select.mem 2
  7166         fun $memory 1
  7167         var S
  7168           type-con $state 0
  7169         fun $dot 2
  7170         var p
  7171           type-con $ptr 0
  7172         var f
  7173           type-con $field 0
  7174       pat 1
  7175         fun $by_claim 4
  7176         var S
  7177           type-con $state 0
  7178         var c
  7179           type-con $ptr 0
  7180         var p
  7181           type-con $ptr 0
  7182         fun $dot 2
  7183         var p
  7184           type-con $ptr 0
  7185         var f
  7186           type-con $field 0
  7187       attribute qid 1
  7188         string-attr VccPrelu.1031:15
  7189       attribute uniqueId 1
  7190         string-attr 116
  7191       attribute bvZ3Native 1
  7192         string-attr False
  7193     implies
  7194     and 4
  7195     fun $good_state 1
  7196     var S
  7197       type-con $state 0
  7198     fun $closed 2
  7199     var S
  7200       type-con $state 0
  7201     var c
  7202       type-con $ptr 0
  7203     fun $in_claim_domain 2
  7204     var p
  7205       type-con $ptr 0
  7206     var c
  7207       type-con $ptr 0
  7208     fun $is_primitive_non_volatile_field 1
  7209     var f
  7210       type-con $field 0
  7211     and 2
  7212     fun $in_claim_domain 2
  7213     var p
  7214       type-con $ptr 0
  7215     var c
  7216       type-con $ptr 0
  7217     =
  7218     fun $select.mem 2
  7219     fun $memory 1
  7220     var S
  7221       type-con $state 0
  7222     fun $dot 2
  7223     var p
  7224       type-con $ptr 0
  7225     var f
  7226       type-con $field 0
  7227     fun $fetch_from_domain 2
  7228     fun $claim_version 1
  7229     var c
  7230       type-con $ptr 0
  7231     fun $dot 2
  7232     var p
  7233       type-con $ptr 0
  7234     var f
  7235       type-con $field 0
  7236 axiom 0
  7237     forall 7 2 3
  7238       var S
  7239         type-con $state 0
  7240       var p
  7241         type-con $ptr 0
  7242       var c
  7243         type-con $ptr 0