#include <stdlib.h>
#include <list>
#include <iostream>
#include <fstream>
#include <string>

using namespace std;

void clean(ifstream &in, ofstream &out){
  string line, *s, *vars;
  char *val;
  unsigned i=0, j=0, c=0;
  
  getline(in, line);
  vars= new string[line.length()];
  val= new char[line.length()];

  while (i < line.length()){
    s=new(string);
    while((i < line.length()) && (line[i]!='=')){
      *s+=line[i++];
    }      
    vars[c]+=*s;
    i++; // skip =
    val[c++]=line[i++];
    i++; //skip whitespace
    delete(s);
  };

  out << line << endl <<endl;
  
  while(! in.eof() ){
    getline(in, line);
    if (!(line.substr(0,12).compare("Typechecking")))
	break;
    i=0;j=0;
    while (i < line.length()){
      s=new(string);
      while((i < line.length()) && (line[i]!='=')){
	*s+=line[i++];
      }
      while (vars[j]!=*s) j++;
      i++; // skip =
      if (val[j]!=line[i]){
	out << *s<<"="<<line[i]<<" ";
	val[j]=line[i];
      }
      i++;
      i++; //skip whitespace
      delete(s);
    };
    out <<endl <<endl;
  };
}


void examine(char *fnIn, char *fnOut){
  ifstream in;
  ofstream out;
  string line;

  in.open(fnIn);
  if (! in.is_open()){
    cerr << "Error opening file" <<endl;
    exit(EXIT_FAILURE);
  };

  out.open(fnOut);
  if (! out.is_open()){
    cerr << "Error opening file" <<endl;
    exit(EXIT_FAILURE);
  };

  while(!in.eof()){
    getline(in, line);
    if ((line.length() > 9) && !(line.substr(0,9).compare("Invariant"))){
      out<<line <<endl;
      if(line.substr(line.length()-6, line.length()).compare("passed")){
	getline(in, line);
	out << line <<endl;
	getline(in, line);
	out << line <<endl;
	clean(in, out);
      }
    }
  }
  in.close();
  out.close();
}


int main(int argc, char **argv){
  if(argc!=3)
    cerr <<"Usage : ./a.out <input file> <output file>"<<endl;
  else{
    examine(argv[1],argv[2]);
  }
  return EXIT_SUCCESS;
}