int main(){
  int k=1;
  $state s=$get_state();

  k=2;
  $assert(k==2 && $value_at(s, -1, k)==1);
}