153c153,154
< 
---
> vec<Lit> assumptions; // SW: Vector for storing assumptions
> // SW: Function modified to read files in the iCNF format
155c156
< static void parse_DIMACS_main(B& in, Solver& S) {
---
> static bool parse_DIMACS_main(B& in, Solver& S) {
159,170c160,170
<         if (*in == EOF)
<             break;
<         else if (*in == 'p'){
<             if (match(in, "p cnf")){
<                 int vars    = parseInt(in);
<                 int clauses = parseInt(in);
<                 reportf("|  Number of variables:  %-12d                                         |\n", vars);
<                 reportf("|  Number of clauses:    %-12d                                         |\n", clauses);
<             }else{
<                 reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
<             }
<         } else if (*in == 'c' || *in == 'p')
---
> 
>         if (*in == EOF) break;
>         else if (*in == 'p' && !match(in, "p inccnf") )
>             reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3);            
> 	else if (*in == 'a') {
> 	  ++in;
> 	  skipWhitespace(in);
> 	  readClause(in, S, assumptions); // SW: Not reading a "clause" here, but a sequence of literals anyway
> 	  return true;
> 	}
>         else if (*in == 'c' || *in == 'p')
172,174c172,174
<         else
<             readClause(in, S, lits),
<             S.addClause(lits);
---
>         else{
>             readClause(in, S, lits);
>             S.addClause(lits); }
175a176,177
> 
>     return false;
180,182c182,184
< static void parse_DIMACS(gzFile input_stream, Solver& S) {
<     StreamBuffer in(input_stream);
<     parse_DIMACS_main(in, S); }
---
> static bool parse_DIMACS(gzFile input_stream, Solver& S) {
>     static StreamBuffer in(input_stream);
>     return parse_DIMACS_main(in, S); }
219a222,223
>     reportf("  -stopatsat     = Stop once the first satisfiable\n");
>     reportf("                   result is found.\n");
237,238c241,242
<     S.verbosity = 1;
< 
---
>     S.verbosity = 0;
>     bool stopAtSat = false;
274c278,279
< 
---
>         }else if (strcmp(argv[i], "-stopatsat") == 0) {
>             stopAtSat = true;	 
289c294,296
<     reportf("This is MiniSat 2.0 beta\n");
---
>     reportf("This is MiniSat 2.0 beta - modified to handle the iCNF file format\n");
>     reportf("\nModifications (c) 2009 Siert Wieringa\n");
>     reportf("For information about the iCNF file format visit:\nhttp://www.tcs.hut.fi/~swiering/icnf\n\n");
295d301
<     double cpu_time = cpuTime();
308,312d313
<     reportf("============================[ Problem Statistics ]=============================\n");
<     reportf("|                                                                             |\n");
< 
<     parse_DIMACS(in, S);
<     gzclose(in);
315,323c316,331
<     double parse_time = cpuTime() - cpu_time;
<     reportf("|  Parsing time:         %-12.2f s                                       |\n", parse_time);
< 
<     if (!S.simplify()){
<         reportf("Solved by unit propagation\n");
<         if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
<         printf("UNSATISFIABLE\n");
<         exit(20);
<     }
---
>     bool ret = false;
>     int  assline=0;
>     while( parse_DIMACS( in, S ) && (!stopAtSat || !ret) ) {
>       reportf("%d.\t", ++assline );
> 
>       if (!S.simplify()){
> 	reportf("UNSATISFIABLE (Solved by unit propagation)\n");
>         ret = false;
>       }
>       else {
> 	ret = S.solve( assumptions );
> 
> 	reportf(ret ? "SATISFIABLE  " : "UNSATISFIABLE");
> 	reportf(" (CPU time usage so far %g s)\n", cpuTime() );
> 	fflush(stdout);
>       }
325,329c333
<     bool ret = S.solve();
<     printStats(S);
<     reportf("\n");
<     printf(ret ? "SATISFIABLE\n" : "UNSATISFIABLE\n");
<     if (res != NULL){
---
>       if (res != NULL){
331,335c335,339
<             fprintf(res, "SAT\n");
<             for (int i = 0; i < S.nVars(); i++)
<                 if (S.model[i] != l_Undef)
<                     fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
<             fprintf(res, " 0\n");
---
> 	  fprintf(res, "SAT\n");
> 	  for (int i = 0; i < S.nVars(); i++)
> 	    if (S.model[i] != l_Undef)
> 	      fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
> 	  fprintf(res, " 0\n");
337,339c341,345
<             fprintf(res, "UNSAT\n");
<         fclose(res);
<     }
---
> 	  fprintf(res, "UNSAT\n");
>       }
>     }   
>     gzclose(in);
>     if ( res != NULL ) fclose(res);