Checking of STG normalcy has an error

Normalcy checking returns "property" satisfied for the attached example, even though there is a violation. This is due to incorrect parsing of the MPSat output.

Normalcy checking can have 3 types of outputs for the case of violation that need to be considered. Victor could not find a benchmark for the complicated case. Below is the printing code - 1, 2 or 3 traces are printed depending on the circumstances.

void solution_Normalcy::print_results(ostream& os) const{
 switch(normalcy_violation_reason){
 case nvr_mixed_triggers:
  ASSERT(paths.size()==1);
  print_sequence(paths[0],os);
  if(&os==&cout){
   os<<"triggers: ";
   print_sequence(trig_set1,os);
   ASSERT(!signal_name.empty());
   os<<"\nNormalcy violation due to different triggers' signs for signal "<<signal_name<<'\n';
  }
  break;
 case nvr_contradictious_hypotheses:
  ASSERT(paths.size()==2);
  print_sequence(paths[0],os);
  if(&os==&cout){
   os<<"triggers: ";
   print_sequence(trig_set1,os);
  }
  print_sequence(paths[1],os);
  if(&os==&cout){
   os<<"triggers: ";
   print_sequence(trig_set2,os);
   os<<
    "\nNormalcy violation due to contradictious normalcy type hypotheses for signal "<<
    signal_name<<
    "\n(the paths show violations of p- and n-normalcy correspondingly)\n";
  }
  break;
 case nvr_CSC_conflict:
  print_sequence(paths[0],os);
  print_sequence(paths[1],os);
  os<<"\nNormalcy violation due to a CSC conflict for signal "<<signal_name<<'\n';
  break;
 case nvr_other:
  print_sequence(paths[0],os);
  os<<"triggers: ";
  print_sequence(trig_set1,os);
  print_sequence(paths[1],cout);
  print_sequence(paths[2],cout);
  ASSERT(n_type!=0);
  cout<<
   "\nNormalcy violation for signal "<<signal_name<<':'<<
   '\n'<<(n_type==STG_TS_PLUS ? 'p' : 'n')<<"-normalcy is violated according to the first path"<<
   '\n'<<(n_type==STG_TS_PLUS ? 'n' : 'p')<<"-normalcy is violated according to the other two paths\n";
  break;
 case nvr_no_violation:
 default:
  ASSERT0;
 }
}

Currently normalcy violation is correctly checked for a single trace only (case nvr_mixed_triggers).