Some instances sometimes produce a Princess crash: Proof Certificate Missing

[amandasystems]

Example instance:

counter int R0, R1, R2, R3, R4, R5;
synchronised {  // Automata constraining uri
automaton uri_0 {
  init s0;
  s0 -> s1 [109, 109];
  s1 -> s2 [111, 111];
  s2 -> s3 [110, 110];
  s3 -> s4 [103, 103];
  s4 -> s5 [111, 111];
  s5 -> s6 [100, 100];
  s6 -> s7 [98, 98];
  s7 -> s8 [58, 58];
  s8 -> s9 [47, 47];
  s9 -> s10 [47, 47];
  s10 -> s10 [0, 65535];
  accepting s10;
};
automaton uri_1 {
  init s0;
  s0 -> s0 [0, 65535] { R1 += 1 };
  accepting s0;
};
automaton uri_2 {
  init s0;
  s0 -> s1 [0, 36] { R3 += 1 };
  s0 -> s0 [0, 65535] { R2 += 1, R3 += 1 };
  s0 -> s1 [38, 42] { R3 += 1 };
  s0 -> s2 [44, 44] { R3 += 1 };
  s0 -> s1 [45, 45] { R3 += 1 };
  s0 -> s3 [46, 46] { R3 += 1 };
  s0 -> s1 [48, 62] { R3 += 1 };
  s0 -> s1 [65, 65535] { R3 += 1 };
  s1 -> s1 [0, 36] { R3 += 1 };
  s1 -> s1 [38, 42] { R3 += 1 };
  s1 -> s2 [44, 44] { R3 += 1 };
  s1 -> s1 [45, 45] { R3 += 1 };
  s1 -> s3 [46, 46] { R3 += 1 };
  s1 -> s1 [48, 62] { R3 += 1 };
  s1 -> s1 [65, 65535] { R3 += 1 };
  s2 -> s2 [0, 36] { R3 += 1 };
  s2 -> s2 [38, 42] { R3 += 1 };
  s2 -> s2 [44, 45] { R3 += 1 };
  s2 -> s9 [46, 46] { R3 += 1 };
  s2 -> s2 [48, 62] { R3 += 1 };
  s2 -> s2 [65, 65535] { R3 += 1 };
  s3 -> s1 [0, 36] { R3 += 1 };
  s3 -> s1 [38, 42] { R3 += 1 };
  s3 -> s2 [44, 44] { R3 += 1 };
  s3 -> s1 [45, 45] { R3 += 1 };
  s3 -> s3 [46, 46] { R3 += 1 };
  s3 -> s1 [48, 62] { R3 += 1 };
  s3 -> s1 [65, 114] { R3 += 1 };
  s3 -> s4 [115, 115] { R3 += 1 };
  s3 -> s1 [116, 65535] { R3 += 1 };
  s4 -> s1 [0, 36] { R3 += 1 };
  s4 -> s1 [38, 42] { R3 += 1 };
  s4 -> s2 [44, 44] { R3 += 1 };
  s4 -> s1 [45, 45] { R3 += 1 };
  s4 -> s3 [46, 46] { R3 += 1 };
  s4 -> s1 [48, 62] { R3 += 1 };
  s4 -> s1 [65, 110] { R3 += 1 };
  s4 -> s5 [111, 111] { R3 += 1 };
  s4 -> s1 [112, 65535] { R3 += 1 };
  s5 -> s1 [0, 36] { R3 += 1 };
  s5 -> s1 [38, 42] { R3 += 1 };
  s5 -> s2 [44, 44] { R3 += 1 };
  s5 -> s1 [45, 45] { R3 += 1 };
  s5 -> s3 [46, 46] { R3 += 1 };
  s5 -> s1 [48, 62] { R3 += 1 };
  s5 -> s1 [65, 98] { R3 += 1 };
  s5 -> s6 [99, 99] { R3 += 1 };
  s5 -> s1 [100, 65535] { R3 += 1 };
  s6 -> s1 [0, 36] { R3 += 1 };
  s6 -> s1 [38, 42] { R3 += 1 };
  s6 -> s2 [44, 44] { R3 += 1 };
  s6 -> s1 [45, 45] { R3 += 1 };
  s6 -> s3 [46, 46] { R3 += 1 };
  s6 -> s1 [48, 62] { R3 += 1 };
  s6 -> s1 [65, 106] { R3 += 1 };
  s6 -> s7 [107, 107] { R3 += 1 };
  s6 -> s1 [108, 65535] { R3 += 1 };
  s7 -> s7 [0, 36] { R3 += 1 };
  s7 -> s7 [38, 42] { R3 += 1 };
  s7 -> s8 [44, 44] { R3 += 1 };
  s7 -> s7 [45, 46] { R3 += 1 };
  s7 -> s7 [48, 62] { R3 += 1 };
  s7 -> s7 [65, 65535] { R3 += 1 };
  s8 -> s8 [0, 36] { R3 += 1 };
  s8 -> s8 [0, 65535];
  s8 -> s8 [38, 42] { R3 += 1 };
  s8 -> s8 [44, 46] { R3 += 1 };
  s8 -> s8 [48, 62] { R3 += 1 };
  s8 -> s8 [65, 65535] { R3 += 1 };
  s9 -> s2 [0, 36] { R3 += 1 };
  s9 -> s2 [38, 42] { R3 += 1 };
  s9 -> s2 [44, 45] { R3 += 1 };
  s9 -> s9 [46, 46] { R3 += 1 };
  s9 -> s2 [48, 62] { R3 += 1 };
  s9 -> s2 [65, 114] { R3 += 1 };
  s9 -> s10 [115, 115] { R3 += 1 };
  s9 -> s2 [116, 65535] { R3 += 1 };
  s10 -> s2 [0, 36] { R3 += 1 };
  s10 -> s2 [38, 42] { R3 += 1 };
  s10 -> s2 [44, 45] { R3 += 1 };
  s10 -> s9 [46, 46] { R3 += 1 };
  s10 -> s2 [48, 62] { R3 += 1 };
  s10 -> s2 [65, 110] { R3 += 1 };
  s10 -> s11 [111, 111] { R3 += 1 };
  s10 -> s2 [112, 65535] { R3 += 1 };
  s11 -> s2 [0, 36] { R3 += 1 };
  s11 -> s2 [38, 42] { R3 += 1 };
  s11 -> s2 [44, 45] { R3 += 1 };
  s11 -> s9 [46, 46] { R3 += 1 };
  s11 -> s2 [48, 62] { R3 += 1 };
  s11 -> s2 [65, 98] { R3 += 1 };
  s11 -> s12 [99, 99] { R3 += 1 };
  s11 -> s2 [100, 65535] { R3 += 1 };
  s12 -> s2 [0, 36] { R3 += 1 };
  s12 -> s2 [38, 42] { R3 += 1 };
  s12 -> s2 [44, 45] { R3 += 1 };
  s12 -> s9 [46, 46] { R3 += 1 };
  s12 -> s2 [48, 62] { R3 += 1 };
  s12 -> s2 [65, 106] { R3 += 1 };
  s12 -> s8 [107, 107] { R3 += 1 };
  s12 -> s2 [108, 65535] { R3 += 1 };
  accepting s8;
};
automaton uri_3 {
  init s0;
  s0 -> s0 [0, 65535] { R4 += 1, R5 += 1 };
  s0 -> s1 [0, 65535] { R5 += 1, R0 += 1 };
  s1 -> s2 [0, 65535];
  s1 -> s1 [0, 65535] { R5 += 1, R0 += 1 };
  s2 -> s2 [0, 65535];
  accepting s0, s1, s2;
};
};
constraint R1 = R5 && R2 = 10 && R3 = R5 && R4 = 10 && R0 != 0 && 9 < R5;

Note that the issue is nondeterministic: it is sometimes triggered, sometimes not.

[amandasystems]

My best guess is that this is a race condition in Princess.

[amandasystems]

The patch uuverifiers/princess#4 seems to address this problem