// Description: A simple module with 1 variable, which is an array of bitvectors. It also declares an enum type, and an uninterpreted function with a bitvector input and an enum return type. The property checks that we can call the function with an element of the array as the function argument and the output will be equal to one of the elements of the enum. Use bounded model checking to check the property.

module main {
  type op_t = enum { add, sub, load, store };
  var somearray : [bv8]bv8;
  function word2op(w : bv8) : op_t;

  init {}
  next {}

  property P3 : word2op(somearray[0bv8]) == add;
  control {
    x = unroll (1);
    check;
    print_results;
  }
}
