bench/check-ce/oracles/map_of_algebraic_Alt-Ergo,2.5.4_WP.oracle

   1 <check_ce:categorization>Categorizations of models:
   2 - Checked model 0: INCOMPLETE
   3   - Concrete RAC: INCOMPLETE (terminated because Precondition of `load_val` cannot be evaluated)
   4   - Abstract RAC: INCOMPLETE (terminated because Precondition of `load_val` cannot be evaluated)
   5 - Selected model 1: INCOMPLETE
   6   - Concrete RAC: INCOMPLETE (terminated because Precondition of `load_val` cannot be evaluated)
   7   - Abstract RAC: INCOMPLETE (terminated because Precondition of `load_val` cannot be evaluated)
   8 File "bench/check-ce/map_of_algebraic.mlw", line 34, characters 4-16:
   9 Sub-goal Precondition of goal not_valid'vc.
  10 Prover result is: Step limit exceeded (13 steps).
  11 The following counterexample model could not be verified
  12   (both RAC terminated because Precondition of `load_val` cannot be evaluated):
  13 File bv.mlw:
  14   Line 361:
  15     size_bv : t = {t'int => 32}
  16 File map_of_algebraic.mlw:
  17   Line 33:
  18     m :  = {block_size = "undefined"; mem_access_address = "undefined"}
  19     m :  = {block_size = "undefined"; mem_access_address = "undefined"}
  20     x :  = {base_addr = 0; offset = {t'int => 32}}
  21     x : loc = {base_addr = 0; offset = {t'int => 32}}
  22