Soundness bug: early materialisation of products produces incorrect results

[amandasystems]

Soundness bug: early materialisation of products produces incorrect results

[amandasystems]

This appears to be a minimal failing example input, reduced from parikh-plus/peterc-pyex-doc-cav17-td/experiments/8-600-1-7200/packages/httplib2/httplib2-www-authenticate/7493b346c2ff22b2865c8daa48dddec22d6b07ae7119451ebd26b3e8.smt2/parikh-constraints-1.par

synchronised {
automaton value_0 {
  init s0;
  s0 -> s1 [32, 32];
  s0 -> s0 [33, 65535];
  s1 -> s1 [0, 65535];
  accepting s1;
};
automaton value_8 {
  init s0;
  s0 -> s1 [85, 65535];
  s1 -> s2 [84, 84];
  // Critical: removing either of these makes it SAT:
  s2 -> s2 [0, 64]; 
  s2 -> s2 [0, 65535]; 
  accepting s2;
};
automaton value_9 {
  init s0;
  s0 -> s1 [0, 65535];
  s1 -> s1 [0, 65535];
  accepting s0, s1;
};
};

[amandasystems]

Original inputs:

parikh-plus/peterc-pyex-doc-cav17-td/experiments/8-600-1-7200/packages/httplib2/httplib2-www-authenticate/7493b346c2ff22b2865c8daa48dddec22d6b07ae7119451ebd26b3e8.smt2/parikh-constraints-1.par
parikh-plus/peterc-pyex-doc-cav17-z3/experiments/8-600-1-7200/packages/httplib2/httplib2-entry-disposition/55f625b8aea4a97735132d7e678895146ef735a2fee878846314337d.smt2/parikh-constraints-1.par
peterc-pyex-doc-cav17-td/experiments/8-600-1-7200/packages/httplib2/httplib2-entry-disposition/55f625b8aea4a97735132d7e678895146ef735a2fee878846314337d.smt2/parikh-constraints-1.par
parikh-plus/peterc-pyex-doc-cav17-zz/experiments/8-600-1-7200/packages/httplib2/httplib2-www-authenticate/7493b346c2ff22b2865c8daa48dddec22d6b07ae7119451ebd26b3e8.smt2/parikh-constraints-1.par
parikh-plus/peterc-pyex-doc-cav17-z3/experiments/8-600-1-7200/packages/httplib2/httplib2-www-authenticate/7493b346c2ff22b2865c8daa48dddec22d6b07ae7119451ebd26b3e8.smt2/parikh-constraints-1.par