diff --git a/regression/ebmc/BDD2/main.sv b/regression/ebmc/BDD2/main.sv
index ddd1cf493..f9a628f74 100644
--- a/regression/ebmc/BDD2/main.sv
+++ b/regression/ebmc/BDD2/main.sv
@@ -7,7 +7,7 @@ module main(input clk, input [31:0] a);
       counter=counter+a;
 
   initial counter=0;
-  
+
   my_prop1: assert property (counter<199); // should pass
   my_prop2: assert property (counter<198); // should fail
 
diff --git a/regression/ebmc/ic3/exmp1/pdtvispeterson.sv b/regression/ebmc/ic3_1/pdtvispeterson.sv
similarity index 100%
rename from regression/ebmc/ic3/exmp1/pdtvispeterson.sv
rename to regression/ebmc/ic3_1/pdtvispeterson.sv
diff --git a/regression/ebmc/ic3/exmp1/test.desc b/regression/ebmc/ic3_1/test.desc
similarity index 100%
rename from regression/ebmc/ic3/exmp1/test.desc
rename to regression/ebmc/ic3_1/test.desc
diff --git a/regression/ebmc/ic3/non_inductive1/non_inductive.sv b/regression/ebmc/ic3_10/non_inductive.sv
similarity index 100%
rename from regression/ebmc/ic3/non_inductive1/non_inductive.sv
rename to regression/ebmc/ic3_10/non_inductive.sv
diff --git a/regression/ebmc/ic3/non_inductive1/test.desc b/regression/ebmc/ic3_10/test.desc
similarity index 100%
rename from regression/ebmc/ic3/non_inductive1/test.desc
rename to regression/ebmc/ic3_10/test.desc
diff --git a/regression/ebmc/ic3/exmp2/bobcount.sv b/regression/ebmc/ic3_2/bobcount.sv
similarity index 100%
rename from regression/ebmc/ic3/exmp2/bobcount.sv
rename to regression/ebmc/ic3_2/bobcount.sv
diff --git a/regression/ebmc/ic3/exmp2/test.desc b/regression/ebmc/ic3_2/test.desc
similarity index 100%
rename from regression/ebmc/ic3/exmp2/test.desc
rename to regression/ebmc/ic3_2/test.desc
diff --git a/regression/ebmc/ic3/exmp3/test.desc b/regression/ebmc/ic3_3/test.desc
similarity index 100%
rename from regression/ebmc/ic3/exmp3/test.desc
rename to regression/ebmc/ic3_3/test.desc
diff --git a/regression/ebmc/ic3/exmp3/viseisenberg.sv b/regression/ebmc/ic3_3/viseisenberg.sv
similarity index 100%
rename from regression/ebmc/ic3/exmp3/viseisenberg.sv
rename to regression/ebmc/ic3_3/viseisenberg.sv
diff --git a/regression/ebmc/ic3/exmp4/test.desc b/regression/ebmc/ic3_4/test.desc
similarity index 100%
rename from regression/ebmc/ic3/exmp4/test.desc
rename to regression/ebmc/ic3_4/test.desc
diff --git a/regression/ebmc/ic3/exmp4/visbakery.sv b/regression/ebmc/ic3_4/visbakery.sv
similarity index 100%
rename from regression/ebmc/ic3/exmp4/visbakery.sv
rename to regression/ebmc/ic3_4/visbakery.sv
diff --git a/regression/ebmc/ic3/exmp5/ringp0.sv b/regression/ebmc/ic3_5/ringp0.sv
similarity index 100%
rename from regression/ebmc/ic3/exmp5/ringp0.sv
rename to regression/ebmc/ic3_5/ringp0.sv
diff --git a/regression/ebmc/ic3/exmp5/test.desc b/regression/ebmc/ic3_5/test.desc
similarity index 100%
rename from regression/ebmc/ic3/exmp5/test.desc
rename to regression/ebmc/ic3_5/test.desc
diff --git a/regression/ebmc/ic3/exmp6/eijks208o.sv b/regression/ebmc/ic3_6/eijks208o.sv
similarity index 100%
rename from regression/ebmc/ic3/exmp6/eijks208o.sv
rename to regression/ebmc/ic3_6/eijks208o.sv
diff --git a/regression/ebmc/ic3/exmp6/test.desc b/regression/ebmc/ic3_6/test.desc
similarity index 100%
rename from regression/ebmc/ic3/exmp6/test.desc
rename to regression/ebmc/ic3_6/test.desc
diff --git a/regression/ebmc/ic3/exmp7/bobmiterbm1multi.sv b/regression/ebmc/ic3_7/bobmiterbm1multi.sv
similarity index 100%
rename from regression/ebmc/ic3/exmp7/bobmiterbm1multi.sv
rename to regression/ebmc/ic3_7/bobmiterbm1multi.sv
diff --git a/regression/ebmc/ic3/exmp7/test.desc b/regression/ebmc/ic3_7/test.desc
similarity index 100%
rename from regression/ebmc/ic3/exmp7/test.desc
rename to regression/ebmc/ic3_7/test.desc
diff --git a/regression/ebmc/ic3/exmp8/bobmiterbm1multi.sv b/regression/ebmc/ic3_8/bobmiterbm1multi.sv
similarity index 100%
rename from regression/ebmc/ic3/exmp8/bobmiterbm1multi.sv
rename to regression/ebmc/ic3_8/bobmiterbm1multi.sv
diff --git a/regression/ebmc/ic3/exmp8/test.desc b/regression/ebmc/ic3_8/test.desc
similarity index 100%
rename from regression/ebmc/ic3/exmp8/test.desc
rename to regression/ebmc/ic3_8/test.desc
diff --git a/regression/ebmc/ic3/exmp9/sm98a7multi.sv b/regression/ebmc/ic3_9/sm98a7multi.sv
similarity index 100%
rename from regression/ebmc/ic3/exmp9/sm98a7multi.sv
rename to regression/ebmc/ic3_9/sm98a7multi.sv
diff --git a/regression/ebmc/ic3/exmp9/sm98a7multi.sv.cnstr b/regression/ebmc/ic3_9/sm98a7multi.sv.cnstr
similarity index 100%
rename from regression/ebmc/ic3/exmp9/sm98a7multi.sv.cnstr
rename to regression/ebmc/ic3_9/sm98a7multi.sv.cnstr
diff --git a/regression/ebmc/ic3/exmp9/test.desc b/regression/ebmc/ic3_9/test.desc
similarity index 100%
rename from regression/ebmc/ic3/exmp9/test.desc
rename to regression/ebmc/ic3_9/test.desc
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index eb81aeb26..acb918a6b 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -257,6 +257,7 @@ void ebmc_parse_optionst::help()
     " --property <id>                   check the property with given ID\n"
     " -I path                           set include path\n"
     " --reset <expr>                    set up module reset\n"
+    " --verbosity <nr>                  set verbosity level (default: 6)\n"
     "\n"
     "Methods:\n"
     " --k-induction                     do k-induction with k=bound\n"
diff --git a/src/ic3/Makefile b/src/ic3/Makefile
index 4e637cc5f..f08083b41 100644
--- a/src/ic3/Makefile
+++ b/src/ic3/Makefile
@@ -23,7 +23,7 @@ INC_DIR = -I . -I build_prob -I seq_circ -I $(MINISAT_INC) -I $(CBMC)/src -I ../
 OBJ_DIR = .
 
 BUILD_PROB =   $(OBJ_DIR)/g3en_cnf.o  $(OBJ_DIR)/g0en_cnf.o $(OBJ_DIR)/g1en_cnf.o \
-               $(OBJ_DIR)/g2en_cnf.o $(OBJ_DIR)/assign_indexes.o $(OBJ_DIR)/build_arrays.o
+               $(OBJ_DIR)/g2en_cnf.o $(OBJ_DIR)/assign_indices.o $(OBJ_DIR)/build_arrays.o
 
 SEQ_CIRC = $(OBJ_DIR)/p1rint_blif.o $(OBJ_DIR)/p2rint_blif.o $(OBJ_DIR)/finish_gate.o \
            $(OBJ_DIR)/a2dd_gate.o  $(OBJ_DIR)/a3dd_gate.o  $(OBJ_DIR)/c2irc_util.o \
@@ -52,7 +52,7 @@ OBJ_ROOT = $(OBJ_DIR)/m5y_aiger_print.o \
 
 OBJ =      $(OBJ_ROOT) $(BUILD_PROB) $(SEQ_CIRC)
 
-H_FILES1 = m0ic3.hh dnf_io.hh  m2ethods.hh aux_types.hh i5nline.hh
+H_FILES1 = m0ic3.hh dnf_io.hh  m2ethods.hh aux_types.hh i5nline.hh s0hared_consts.hh
 H_FILES2 = ccircuit.hh ebmc_ic3_interface.hh more_fun_prot.hh
 $(OBJ_DIR)/%.o : %.cc  $(H_FILES1) $(H_FILES2)
 	$(CXX) -c $(CXXFLAGS)  $< -o $@
diff --git a/src/ic3/build_prob/assign_indexes.cc b/src/ic3/build_prob/assign_indices.cc
similarity index 94%
rename from src/ic3/build_prob/assign_indexes.cc
rename to src/ic3/build_prob/assign_indices.cc
index bffd83604..24718505b 100644
--- a/src/ic3/build_prob/assign_indexes.cc
+++ b/src/ic3/build_prob/assign_indices.cc
@@ -88,10 +88,10 @@ void find_latch(Circuit *N,Gate &G,int &latch_ind)
 
 /*=============================================
 
-  A S S I G N _ V A R _ I N D E X E S
+  A S S I G N _ V A R _ I N D I C E S 
 
   =============================================*/
-void CompInfo::assign_var_indexes()
+void CompInfo::assign_var_indices()
 {
 
   Gate_to_var.assign(N->Gate_list.size(),-1);
@@ -101,4 +101,4 @@ void CompInfo::assign_var_indexes()
   }
 
   num_circ_vars = curr_index-1;
-} /* end of function assign_var_indexes */
+} /* end of function assign_var_indices */
diff --git a/src/ic3/build_prob/g0en_cnf.cc b/src/ic3/build_prob/g0en_cnf.cc
index e6ad322b0..868daeeab 100755
--- a/src/ic3/build_prob/g0en_cnf.cc
+++ b/src/ic3/build_prob/g0en_cnf.cc
@@ -17,8 +17,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include "ccircuit.hh"
 #include "m0ic3.hh"
 
-int debug_flag=0;
-
 /*======================
 
   G E N _ C N F S
@@ -26,15 +24,12 @@ int debug_flag=0;
   =====================*/
 void  CompInfo::gen_cnfs(const char *fname,bool print_flag)
 {  
-  assign_var_indexes();
+  assign_var_indices();
  
-  char fname1[MAX_NAME];
 
   if (print_flag) {
     // print index file
-    strcpy(fname1,fname);
-    strcat(fname1,".ind");
-    print_var_indexes(fname1);
+    print_var_indices(std::string(fname)+".ind");
   }
 
   gen_initial_state_cubes();
@@ -108,11 +103,11 @@ void CompInfo::gen_out_fun(DNF &H,int shift,bool short_version)
 	add_truth_table_gate_cubes(H,gate_ind,shift);                 
 	break;
       case COMPLEX: 
-        printf("complex gates are not allowed\n");
-	exit(1);
+	M->error() << "complex gates are not allowed" << M->eom;
+	throw(ERROR1);
       default:   
-	printf("wrong gate type\n");
-	exit(1);
+	M->error() << "wrong gate type" << M->eom;
+	throw(ERROR1);
       }
   }
 
@@ -162,7 +157,7 @@ void  CompInfo::gen_initial_state_cubes()
 void  CompInfo::add_const_gate_cube(DNF &F,int gate_ind,int shift)
 {
 
-  // form indexes 
+  // form indices 
   Gate &G =  N->Gate_list[gate_ind];
  
   int var_ind = Gate_to_var[gate_ind] + shift;
@@ -171,7 +166,6 @@ void  CompInfo::add_const_gate_cube(DNF &F,int gate_ind,int shift)
   assert(G.F.size() < 2);
   if (G.F.size() == 1) C.push_back(var_ind + shift);
   else if (G.F.size() == 0) C.push_back(-(var_ind + shift));
-  if (debug_flag) std::cout << C << " 0\n";
 
   F.push_back(C);
 
@@ -186,34 +180,32 @@ void  CompInfo::add_const_gate_cube(DNF &F,int gate_ind,int shift)
 void CompInfo::add_buffer_gate_cubes(DNF &F,int gate_ind,int shift)
 {
 
-  // form indexes 
-  CUBE var_indexes;
+  // form indices 
+  CUBE var_indices;
   Gate &G = N->Gate_list[gate_ind];
 
 
   for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 =  G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
-    var_indexes.push_back(var_ind);
+    var_indices.push_back(var_ind);
   }
 
   // add the output var
-  var_indexes.push_back(Gate_to_var[gate_ind]);
+  var_indices.push_back(Gate_to_var[gate_ind]);
 
   CUBE C;
   // first cube
-  if (G.Polarity[0] == 0)  C.push_back(var_indexes[0]+shift);  
-  else C.push_back(-(var_indexes[0]+shift));
-  C.push_back(-(var_indexes[1]+shift)); 
+  if (G.Polarity[0] == 0)  C.push_back(var_indices[0]+shift);  
+  else C.push_back(-(var_indices[0]+shift));
+  C.push_back(-(var_indices[1]+shift)); 
   F.push_back(C);
-  if (debug_flag) std::cout << C << " 0\n";
 
   // second cube
   C.clear();
-  if (G.Polarity[0] == 0)  C.push_back(-(var_indexes[0]+shift));  
-  else C.push_back(var_indexes[0]+shift);
-  C.push_back(var_indexes[1]+shift);
+  if (G.Polarity[0] == 0)  C.push_back(-(var_indices[0]+shift));  
+  else C.push_back(var_indices[0]+shift);
+  C.push_back(var_indices[1]+shift);
   F.push_back(C);
-  if (debug_flag) std::cout << C << " 0\n";
 
 } /* end of function add_buffer_gate_cubes */
diff --git a/src/ic3/build_prob/g1en_cnf.cc b/src/ic3/build_prob/g1en_cnf.cc
index 6a6321556..b554c69da 100644
--- a/src/ic3/build_prob/g1en_cnf.cc
+++ b/src/ic3/build_prob/g1en_cnf.cc
@@ -43,30 +43,29 @@ void  CompInfo::add_or_gate_cubes(DNF &F,int gate_ind,int shift)
 {
 
 
-  // form indexes 
-  CUBE var_indexes;
+  // form indices 
+  CUBE var_indices;
   Gate &G =  N->Gate_list[gate_ind];
 
 
   for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 = G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
-    var_indexes.push_back(var_ind);
+    var_indices.push_back(var_ind);
   }
 
 
   // add the output var
-  var_indexes.push_back(Gate_to_var[gate_ind]);
+  var_indices.push_back(Gate_to_var[gate_ind]);
 
   //
   // generate the long clause
   //
   CUBE C;
   for (size_t i=0; i <  G.Fanin_list.size();i++)
-    if (G.Polarity[i] == 0)   C.push_back(var_indexes[i]+shift); 
-    else C.push_back(-(var_indexes[i]+shift)); 
-  C.push_back(-(var_indexes.back()+shift));
-  if (debug_flag) std::cout << C << " 0\n";
+    if (G.Polarity[i] == 0)   C.push_back(var_indices[i]+shift); 
+    else C.push_back(-(var_indices[i]+shift)); 
+  C.push_back(-(var_indices.back()+shift));
   if (!empty_cube(C))  F.push_back(C);
 
   //
@@ -75,10 +74,9 @@ void  CompInfo::add_or_gate_cubes(DNF &F,int gate_ind,int shift)
   //
   for (size_t i=0; i < G.Fanin_list.size();i++)
     {C.clear();
-      if (G.Polarity[i] == 0)   C.push_back(-(var_indexes[i]+shift)); 
-      else C.push_back(var_indexes[i]+shift); 
-      C.push_back(var_indexes.back()+shift);
-      if (debug_flag) std::cout << C << " 0\n";
+      if (G.Polarity[i] == 0)   C.push_back(-(var_indices[i]+shift)); 
+      else C.push_back(var_indices[i]+shift); 
+      C.push_back(var_indices.back()+shift);
       if (!empty_cube(C)) F.push_back(C);
     }
 
@@ -93,18 +91,18 @@ void  CompInfo::add_or_gate_cubes(DNF &F,int gate_ind,int shift)
 void CompInfo::add_and_gate_cubes(DNF &F,int gate_ind,int shift)
 {
 
-  // form indexes 
-  CUBE var_indexes;
+  // form indices 
+  CUBE var_indices;
   Gate &G =  N->Gate_list[gate_ind];
     
   for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 = G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
-    var_indexes.push_back(var_ind);
+    var_indices.push_back(var_ind);
   }
 
   // add the output var
-  var_indexes.push_back(Gate_to_var[gate_ind]);
+  var_indices.push_back(Gate_to_var[gate_ind]);
  
 
   //
@@ -112,10 +110,9 @@ void CompInfo::add_and_gate_cubes(DNF &F,int gate_ind,int shift)
   //
   CUBE C;
   for (size_t i=0; i < G.Fanin_list.size();i++)
-    if (G.Polarity[i] == 0)   C.push_back(-(var_indexes[i]+shift)); 
-    else C.push_back(var_indexes[i]+shift); 
-  C.push_back(var_indexes.back()+shift);
-  if (debug_flag) std::cout << C << " 0\n";
+    if (G.Polarity[i] == 0)   C.push_back(-(var_indices[i]+shift)); 
+    else C.push_back(var_indices[i]+shift); 
+  C.push_back(var_indices.back()+shift);
   if (!empty_cube(C))  F.push_back(C);
 
   //
@@ -124,10 +121,9 @@ void CompInfo::add_and_gate_cubes(DNF &F,int gate_ind,int shift)
   //
   for (size_t i=0; i < G.Fanin_list.size();i++) {
     C.clear();
-    if (G.Polarity[i] == 0)   C.push_back(var_indexes[i]+shift); 
-    else C.push_back(-(var_indexes[i]+shift)); 
-    C.push_back(-(var_indexes.back()+shift));
-    if (debug_flag) std::cout << C << " 0\n";
+    if (G.Polarity[i] == 0)   C.push_back(var_indices[i]+shift); 
+    else C.push_back(-(var_indices[i]+shift)); 
+    C.push_back(-(var_indices.back()+shift));
     if (!empty_cube(C)) F.push_back(C);
   }
 
@@ -141,19 +137,19 @@ void CompInfo::add_and_gate_cubes(DNF &F,int gate_ind,int shift)
 void  CompInfo::add_truth_table_gate_cubes(DNF &F,int gate_ind,int shift)
 {
 
-  // form indexes 
-  CUBE var_indexes;
+  // form indices 
+  CUBE var_indices;
   Gate &G =  N->Gate_list[gate_ind];
 
  
   for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 = G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
-    var_indexes.push_back(var_ind);
+    var_indices.push_back(var_ind);
   }
 
   // add the output var
-  var_indexes.push_back(Gate_to_var[gate_ind]);
+  var_indices.push_back(Gate_to_var[gate_ind]);
 
   CUBE TT(1 << G.ninputs);
   for (size_t i=0; i < TT.size(); i++)
@@ -170,10 +166,10 @@ void  CompInfo::add_truth_table_gate_cubes(DNF &F,int gate_ind,int shift)
     CUBE &C = D[i];
     CUBE C1;
     for (size_t j=0; j < C.size(); j++) {
-      C1.push_back(var_indexes[abs(C[j])-1]+shift);
+      C1.push_back(var_indices[abs(C[j])-1]+shift);
       if (C[j] > 0) C1[j] = -C1[j];
     }
-    C1.push_back(var_indexes.back()+shift);
+    C1.push_back(var_indices.back()+shift);
     if (!empty_cube(C1)) F.push_back(C1);
   }
 
@@ -184,10 +180,10 @@ void  CompInfo::add_truth_table_gate_cubes(DNF &F,int gate_ind,int shift)
       if (TT[i] == 1) continue;
       make_cube(i,G.ninputs,C);
       for (size_t j=0; j < C.size(); j++)
-	{C1.push_back(var_indexes[abs(C[j])-1]+shift);
+	{C1.push_back(var_indices[abs(C[j])-1]+shift);
 	  if (C[j] >  0) C1[j] = -C1[j];
 	}
-      C1.push_back(var_indexes.back()+shift);
+      C1.push_back(var_indices.back()+shift);
       C1.back() = -C1.back();
       if (!empty_cube(C1)) F.push_back(C1);
     }
diff --git a/src/ic3/build_prob/g2en_cnf.cc b/src/ic3/build_prob/g2en_cnf.cc
index fcc3f7c47..ea134c068 100644
--- a/src/ic3/build_prob/g2en_cnf.cc
+++ b/src/ic3/build_prob/g2en_cnf.cc
@@ -6,6 +6,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
 #include <iostream>
+#include <fstream>
 #include <set>
 #include <map>
 #include <algorithm>
@@ -24,8 +25,8 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
   ==================================*/
 void CompInfo::add_constrs() 
 {
-  printf("adding %d unit constraints\n",(int) (Constr_ilits.size() +
-					       Constr_nilits.size()));
+  M->status() << "adding " << Constr_ilits.size() + Constr_nilits.size()
+	      << " unit constraints" << M->eom;
   for (size_t i=0; i < Constr_ilits.size(); i++) {
     CLAUSE U;
     U.push_back(Constr_ilits[i]);
@@ -92,7 +93,7 @@ void CompInfo::gen_trans_rel(int shift)
 {
 
   for (size_t i=0; i < N->Gate_list.size();i++) {
-    int gate_ind = Ordering[i];
+    unsigned gate_ind = Ordering[i];
     Gate &G =  N->Gate_list[gate_ind];
     if (G.gate_type == INPUT) continue;
     if (G.gate_type == LATCH) continue;
@@ -116,27 +117,30 @@ void CompInfo::gen_trans_rel(int shift)
 	add_truth_table_gate_cubes(Tr,gate_ind,shift);         
 	break;
       case COMPLEX: 
-        printf("complex gates are not allowed\n");
-	exit(1);
+        M->error() << "complex gates are not allowed" << M->eom;
+	throw(ERROR1);
       default:   
-        printf("wrong gate type\n");
-	exit(1);
+        M->error() << "wrong gate type" << M->eom;
+	throw(ERROR1);
       }
   }
 
 } /* end of function gen_trans_rel */
 
+ 
+
 /*====================================
 
-   P R I N T _ V A R _ I N D E X E S
+  P R I N T _ V A R _ I N D I C E S
 
-====================================*/
-void CompInfo::print_var_indexes(char *fname)
+  ====================================*/
+void CompInfo::print_var_indices(const std::string &fname)
 {
 
-
-  FILE *fp = fopen(fname,"w");
-  assert(fp != NULL);
+  std::ofstream Out_str(fname.c_str(),std::ios::out);
+  if (!Out_str) {
+    M->error() << "cannot open file " << fname << M->eom;
+    throw(ERROR2);}
 
   DNF topol_levels;
   
@@ -144,35 +148,35 @@ void CompInfo::print_var_indexes(char *fname)
   CCUBE marked_vars;
   marked_vars.assign(2*N->Gate_list.size(),0);
 
-   // print var indexes in topological order
-   for (size_t i=0; i <= N->max_levels; i++)
-     {fprintf(fp,"--------------------------------------\n");
-       fprintf(fp,"topological level %zu\n",i);
-      CUBE &Gates = topol_levels[i];
-      for (size_t j=0; j < Gates.size(); j++)
-	{int gate_ind = Gates[j];
-	 Gate &G = N->get_gate(gate_ind);
-         switch (G.gate_type)
-	   {case LATCH: fprintf(fp,"L: ");
-	                break;
-	   case INPUT: fprintf(fp,"I: ");
-	                break;
-	   case GATE: fprintf(fp,"G: ");
-	               break;
-           default: assert(false);
-           }
-         fprint_name(fp,G.Gate_name);
-         fprintf(fp,"  %d\n",Gate_to_var[gate_ind]);
-	 int tmp = Gate_to_var[gate_ind];
-	 if (marked_vars[tmp] != 0)
-	   {fprintf(fp,"variable %d is shared!!\n",tmp);
-	   }
-         marked_vars[tmp] = 1;
+  // print var indices in topological order
+  for (size_t i=0; i <= N->max_levels; i++) {    
+    Out_str << "--------------------------------------\n";
+    Out_str << "topological level " << i << "\n";
+    CUBE &Gates = topol_levels[i];
+    for (size_t j=0; j < Gates.size(); j++) {
+      unsigned gate_ind = Gates[j];
+      Gate &G = N->get_gate(gate_ind);
+      switch (G.gate_type)
+	{case LATCH: Out_str << "L: ";
+	    break;
+	case INPUT: Out_str << "I: ";
+	  break;
+	case GATE: Out_str << "G: ";
+	  break;
+	default: assert(false);
 	}
-     }
-   fclose(fp);
+      fprint_name(Out_str,G.Gate_name);
+      Out_str << "  " << Gate_to_var[gate_ind] << "\n";
+      unsigned tmp = Gate_to_var[gate_ind];
+      if (marked_vars[tmp] != 0) 
+	Out_str << "variable " << tmp <<  " is shared!!\n";
+	  
+      marked_vars[tmp] = 1;
+    }
+  }
+  Out_str.close();
 
-}/* end of function print_var_indexes */
+}/* end of function print_var_indices */
 
 /*=========================================
 
@@ -194,7 +198,7 @@ void CompInfo::set_constr_flag()
   for (pnt = Constr_gates.begin(); pnt!=Constr_gates.end(); pnt++)  {
     CUBE Gates;
     CUBE Stack;
-    int gate_ind = pnt->first;
+    unsigned gate_ind = pnt->first;
     Gate &G = N->get_gate(gate_ind);
     if (G.gate_type == LATCH) continue;
     if (G.gate_type == INPUT) continue;
diff --git a/src/ic3/c0ex.cc b/src/ic3/c0ex.cc
index de94ba292..2539ad225 100644
--- a/src/ic3/c0ex.cc
+++ b/src/ic3/c0ex.cc
@@ -16,6 +16,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include "ccircuit.hh"
 #include "m0ic3.hh"
 
+
 /*==========================================
 
   F O R M _ I N P _ T R A C E
@@ -49,7 +50,7 @@ bool CompInfo::check_one_state_cex()
 
   int num_vars = std::max(num_ist_vars,num_prop_vars);
 
-  std::string Name = "Gen_sat";
+  std::string Name("Gen_sat");
   init_sat_solver(Gen_sat,num_vars,Name);
 
   // add formulas Ist
@@ -66,7 +67,7 @@ bool CompInfo::check_one_state_cex()
   bool sat_form = check_sat1(Gen_sat);
   bool ok = true;
   if (sat_form) {
-    printf("an initial state does not satisfy the property\n");
+    M->result() << "an initial state does not satisfy the property" << M->eom;
     form_one_state_cex(Gen_sat);
     max_num_tfs = 0;
     ok = false;
@@ -86,7 +87,7 @@ bool CompInfo::check_two_state_cex()
 {
 
 
-  std::string Name = "Gen_sat";
+  std::string Name("Gen_sat");
   init_sat_solver(Gen_sat,max_num_vars,Name);
 
   // add formulas Ist, Tr and Bad_states
diff --git a/src/ic3/c2tg.cc b/src/ic3/c2tg.cc
index db890f8d0..a00b0948f 100644
--- a/src/ic3/c2tg.cc
+++ b/src/ic3/c2tg.cc
@@ -29,13 +29,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
  =======================================*/
 bool CompInfo::exclude_ctg(CUBE &St,int curr_tf,int rec_depth)
 {
-
-  if (verbose > 2) {
-    printf("   exclude_ctg\n");
-    std::cout << "    St-> " << St << std::endl;
-    printf("curr_tf = %d, rec_depth = %d\n",curr_tf,rec_depth);}
-
-  
   
   CLAUSE C0;
   form_lngst_clause(C0,St);
diff --git a/src/ic3/c5tg.cc b/src/ic3/c5tg.cc
index 1db309f4b..f73428083 100644
--- a/src/ic3/c5tg.cc
+++ b/src/ic3/c5tg.cc
@@ -93,10 +93,10 @@ void CompInfo::lift_ctg_state(CUBE &Ctg_cube,CUBE &Ctg_st,CUBE &Inps,
   bool sat_form = check_sat2(Lgs_sat,Assmps);
   if (sat_form) {
     p();
-    printf("Ctg_st.size() = %d, Nst_cube.size() = %d\n",(int) Ctg_st.size(),
-          (int) Nst_cube.size());    
-    printf("tf_lind = %d\n",tf_lind);
-    exit(1);
+    M->error() << "Ctg_st.size() = " << Ctg_st.size() << ", Nst_cube.size() = " 
+	       << Nst_cube.size() << M->eom;
+    M->error() << "tf_lind = " << tf_lind << M->eom;
+    throw(ERROR1);
   }
     
   gen_state_cube(Ctg_cube,Ctg_st,Lgs_sat);
diff --git a/src/ic3/dnf_io.cc b/src/ic3/dnf_io.cc
index 9c3856528..857ab4454 100644
--- a/src/ic3/dnf_io.cc
+++ b/src/ic3/dnf_io.cc
@@ -8,18 +8,18 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 ******************************************************/
 #include <assert.h>
 #include <iostream>
+#include <fstream>
 #include <set>
 #include <queue>
 #include <algorithm>
 #include <map>
 #include <stdio.h>
 #include "dnf_io.hh"
-
+#include "s0hared_consts.hh"
 
 /*========================================
 
-
-  F I N D _ M A X _ V A R
+    F I N D _ M A X _ V A R
 
   returns the maximal (order) number
   of a variable occuring in cubes  of D
@@ -71,12 +71,11 @@ int find_max_var(DNF &D,bool_vector &marked_sat)
 
 
 
-/*============================================
-
+/*==========================
 
-  P R I N T _ S E T 
+    P R I N T _ S E T 
 
-  =============================================*/
+  ========================*/
 void print_set(SCUBE &s)
 
 {SCUBE::iterator i;
@@ -94,10 +93,10 @@ void print_set(SCUBE &s)
   ==========================*/
 void print_cube(CUBE &C) {
   for (size_t i=0; i < C.size(); i++) {
-    if (i > 0) printf(" ");
-    printf("%d",C[i]);
+    if (i > 0) std::cout << " ";
+    std::cout << C[i];
   }
-  printf(" 0\n");
+  std::cout << " 0\n";
 } /* end of function print_cube */
 
 
@@ -109,9 +108,9 @@ void print_cube(CUBE &C) {
 void print_cube(CCUBE &C)
 {
   for (size_t i=0; i < C.size(); i++)
-    printf("%d ",C[i]);
+    std::cout << C[i] << " ";
 
-  printf("\n");
+  std::cout << "\n";
 }/* end of function print_cube */
 
 /*===========================
@@ -119,12 +118,13 @@ void print_cube(CCUBE &C)
   P R I N T _ C U B E 
 
   ===========================*/
-void print_cube(FILE *fp,CCUBE &C)
+void print_cube(std::ofstream &Out_str,CCUBE &C)
 {
   for (size_t i=0; i < C.size(); i++)
-    fprintf(fp,"%d ",C[i]);
+    Out_str << C[i] << " ";
+
+  Out_str << "\n";
 
-  fprintf(fp,"\n");
 }/* end of function print_cube */
 
 /*===========================
@@ -132,18 +132,13 @@ void print_cube(FILE *fp,CCUBE &C)
   P R I N T _ C U B E 
 
   ===========================*/
-void print_cube(FILE *fp,CUBE &C)
+void print_cube(std::ofstream &Out_str,CUBE &C)
 {
   for (size_t i=0; i < C.size(); i++)
-    fprintf(fp,"%d ",C[i]);
+     Out_str << C[i] << " ";
 
 }/* end of function print_cube */
 
-
-
-
-
-
  
 /*==========================================
 
@@ -187,8 +182,8 @@ std::ostream &operator<<(std::ostream &os,CUBE const &v)
 std::ostream &operator<<(std::ostream &os,CCUBE const &v)
 {CCUBE:: const_iterator i;
   for (i=v.begin();i!= v.end();i++)
-    if (i == v.begin()) printf("%d",*i);
-    else printf("%d",*i);
+    std::cout << *i;
+  
   return(os);
 }
 
@@ -206,7 +201,7 @@ std::ostream &operator<<(std::ostream &os,CCUBE const &v)
 void print_dnf(DNF &D,CUBE &Cube_nums)
 
 {
-  printf("p cnf %d %d\n",find_max_var(D),(int) Cube_nums.size());
+  std::cout << "p cnf " << find_max_var(D) << " " << Cube_nums.size() << "\n";
   for (size_t i = 0; i < Cube_nums.size();i++)
     print_cube(D[Cube_nums[i]]);
 } /* end of function print_dnf */
@@ -229,19 +224,31 @@ void print_dnf1(DNF &D,CCUBE &Active_cubes)
     
 } /* end of function print_dnf1 */
 
+
+/*===========================
+
+  F P R I N T _ C U B E
+
+  ==========================*/
+void fprint_cube(std::ofstream &Out_str,CUBE &C) {
+  for (size_t i=0; i < C.size(); i++) {
+    if (i > 0) Out_str << " ";
+    Out_str << C[i];
+  }
+  Out_str << " 0\n";
+} /* end of function fprint_cube */
 /*==============================
 
-  P R I N T _ D N F
+   P R I N T _ D N F
 
-  prints D   to the file "fname" 
-  in the dimacs format
+  prints D  in the dimacs format
    
   ===============================*/
-void print_dnf(DNF &D,FILE *fp)
+void print_dnf(DNF &D,std::ofstream &Out_str)
 {
-  fprintf(fp,"p cnf %d %d\n",find_max_var(D),(int) D.size());
+  Out_str << "p cnf " << find_max_var(D) << " " << D.size() << "\n";
   for (size_t i = 0; i < D.size();i++)
-    fprint_cube(fp,D[i]);
+    fprint_cube(Out_str,D[i]);
  
 } /* end of function print_dnf */
 
@@ -254,17 +261,16 @@ void print_dnf(DNF &D,FILE *fp)
   in the dimacs format
    
   ==================================*/
-void print_dnf(DNF &D,char *fname)
-{ FILE *fp;
-
-  fp = fopen(fname,"w");
-  if (fp == NULL) {
-    std::cout << "cannot open file " << fname << std::endl;
-    exit(1);}
-     
+bool print_dnf(DNF &D,char *fname)
+{
+  
+  std::ofstream Out_str(fname,std::ios::out);
+  if (!Out_str) return(false);
    
-  print_dnf(D,fp);  
-  fclose(fp);
+     
+  print_dnf(D,Out_str);  
+  Out_str.close();
+  return(true);
 
 } /* end of function print_dnf */
 
@@ -273,36 +279,12 @@ void print_dnf(DNF &D,char *fname)
   P R I N T _ D N F
 
   ======================*/
-
-void print_dnf(DNF &D,const char *fname)
+bool print_dnf(DNF &D,const char *fname)
 {
-  print_dnf(D,(char *) fname);
+  bool success = print_dnf(D,(char *) fname);
+  return(success);
 } /* end of function print_dnf */
 
-/*=================================
-
-  P R I N T _ D N F
-
-  prints D   to the file "fname" 
-  in the dimacs format
-   
-  ==================================*/
-void print_dnf(DNF &D,int nvars,char *fname)
-
-{ 
-  FILE *fp;
-
-  fp = fopen(fname,"w");
-  if (fp == NULL) 
-    {std::cout << "cannot open file " << fname << std::endl;
-      exit(1);
-    }
-   
-  fprintf(fp,"p cnf %d %d\n",nvars,(int) D.size());
-  for (size_t i = 0; i < D.size();i++)
-    fprint_cube(fp,D[i]);
-  fclose(fp);
-} /* end of function print_dnf */
 
 /*=================================
 
@@ -314,7 +296,7 @@ void print_dnf(DNF &D,int nvars,char *fname)
   ==================================*/
 void print_dnf(DNF &D) {
 
-  printf("p cnf %d %d\n",find_max_var(D),(int) D.size());
+  std::cout << "p cnf " << find_max_var(D) << " " << D.size() << "\n";
   for (size_t i = 0; i < D.size();i++)
     print_cube(D[i]);
 } /* end of function print_dnf */
@@ -332,7 +314,7 @@ void print_dnf(DNF &D,int start,int finish) {
 
   // note that in the line below we compute find_max_var for
   //   the whole DNF formula
-  printf("p cnf %d %d\n",find_max_var(D),finish-start); 
+  std::cout << "p cnf " << find_max_var(D) << " " << finish-start << "\n";
   for (int i = start; i < finish;i++)
     print_cube(D[i]);
 } /* end of function print_dnf */
@@ -346,7 +328,7 @@ void print_dnf(DNF &D,int start,int finish) {
   ==================================*/
 void print_dnf(DNF &D,unsigned int threshold)
 {
-  printf("p cnf %d %d\n",find_max_var(D),(int) D.size());
+  std::cout << "p cnf " << find_max_var(D) << " " << D.size() << "\n";
   for (size_t i = 0; i < D.size();i++)
     if (D[i].size() <= threshold)
       print_cube(D[i]);
@@ -377,49 +359,13 @@ void print_dnf1(DNF &D) {
 void print_dnf2(DNF &D,int start_num)
 
 {
-  printf("p cnf %d %d\n",find_max_var(D),(int) D.size());
+  std::cout << "p cnf " << find_max_var(D) << " " << D.size() << "\n";
   for (size_t i = 0; i < D.size();i++) {
     std::cout << start_num+i << "/ ";
     print_cube(D[i]);
   }
 } /* end of function print_dnf2 */
 
-/*============================
-
-  P R I N T _ D N F 3
-
-  Prints numbers of cubes
-
-  ==========================*/
-void print_dnf3(DNF &D,char *fname,int start_num)
-
-{CUBE cube;
-
-  FILE *fp = fopen(fname,"w");
-  assert(fp != NULL);
-
-  fprintf(fp,"p cnf %d %d\n",find_max_var(D),(int) D.size());
-  for (size_t i = 0; i < D.size();i++)   {
-    fprintf(fp,"%zu/ ", start_num+i);
-    fprint_cube(fp,D[i]);
-  }
-  fclose(fp);
-} /* end of function print_dnf3 */
-
-
-
-/*===========================
-
-  F P R I N T _ C U B E
-
-  ==========================*/
-void fprint_cube(FILE *fp,CUBE &C) {
-  for (size_t i=0; i < C.size(); i++) {
-    if (i > 0) fprintf(fp," ");
-    fprintf(fp,"%d",C[i]);
-  }
-  fprintf(fp," 0\n");
-} /* end of function fprint_cube */
 
 
 /*=====================
@@ -434,33 +380,7 @@ void add_dnf(DNF &F1,DNF &F)
     F1.push_back(F[i]);
 } /* end of function add_dnf */
 
-/*=========================================================
-
-  P R I N T _ D N F
-
-  Print a subset of cubes of D  in the DIMACS format to 
-  the standard output. This subset consists of cubes
-  whose numbers are greater or equal   than start and 
-  smaller than finish
-  ======================================================*/
-void print_dnf(DNF &D,char *fname,int start,int finish)
-{
-  
-  FILE *fp;
 
-  fp = fopen(fname,"w");
-  if (fp == NULL) {
-    printf("cannot open file %s\n",fname);
-    exit(1);}
-     
-  // note that in the line below we compute find_max_var for
-  //   the whole DNF formula
-  fprintf(fp,"p cnf %d %d\n",find_max_var(D),finish-start); 
-
-  for (int i = start; i < finish;i++)
-    fprint_cube(fp,D[i]);
-   
-} /* end of function print_dnf */
 
 /*========================
 
@@ -476,31 +396,6 @@ std::ostream &operator<<(std::ostream &os,std::deque <int> const &v)
   return(os);
 }
 
-/*=================================
-
-  P R I N T _ D N F
-
-  prints D   to the file "fname" 
-  in the dimacs format
-   
-  ==================================*/
-void print_dnf(DNF &D,char *fname,int num_vars)
-
-{ FILE *fp;
-
-  fp = fopen(fname,"w");
-  if (fp == NULL) {
-    std::cout << "cannot open file " << fname << std::endl;
-    exit(1);
-  }
-   
-  fprintf(fp,"p cnf %d %d\n",num_vars,(int) D.size());
-  for (size_t i = 0; i < D.size();i++)
-    fprint_cube(fp,D[i]);
-
-  fclose(fp);
-} /* end of function print_dnf */
-
 
 /*================================
 
@@ -515,18 +410,7 @@ void print_srt_cube(CUBE &C) {
 
 } /* end of function print_srt_cube */
 
-/*================================
-
-  F P R I N T _ S R T _ C U B E
-
-  =================================*/
-void fprint_srt_cube(FILE *fp,CUBE &C) {
-
-  CUBE A = C;
-  sort(A.begin(),A.end());
-  fprint_cube(fp,A);
 
-} /* end of function fprint_srt_cube */
 
 /*================================
 
@@ -536,40 +420,25 @@ void fprint_srt_cube(FILE *fp,CUBE &C) {
 void print_srt_dnf(DNF &D) {
 
 
-  printf("p cnf %d %d\n",find_max_var(D),(int) D.size());
+  std::cout << "p cnf " << find_max_var(D) << " " << D.size() << "\n";
   for (size_t i=0; i < D.size(); i++)
     print_srt_cube(D[i]);
 
 } /* end of function print_srt_dnf */
 
-/*================================
-
-  F P R I N T _ S R T _ D N F
-
-  =================================*/
-void fprint_srt_dnf(DNF &D,char *fname) {
 
-  FILE *fp = fopen(fname,"w");
-  if (fp == NULL) {
-    printf("failed to open file %s\n",fname);
-    exit(1);
-  }
-
-  fprintf(fp,"p cnf %d %d\n",find_max_var(D),(int) D.size());
-  for (size_t i=0; i < D.size(); i++)
-    fprint_srt_cube(fp,D[i]);
-
-  fclose(fp);
-} /* end of function fprint_srt_dnf */
-
-
-/*================================
+/*=================================
 
-  F P R I N T _ S R T _ D N F
+  P R I N T _ D N F
 
-  =================================*/
-void fprint_srt_dnf(DNF &D,const char *fname) {
+  prints D   to the file "fname" 
+  in the dimacs format
+   
+  ==================================*/
+bool print_dnf(DNF &D,std::string &Name)
+{
 
-  fprint_srt_dnf(D,(char *) fname);
+  bool success = print_dnf(D,Name.c_str());
+  return(success);
 
-} /* end of function fprint_srt_dnf */
+} /* end of function print_dnf */
diff --git a/src/ic3/dnf_io.hh b/src/ic3/dnf_io.hh
index 9c3ddec4d..5018c38c4 100644
--- a/src/ic3/dnf_io.hh
+++ b/src/ic3/dnf_io.hh
@@ -18,9 +18,6 @@ typedef DNF CNF;
 typedef std::vector <float> FltCube;
 
 
-#define BUF_SIZE 1000
-#define MAX_NUM 20
-
 
 /*========================
 
@@ -44,29 +41,26 @@ void print_dnf(DNF &D,int start,int finish);
 void print_dnf1(DNF &D);
 void print_dnf1(DNF &D,CCUBE &Active_cubes);
 void print_dnf2(DNF &D,int start_num=0);
-void print_dnf3(DNF &D,char *fname,int start_num=0);
-void print_dnf(DNF &D,const char *fname);
+bool print_dnf(DNF &D,const char *fname);
 // print DNF D in the dimacs format the number of variables is 
 // computed by the value of the largest literal number
-void print_dnf(DNF &D,char *fname); 
-void print_dnf(DNF &D,FILE *fp); 
-void print_dnf(DNF &D,int nvars,char *fname);// print DNF D in the dimacs format 
+bool print_dnf(DNF &D,char *fname);
+bool print_dnf(DNF &D,std::string &Name);
+void print_dnf(DNF &D,std::ofstream &Out_str);
 void print_dnf(DNF &D,CUBE &cube_nums);
 void print_dnf(DNF &D,unsigned int threshold);
-void print_dnf(DNF &D,char *fname,int start,int finish);
-void print_dnf(DNF &D,char *fname,int num_vars);
 void print_set(SCUBE &S);
 int find_max_var(DNF &D);
 void print_cube(CUBE &C);
-void print_cube(FILE *fp,CCUBE &C);
-void print_cube(FILE *fp,CUBE &C);
+void print_cube(std::ofstream &Out_str,CCUBE &C);
+void print_cube(std::ofstream &Out_str,CUBE &C);
 void print_cube(CCUBE &C);
 void add_dnf(DNF &F1,DNF &F);
-void fprint_cube(FILE *fp,CUBE &C);
 void print_srt_cube(CUBE &C);
-void fprint_srt_cube(FILE *fp,CUBE &C);
 void print_srt_dnf(DNF &D);
-void fprint_srt_dnf(DNF &D,char *fname);
-void fprint_srt_dnf(DNF &D,const char *fname);
 
+//
+//  
+//
+void fprint_cube(std::ofstream &Out_str,CUBE &C);
 
diff --git a/src/ic3/e1xclude_state.cc b/src/ic3/e1xclude_state.cc
index 697746d60..1adcdd29e 100644
--- a/src/ic3/e1xclude_state.cc
+++ b/src/ic3/e1xclude_state.cc
@@ -23,12 +23,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
   ======================================*/
 void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0)
 {
-  if (verbose > 1)  {
-    printf("======\n");
-    printf("   exclude_state_cube\n");
-    std::cout << St0_cube << std::endl;
-  }
-
+ 
 
   assert(Pr_queue.empty());
   Obl_table.clear();
@@ -40,15 +35,10 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0)
   add_new_elem(St0_cube,Inps0,curr_tf,1,-1,ROOT_STATE);
   min_tf = curr_tf; 
   while (Pr_queue.size() > 0) {   
-    if (verbose > 1)  {
-      printf("Pr_queue.size() = %d\n",(int) Pr_queue.size());
-    }
 
     int curr_tf = Pr_queue.top().tf_ind;
     int tbl_ind = Pr_queue.top().tbl_ind;
     
-    if (verbose > 1)
-      printf("curr_tf = %d, tbl_ind = %d, min_tf = %d\n",curr_tf,tbl_ind, min_tf);
 
     CUBE St_cube  =  Obl_table[tbl_ind].St_cb;
     char st_descr = Obl_table[tbl_ind].st_descr;
@@ -81,11 +71,7 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0)
 
     if (found) { // inductive clause is found      
       Pr_queue.pop();
-      if (verbose > 1) 	{	 
-	printf("Inductive clause F[%d] is found ",(int) F.size());
-	std::cout  << C << std::endl;
-      }
-
+   
       if (succ_ind == -1) 
 	G.push_back(C);
             
@@ -126,8 +112,9 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0)
 
     if (state_found == 0) {
       p();
-      printf("st_ind = %d, curr_tf = %d\n",st_ind,curr_tf);
-      exit(100);
+      M->error() << "st_ind = " << st_ind << ", curr_tf = " << curr_tf 
+		 << M->eom;
+      throw(ERROR1);
     }
     
     add_new_elem(Erl_st_cube,Erl_inps,curr_tf-1,dist+1,tbl_ind,NEW_STATE);
@@ -197,12 +184,6 @@ bool CompInfo::find_prev_state_cube(CLAUSE &C,int curr_tf,CUBE &Prv_st_cube,
 
   SatSolver &Slvr = Time_frames[curr_tf].Slvr;
  
-
-  if (verbose > 1) {
-    printf("%*c",6,' ');
-    printf("find_prev_state_cube\n");
-    printf("curr_tf = %d\n",curr_tf);
-  }
  
   CUBE Nst_cube;
   conv_to_next_state(Nst_cube,St_cube);
@@ -218,12 +199,7 @@ bool CompInfo::find_prev_state_cube(CLAUSE &C,int curr_tf,CUBE &Prv_st_cube,
     CUBE St0;
     extr_cut_assgns1(St0,Pres_svars,Slvr);
     extr_cut_assgns1(Prev_inps,Inp_vars,Slvr);
-    lift_good_state(Prv_st_cube,St0,Prev_inps,Nst_cube);
-    if (verbose > 2) {
-      printf("%*c",6,' ');
-      printf("Prv. state cube is found: ");
-      std::cout << Prv_st_cube << std::endl;
-    }
+    lift_good_state(Prv_st_cube,St0,Prev_inps,Nst_cube);    
     return(true);
   }
 
diff --git a/src/ic3/e2xclude_state.cc b/src/ic3/e2xclude_state.cc
index ae2639a2a..820b14650 100644
--- a/src/ic3/e2xclude_state.cc
+++ b/src/ic3/e2xclude_state.cc
@@ -31,10 +31,6 @@ bool CompInfo::find_ind_subclause_cti(CLAUSE &C,SatSolver &Slvr,
                                       CLAUSE &C0,char st_descr)
 {
 
-  if (verbose > 2) {
-    printf("%*c",6,' ');
-    printf("find_ind_sub_clause_cti\n");
-  }
   C = C0;
 
 
@@ -148,10 +144,6 @@ bool CompInfo::corr_clause(CLAUSE &C)
 void CompInfo::adjust_clause1(CLAUSE &C,CUBE &St)
 {
 
-  if (verbose > 3) {
-    printf("%*c",9,' ');
-    printf("expand_clause\n");
-  }
   htable_lits.change_marker(); 
   htable_lits.started_using();
 
@@ -179,8 +171,8 @@ void CompInfo::adjust_clause1(CLAUSE &C,CUBE &St)
 
   if (shift == 0) {
     p();
-    print_bnd_sets1();
-    exit(1); }
+    print_bnd_sets1(messaget::M_ERROR);
+    throw(ERROR1); }
 
   C.resize(C.size()-shift);
   htable_lits.done_using();
diff --git a/src/ic3/e3xclude_state.cc b/src/ic3/e3xclude_state.cc
index 11c2b3237..daa1ed041 100644
--- a/src/ic3/e3xclude_state.cc
+++ b/src/ic3/e3xclude_state.cc
@@ -26,12 +26,6 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf,
                           char st_descr,int rec_depth)
 {
 
-  if (verbose > 1) {
-    printf("%*c",6,' ');
-    printf("incr_short\n");
-  }
-
-
   int impr_count = 0;
   C = C0;
   if (C.size() == 1) return;
@@ -122,7 +116,6 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf,
 void CompInfo::modif_loc_clause(CLAUSE &C,CUBE &St)
 {
 
-  if (verbose > 1) printf("correcting local clause\n");
   // find a variable where 'St' has the oposite
   // value of all initial states
 
diff --git a/src/ic3/e4xclude_state.cc b/src/ic3/e4xclude_state.cc
index ee84b0f1d..0c7d87e9a 100644
--- a/src/ic3/e4xclude_state.cc
+++ b/src/ic3/e4xclude_state.cc
@@ -40,8 +40,8 @@ int CompInfo::pick_lit_to_remove(CLAUSE &Curr,SCUBE &Tried,int curr_tf)
     lit = fxd_ord_lit(Curr,Tried);
     break;
   default:
-    printf("lit_pick_heur = %d\n",lit_pick_heur);
-    exit(100);
+    M->error() << "lit_pick_heur = " << lit_pick_heur << M->eom;
+    throw(ERROR1);
   }
 
   return(lit);
diff --git a/src/ic3/e5xclude_state.cc b/src/ic3/e5xclude_state.cc
index 875160118..42b55f614 100644
--- a/src/ic3/e5xclude_state.cc
+++ b/src/ic3/e5xclude_state.cc
@@ -36,10 +36,6 @@ bool CompInfo::adjust_clause2(CLAUSE &C,CUBE &St_cube,SCUBE &Failed_lits)
 
   if (St_cube.size() == 0) return(false);
 
-  if (verbose > 3) {
-    printf("%*c",9,' ');
-    printf("expand_clause\n");
-  }
   htable_lits.change_marker(); 
   htable_lits.started_using();
 
@@ -74,7 +70,7 @@ bool CompInfo::adjust_clause2(CLAUSE &C,CUBE &St_cube,SCUBE &Failed_lits)
 
   if (shift == 0) {
     p();
-    exit(1); }
+    throw(ERROR1); }
 
   C.resize(C.size()-shift);
   htable_lits.done_using();
@@ -110,9 +106,6 @@ bool CompInfo::find_ind_subclause_ctg(CLAUSE &C,int curr_tf,CLAUSE &C0,
 		       	char st_descr,int rec_depth,SCUBE &Failed_lits)
 {
 
-  if (verbose > 2) {
-    printf("find_ind_subclause_ctg\n");
-}
 
   SatSolver &Slvr = Time_frames[curr_tf].Slvr;
 
diff --git a/src/ic3/ebmc_ic3_interface.hh b/src/ic3/ebmc_ic3_interface.hh
index 11169996b..0addd9638 100644
--- a/src/ic3/ebmc_ic3_interface.hh
+++ b/src/ic3/ebmc_ic3_interface.hh
@@ -49,7 +49,6 @@ public:
   bool form_orig_name(CCUBE &Name,literalt &lit,bool subtract = false);
   void form_inv_names(CDNF &Pin_names,int lit);
   void form_invs();
-  void print_expr_id(exprt &E);
   bool banned_expr(exprt &expr);
   bool find_prop(propertyt &Prop);
   void read_parameters();
diff --git a/src/ic3/i1nit.cc b/src/ic3/i1nit.cc
index c9b772c02..19f5f77d6 100644
--- a/src/ic3/i1nit.cc
+++ b/src/ic3/i1nit.cc
@@ -165,9 +165,9 @@ void CompInfo::form_bad_states0(CNF &Bstates)
 	int var_ind1 = Pres_to_next[var_ind];
 	if (var_ind1 < 0) {
 	  p();
-	  printf("Pres_svars.size() = %d\n",(int) Pres_svars.size());
-	  printf("Next_svars.size() = %d\n",(int) Next_svars.size());
-	  exit(100);
+	  M->error() << "Pres_svars.size() = " << Pres_svars.size() <<	   
+               "Next_svars.size() = " << Next_svars.size() << M->eom;
+	  throw ERROR1;
 	}
 	if (C[j] < 0) Res.push_back(-(var_ind1+1));
 	else Res.push_back(var_ind1+1);
@@ -201,7 +201,7 @@ void CompInfo::form_cex()
   form_init_st(St_cube);
   Cex.push_back(St_cube);
  
-  std::string Name = "Gen_sat";
+  std::string Name("Gen_sat");
   init_sat_solver(Gen_sat,max_num_vars,Name);
 
   accept_new_clauses(Gen_sat,Tr);
diff --git a/src/ic3/i2nit_sat_solvers.cc b/src/ic3/i2nit_sat_solvers.cc
index cbe015380..9ab4652c0 100644
--- a/src/ic3/i2nit_sat_solvers.cc
+++ b/src/ic3/i2nit_sat_solvers.cc
@@ -9,6 +9,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <set>
 #include <map>
 #include <algorithm>
+#include <sstream>
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -101,9 +102,10 @@ void CompInfo::init_time_frame_solver(int tf_ind)
 {
  
   SatSolver &Slvr = Time_frames[tf_ind].Slvr;
-  char Name[MAX_NAME];
-  sprintf(Name,"Tf_sat%d",tf_ind);
-  std::string Slv_name = Name;
+
+
+  std::string Slv_name("Tf_sat" + std::to_string(tf_ind));
+  
   init_sat_solver(Slvr,max_num_vars0,Slv_name);
   
   if (tf_ind == 0) add_tf0_clauses(Slvr);
@@ -126,7 +128,7 @@ void CompInfo::init_time_frame_solver(int tf_ind)
 void CompInfo::init_lbs_sat_solver()
 {
 
-  std::string Name = "Lbs_sat";
+  std::string Name("Lbs_sat");
   init_sat_solver(Lbs_sat,max_num_vars0,Name);
 
   for (size_t i=0; i < Prop.size()-1; i++) 
@@ -166,7 +168,7 @@ void CompInfo::init_lbs_sat_solver()
 void CompInfo::init_lgs_sat_solver()
 {
 
-  std::string Name = "Lgs_sat";
+  std::string Name("Lgs_sat");
   init_sat_solver(Lgs_sat,max_num_vars0,Name);
   assert(Simp_PrTr.size() > 0);
 
@@ -187,7 +189,7 @@ void CompInfo::init_lgs_sat_solver()
   ======================================*/
 void CompInfo::init_bst_sat_solver()
 {
-  std::string Name = "Bst_sat";
+  std::string Name("Bst_sat");
   init_sat_solver(Bst_sat,max_num_vars,Name);
 
   // accept property and transition relation
diff --git a/src/ic3/l0ift_states.cc b/src/ic3/l0ift_states.cc
index fafe53a1e..6ba6a5ec1 100644
--- a/src/ic3/l0ift_states.cc
+++ b/src/ic3/l0ift_states.cc
@@ -53,10 +53,10 @@ void CompInfo::lift_good_state(CUBE &Gst_cube,CUBE &Prs_st,
   bool sat_form = check_sat2(Lgs_sat,Assmps);
   if (sat_form) {
     p();
-    std::cout << "Inps-> " << Inps << std::endl;
-    std::cout << "Prs_st-> " << Prs_st << std::endl;
-    std::cout << "Nst_cube-> " << Nst_cube << std::endl;
-    exit(100);
+    M->error() << "Inps-> " << ivect_to_str(Inps) << M->eom;
+    M->error() << "Prs_st-> " << ivect_to_str(Prs_st) << M->eom;
+    M->error() << "Nst_cube-> " << ivect_to_str(Nst_cube) << M->eom;
+    throw(ERROR1);
   }
   
 
diff --git a/src/ic3/m0ic3.hh b/src/ic3/m0ic3.hh
index e6a31e385..b8db28921 100644
--- a/src/ic3/m0ic3.hh
+++ b/src/ic3/m0ic3.hh
@@ -6,6 +6,8 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
 #include "aux_types.hh"
+#include "s0hared_consts.hh"
+#include <ebmc/ebmc_base.h>
 
 extern int debug_flag;
 /*================================
@@ -17,7 +19,7 @@ class CompInfo
 {
 public:
 
-  
+  messaget *M;
   Circuit *N; // circuit whose safety proprety is to be checked
   CUBE Ordering; // Ordering[i] specifies the order of a gate used to
                  // generate CNF formulas. For every input gate and latch
@@ -115,6 +117,12 @@ public:
 
   CNF F; // set of all inductive cubes
 
+
+  CNF Tr; // transition relation
+ 
+
+  CNF Ist; // initial states
+
   DNF Flits0; // 'Flits0' specifies clauses of F (in terms of indexes of F) that 
                  // contain the negative literal of 'i+1'
 
@@ -172,7 +180,8 @@ public:
   char print_cex_flag; // 0 - counterexample (cex) is not printed out, 
                        // 1 - cex is printed out as a text file
                        // 2 - cex is printed out as a CNF formula
-  char out_file[MAX_NAME]; // the root name of the output file
+  std::string out_file; // the root name of the output file
+ 
   int verbose; // specifies the level details to be printed out
   int gcount_max; // specifies the maximum value of gcount 
                   // (used for debugging)
@@ -323,12 +332,7 @@ protected:
   NameTable Name_table; // Table with the names of Sat-solvers for
                         //  which 'init_sat_solver' were invoked
 
- // ------------- init data
-
-  CNF Tr; // transition relation
  
-
-  CNF Ist; // initial states
  
 
  // protected methods
@@ -348,19 +352,21 @@ void array_to_set(SCUBE &A,CUBE &B);
 bool all_elems_smaller_than(int &err_ind,CUBE &A,int max);
 void form_lngst_clause(CLAUSE &C0,CUBE &St);
 void get_runtime (double &usrtime, double &systime);
-void my_printf(const char *format,...);
 void state_to_clauses(CNF &K,CUBE &A);
-void read_numbers(char *buf,int &num1,int &num2);
 void my_assert(bool cond);
 void find_latch(Circuit *N,Gate &G,int &latch_ind);
 void conv_to_vect(CCUBE &Name1,const char *Name0);
-void conv_to_vect(CCUBE &Name1,std::string &Name0);
+CCUBE conv_to_vect(std::string &Name);
+CCUBE conv_to_vect(const std::string &Name);
 bool overlap(CUBE &A,CLAUSE &B);
 int parse_string(CCUBE &Buff);
 void print_names_of_latches(NamesOfLatches &Latches);
 bool ident_arrays(CUBE &A,CUBE &B);
-void print_blif2(FILE *fp,Circuit *N);
-void print_blif3(const char *Name,Circuit *N);
+void print_blif(std::ofstream &Out_str,Circuit *N);
+void print_blif2(std::ofstream &Out_str,Circuit *N,messaget &M);
+void print_blif3(const char *Name,Circuit *N,messaget &M);
+std::string ivect_to_str(CUBE &A);
+std::string cvect_to_str(CCUBE &A);
 
 extern long long gcount;
 extern hsh_tbl htable_lits;
diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc
index 65e2ba3ea..403072bbe 100644
--- a/src/ic3/m1ain.cc
+++ b/src/ic3/m1ain.cc
@@ -11,8 +11,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <algorithm>
 #include <iostream>
 
-#include <ebmc/ebmc_base.h>
-
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -28,138 +26,170 @@ long long gcount = 0;
 
 /*=====================
 
-       D O _ I C 3
+  D O _ I C 3
 
   ====================*/
 int do_ic3(const cmdlinet &cmdline,
-	   ui_message_handlert &ui_message_handler)
+           ui_message_handlert &ui_message_handler)
 
 {
-  return(ic3_enginet(cmdline,ui_message_handler)());
+  return(ic3_enginet(cmdline, ui_message_handler)());
 } /* end of function do_ic3 */
 
 /*==================================
 
-    O P E R A T O R
+  O P E R A T O R
 
-   (functionall call reloading)
+  (functionall call reloading)
   =================================*/
 int ic3_enginet::operator()()
 
 {
+  messaget message(ui_message_handler);
+  Ci.M = &message;
 
 
-  Ci.init_parameters();
-  read_parameters();
+  try
+    {
+      Ci.init_parameters();
+      read_parameters();
 
-  try    {
-    int result=get_model();
-    if(result!=-1) return result;
+      int result=get_model();
 
-    if(make_netlist(netlist))     {
-      error() << "Failed to build netlist" << eom;
-      return 2;
-    }
-      
-    if(properties.empty())   {
-      error() << "no properties" << eom;
-      return 1;
+      if(result!=-1)
+        return result;
+
+
+      if(make_netlist(netlist))
+        {
+          Ci.M->error() << "Failed to build netlist" << Ci.M->eom;
+          throw ERROR1;
+        }
+
+
+      if(properties.empty())
+        {
+          error() << "no properties" << eom;
+          return ERROR1;
+        }
+
+
+      const0 = false;
+      const1 = false;
+      orig_names = false;
+
+
+
+      read_ebmc_input();
+
+      if(cmdline.isset("aiger"))
+        {
+          Ci.M->status() << "converting to aiger format" << Ci.M->eom;
+          Ci.print_aiger_format();
+          throw EARLY_EXIT;
+        }
+
+      netlistt().swap(this->netlist);
+
+      return(Ci.run_ic3());
     }
-  }
-
-  catch(const char *error_msg)    {
-    error() << error_msg << eom;
-    return 1;
-  }
-  catch(int)    {
-    return 1;
-  }
-
-  const0 = false;
-  const1 = false;
-  orig_names = false;
-  
-  // print_nodes();
-  // print_var_map(std::cout);
-  read_ebmc_input();
-  // print_blif3("tst.blif",Ci.N);
-  if (cmdline.isset("aiger")) {
-    printf("converting to aiger format\n");
-    Ci.print_aiger_format();
-    exit(0);
-  }
-  
-  //  printf("Constr_gates.size() = %d\n",Ci.Constr_gates.size()); 
-  return(Ci.run_ic3());
 
+
+
+  // catch blocks
+  catch(const char *error_msg)
+    {
+      Ci.M->error() << error_msg << Ci.M->eom;
+      return ERROR1;
+    }
+  catch(int err_num)
+    {
+      if(err_num != EARLY_EXIT)
+        Ci.M->error() << "exception number " << err_num << Ci.M->eom;
+      return err_num;
+    }
 } /* end of function operator */
 
 /* ======================
 
-       R U N _ I C 3
+   R U N _ I C 3
 
    ====================*/
 int CompInfo::run_ic3()
 {
-  double usrtime0=0.,systime0=0.;
-  double usrtime=0.,systime=0.;
- 
-  
+  double usrtime0=0., systime0=0.;
+  double usrtime=0., systime=0.;
+
+
   bool ok = check_init_states();
   assert(ok);
   assign_var_type();
   assign_value();
-  get_runtime (usrtime0, systime0);
+  get_runtime(usrtime0, systime0);
   int res = mic3();
-  get_runtime (usrtime, systime);  
+  get_runtime(usrtime, systime);
 
   int ret_val;
-  printf("\n");
-  switch (res) {
-  case 0: {
-    printf("property HOLDS\n");  
-    if (vac_true) {
-      printf("It is vacuously true\n");
-      ret_val = 2;
-      statistics = false;
+  
+  switch(res)
+    {
+    case 0:
+      {
+        M->result() << "property HOLDS" << M->eom;
+        if(vac_true)
+          {
+            M->result() << "It is vacuously true" << M->eom;
+            ret_val = 2;
+            statistics = false;
+            break;
+          }
+        if(print_inv_flag)
+          print_invariant(print_only_ind_clauses);
+        if(print_clauses_flag)
+          print_fclauses();
+        bool ok = ver_trans_inv();
+        if(ok)
+          ret_val = 2;
+        else
+          ret_val = 12;
+        break;
+      }
+    case 1:
+      {
+        M->result() << "property FAILED" << M->eom;
+        form_cex();
+        if(print_cex_flag == 1)
+          fprint_cex1();
+        else if(print_cex_flag == 2)
+          fprint_cex2();
+        if(print_clauses_flag)
+          print_invariant(true);
+
+        bool ok = ver_cex();
+        if(ok)
+          ret_val = 1;
+        else
+          ret_val = 11;
+        break;
+      }
+    case 2:
+      M->result() << "UNDECided" << M->eom;
+      ret_val = 3;
+      if(print_clauses_flag)
+        print_fclauses();
       break;
+    default:
+      assert(false);
     }
-    if (print_inv_flag) 
-      print_invariant(print_only_ind_clauses);
-    if (print_clauses_flag)
-      print_fclauses();
-    bool ok = ver_trans_inv();
-    if (ok) ret_val = 2;
-    else ret_val = 12;
-    break;}
-  case 1: {
-    printf("property FAILED\n");
-    form_cex();  
-    if (print_cex_flag == 1)
-      fprint_cex1();
-    else if (print_cex_flag == 2)
-      fprint_cex2();
-    if (print_clauses_flag) {
-      print_invariant(true);
+  if(statistics)
+    {
+      M->statistics() << "-------------" << M->eom;  
+      if((stat_data > 0) && (ret_val < 10))
+        print_stat();
+      M->result() << std::fixed;
+      M->result().precision(1);
+      M->result() << "total time is " << usrtime-usrtime0 << " sec." << M->eom;
     }
-    bool ok = ver_cex();
-    if (ok)  ret_val = 1;
-    else ret_val = 11;
-    break;}
-  case 2:
-    printf("UNDECided\n");
-    ret_val = 3;
-    if (print_clauses_flag) 
-      print_fclauses();
-    break;
-  default:
-    assert(false);
-  }
-  if (statistics) {
-    printf("*********\n");
-    if ((stat_data > 0) && (ret_val < 10)) print_stat();
-    printf("total time is %.2f sec.\n",usrtime-usrtime0);
-  }
   return(ret_val);
 } /* end of function run_ic3 */
 
@@ -167,75 +197,84 @@ int CompInfo::run_ic3()
 
 /*========================
 
-       M I C 3
+  M I C 3
 
-   Returns: 
-    0 - property holds
-    1 - property failed
-    2 - undecided
+  Returns:
+  0 - property holds
+  1 - property failed
+  2 - undecided
 
   =======================*/
 int CompInfo::mic3()
 {
+  check_conv_tbl(Pres_svars, Pres_to_next, true);
+  check_conv_tbl(Next_svars, Next_to_pres, false);
 
-  check_conv_tbl(Pres_svars,Pres_to_next,true);
-  check_conv_tbl(Next_svars,Next_to_pres,false);
- 
   htable_lits.hsh_init(4*max_num_vars+1);
   form_bad_states();
   form_property();
-  if (use_short_prop) form_short_property();
- 
+  if(use_short_prop)
+    form_short_property();
+
   ci_init();
   bool ok = init_st_satisfy_constrs();
-  if (!ok) {
-    vac_true = true;
-    return(0); // property holds
-  }
+  if(!ok)
+    {
+      vac_true = true;
+      return(0); // property holds
+    }
   ok = check_one_state_cex();
-  if (!ok) return(1); // property does not hold
+  if(!ok)
+    return(1); // property does not hold
 
   ok = check_two_state_cex();
-  if (!ok) return(1);
+  if(!ok)
+    return(1);
 
 
-  if (ctg_flag) form_coi_array();
+  if(ctg_flag)
+    form_coi_array();
   tf_lind = 1;
- 
+
 
   init_lbs_sat_solver();
   init_lgs_sat_solver();
   int ret_val = -1;
- 
-  while (true) {
-    max_num_tfs = tf_lind;
-    int res = next_time_frame();
-    print_time_frame_stat();
-    fflush(stdout);
-
-    if (verbose > 1) {
-      print_bnd_sets1();     
+
+  while(true)
+    {
+      max_num_tfs = tf_lind;
+      int res = next_time_frame();
+      print_time_frame_stat();
+      fflush(stdout);
+
+      if((res == 0) || (res == 1))
+        {
+          ret_val = res;
+          goto FINISH;
+        }
+
+      if(res == 3)
+        {
+          ret_val = 2;
+          goto FINISH;
+        }
+
+      assert(res == 2);
+      tf_lind++;
+      if(fin_tf > 0)
+        {
+          if(tf_lind > fin_tf)
+            {
+              ret_val = 2;
+              goto FINISH;
+            }
+        }
     }
-  
-    if ((res == 0) || (res == 1)) {
-      ret_val = res;
-      goto FINISH; }
-
-    if (res == 3) {
-      ret_val = 2;
-      goto FINISH;}
-
-    assert(res == 2);
-    tf_lind++;
-    if (fin_tf > 0) 
-      if (tf_lind > fin_tf) {
-	ret_val = 2;
-	goto FINISH;}
-  }
-  
+
  FINISH:
+  M->status() << "-------------" << M->eom;
   delete_solver(Lbs_sat);
   delete_solver(Lgs_sat);
   return(ret_val);
-
 } /* end of function mic3 */
diff --git a/src/ic3/m2ethods.hh b/src/ic3/m2ethods.hh
index 0473f4504..fa17d0146 100644
--- a/src/ic3/m2ethods.hh
+++ b/src/ic3/m2ethods.hh
@@ -164,7 +164,6 @@ bool init_st_satisfy_constrs();
 void form_spec_simp_pr_tr(SatSolver &Slvr);
 void load_clauses2(CNF &Ext_clauses,IctMinisat::SimpSolver *Sslvr,CNF &A,
                    int num_clauses);
-void print_bnd_sets1();
 void print_clause_state(int clause_ind);
 void add_constr_nilits(CNF &Bad_states);
 void add_constr_lits2(SatSolver &Slvr);
@@ -180,7 +179,7 @@ void form_next_state_vars();
 void form_inp_vars();
 void form_pres_to_next_conv();
 void form_next_to_pres_conv();
-void assign_var_indexes();
+void assign_var_indices();
 void add_last_cube(DNF &F);
 void form_property_gates(CUBE &Gates);
 void print_files(char *root);
@@ -199,8 +198,8 @@ void  gen_initial_state_cubes();
 
 
 // debugging methods
-void print_var_indexes();
-void print_var_indexes(char *name);
+void print_var_indices();
+void print_var_indices(const std::string &fname);
 //
 void init_gate_order();
 void gate_sort_inps_first();
@@ -210,16 +209,21 @@ void print_gate_sort_mode();
 //
 //  related to printing out circuit in aiger format
 void check_circuit(int &num_buffs,int &num_consts);
-void print_aiger_header(FILE *fp,int max_var,int num_gates);
-void print_aiger_inps(FILE *fp);
-void print_aiger_latches(FILE *fp);
+void print_aiger_header(std::ofstream &Out_str,int max_var,int num_gates);
+void print_aiger_inps(std::ofstream &Out_str);
+void print_aiger_latches(std::ofstream &Out_str);
 int find_aiger_lit1(int gate_ind,char polarity);
 int find_aiger_lit2(int gate_ind,char polarity);
-void print_aiger_gates(FILE *fp,DNF &Gates);
+void print_aiger_gates(std::ofstream &Out_str,DNF &Gates);
 void add_aiger_and_gate(DNF &Gates,int gate_ind);
 void add_aiger_buffer(DNF &Gates,int gate_ind);
-void print_aiger_output(FILE *fp,DNF &Gates,int out_ind);
+void print_aiger_output(std::ofstream &Out_str,DNF &Gates,int out_ind);
 int form_aiger_gates(DNF &Gates);
 void add_triplet(DNF &Gates,int olit,int lit0,int lit1);
 int find_max_aiger_var(DNF &Gates);
-void print_aiger_constrs(FILE *fp);
+void print_aiger_constrs(std::ofstream &Out_str);
+//
+void print_func_type(Gate &G,unsigned message_level);
+void my_printf(unsigned message_level,const char *format,...);
+void print_num_with_commas(unsigned message_level,const int &num);
+void print_bnd_sets1(unsigned message_level);
diff --git a/src/ic3/m4y_aiger_print.cc b/src/ic3/m4y_aiger_print.cc
index be2b2f660..f498482c0 100644
--- a/src/ic3/m4y_aiger_print.cc
+++ b/src/ic3/m4y_aiger_print.cc
@@ -11,8 +11,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <map>
 #include <algorithm>
 #include <iostream>
-
-#include <ebmc/ebmc_base.h>
+#include <fstream>
 
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
@@ -33,25 +32,26 @@ void CompInfo::print_aiger_format()
   int num_buffs;
   check_circuit(num_buffs,num_consts);
   assert(num_consts <= 2);
-  std::string full_name;
-  assert(strlen(out_file) > 0);
-  full_name = out_file;
-  full_name += ".aag";
+  assert(!out_file.empty());
+  std::string full_name(out_file += ".aag");
+
+  std::ofstream Out_str(full_name.c_str(),std::ios::out);
+  if (!Out_str) {
+    M->error() << "cannot open file " << full_name << M->eom;
+    throw(ERROR2);}
 
-  FILE *fp = fopen(full_name.c_str(),"w");
-  assert(fp!= NULL);
   
   DNF Gates;
   int out_ind = form_aiger_gates(Gates);
 
   int max_var = find_max_aiger_var(Gates);
-  print_aiger_header(fp,max_var,Gates.size());
-  print_aiger_inps(fp);
-  print_aiger_latches(fp);
-  print_aiger_output(fp,Gates,out_ind);
-  print_aiger_constrs(fp);
-  print_aiger_gates(fp,Gates);
-  fclose(fp);
+  print_aiger_header(Out_str,max_var,Gates.size());
+  print_aiger_inps(Out_str);
+  print_aiger_latches(Out_str);
+  print_aiger_output(Out_str,Gates,out_ind);
+  print_aiger_constrs(Out_str);
+  print_aiger_gates(Out_str,Gates);
+  Out_str.close();
 } /* end of function print_aiger_format */
 
 /*=======================================
@@ -128,22 +128,23 @@ int CompInfo::find_aiger_lit2(int gate_ind,char polarity)
     P R I N T _ A I G E R _ L A T C H E S
 
   ======================================*/
-void CompInfo::print_aiger_latches(FILE *fp)
+void CompInfo::print_aiger_latches(std::ofstream &Out_str)
 {
 
   for (size_t i=0; i < N->Latches.size(); i++) {
     int gate_ind = N->Latches[i];
     int lit = (gate_ind+1) << 1;
-    fprintf(fp,"%d ",lit);
+    Out_str << lit << " ";
     Gate &G = N->get_gate(gate_ind);
     assert(G.Fanin_list.size() == 1);
     int next_lit = find_aiger_lit1(G.Fanin_list[0],0);
-    fprintf(fp,"%d ",next_lit);
+    Out_str << next_lit << " ";
     if (G.init_value == 2) {
-      fprintf(fp,"%d\n",lit);
+      Out_str << lit << "\n";
       continue;}
     assert((G.init_value == 0) || (G.init_value == 1));
-    fprintf(fp,"%d\n",G.init_value);
+    if (G.init_value == 0)  Out_str <<  "0\n";
+    else Out_str << "1\n";
   }
 
 } /* end of function print_aiger_latches */
@@ -154,12 +155,12 @@ void CompInfo::print_aiger_latches(FILE *fp)
     P R I N T _ A I G E R _ I N P S
 
   ======================================*/
-void CompInfo::print_aiger_inps(FILE *fp)
+void CompInfo::print_aiger_inps(std::ofstream &Out_str)
 {
 
   for (size_t i=0; i < N->Inputs.size(); i++) {
     int gate_ind = N->Inputs[i];
-    fprintf(fp,"%d\n",(gate_ind+1)<<1);
+    Out_str << ((gate_ind+1) << 1) << "\n";
   }
 
 } /* end of function print_aiger_inps */
@@ -170,18 +171,18 @@ void CompInfo::print_aiger_inps(FILE *fp)
     P R I N T _ A I G E R _ H E A D E R
 
   ======================================*/
-void CompInfo::print_aiger_header(FILE *fp,int max_var,int num_gates)
+void CompInfo::print_aiger_header(std::ofstream &Out_str,int max_var,int num_gates)
 {
 
-  fprintf(fp,"aag ");
+  Out_str << "aag ";
 
-  fprintf(fp,"%d ",max_var); 
-  fprintf(fp,"%zu ",N->ninputs);
-  fprintf(fp,"%zu ",N->nlatches);
-  fprintf(fp,"1 ");
-  fprintf(fp,"%d",num_gates);
-  if (Constr_gates.size() == 0)  fprintf(fp,"\n");
-  else fprintf(fp," 0 %d\n",(int) Constr_gates.size());
+  Out_str << max_var << " "; 
+  Out_str << N->ninputs << " ";
+  Out_str << N->nlatches << " ";
+  Out_str << "1 ";
+  Out_str << num_gates;
+  if (Constr_gates.size() == 0)  Out_str << "\n";
+  else Out_str << " 0 " << Constr_gates.size() << "\n";
 } /* end of function print_aiger_header*/
 
 
@@ -207,8 +208,8 @@ void CompInfo::check_circuit(int &num_buffs,int &num_consts)
     cond |= (G.func_type == CONST);
     if (!cond) {
       p();
-      print_func_type(G);
-      exit(100);
+      print_func_type(G,messaget::M_ERROR);
+      throw(ERROR1);
     } 
 
     if (G.func_type == CONST) num_consts++;
@@ -220,10 +221,11 @@ void CompInfo::check_circuit(int &num_buffs,int &num_consts)
       cond |= (G.func_type == CONST);
       if (!cond)      {
         p();
-	printf("i = %zu\n",i);
-	printf("N->Gate_list.size() = %zu\n", N->Gate_list.size());
-	printf("G.ninputs = %zu\n",G.ninputs);
-	exit(100);
+	M->error() << "i = " << i << M->eom;
+	M->error() << "N->Gate_list.size() = " << N->Gate_list.size()
+		   << M->eom;
+	M->error() << "G.ninputs = " << G.ninputs << M->eom;
+	throw(ERROR1);
       }
     }
   }
diff --git a/src/ic3/m5y_aiger_print.cc b/src/ic3/m5y_aiger_print.cc
index 1387f7cef..c97169885 100644
--- a/src/ic3/m5y_aiger_print.cc
+++ b/src/ic3/m5y_aiger_print.cc
@@ -11,8 +11,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <map>
 #include <algorithm>
 #include <iostream>
-
-#include <ebmc/ebmc_base.h>
+#include <fstream>
 
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
@@ -26,7 +25,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
      P R I N T _ A I G E R _ C O N S T R S
 
   ============================================*/
-void CompInfo::print_aiger_constrs(FILE *fp)
+void CompInfo::print_aiger_constrs(std::ofstream &Out_str)
 {
 
   ConstrGates::iterator pnt;
@@ -35,7 +34,7 @@ void CompInfo::print_aiger_constrs(FILE *fp)
     int gate_ind = pnt->first;
     char neg_lit = pnt->second.neg_lit;
     int lit = find_aiger_lit2(gate_ind,neg_lit);
-    fprintf(fp,"%d\n",lit);
+    Out_str << lit << "\n";
   }
 } /* end of function print_aiger_constrs */
 
@@ -44,13 +43,13 @@ void CompInfo::print_aiger_constrs(FILE *fp)
      P R I N T _ A I G E R _ G A T E S
 
   ==========================================*/
-void CompInfo::print_aiger_gates(FILE *fp,DNF &Gates)
+void CompInfo::print_aiger_gates(std::ofstream &Out_str,DNF &Gates)
 {
 
   for (size_t i=0; i < Gates.size(); i++) {
     CUBE &C = Gates[i];
     assert(C.size() == 3);
-    fprintf(fp,"%d %d %d\n",C[0],C[1],C[2]);
+    Out_str << C[0] << " " << C[1] << " " << C[2] << "\n";
   }
 
 } /* end of function print_aiger_gates */
@@ -98,7 +97,7 @@ int CompInfo::find_max_aiger_var(DNF &Gates)
       P R I N T _ A I G E R _ O U T P U T
 
   ==========================================*/
-void CompInfo::print_aiger_output(FILE *fp,DNF &Gates,int out_ind)
+void CompInfo::print_aiger_output(std::ofstream &Out_str,DNF &Gates,int out_ind)
 {
   CUBE &C  = Gates[out_ind];
   assert(C.size() == 3);
@@ -113,7 +112,9 @@ void CompInfo::print_aiger_output(FILE *fp,DNF &Gates,int out_ind)
     if ((C[1] == 0) || (C[2] == 0)) // at least one of the inputs is 0
       lit++;
   }
-  fprintf(fp,"%d\n",lit);
+
+  Out_str << lit << "\n";
+  
 } /* end of function print_aiger_output */
 
 /*=============================================
@@ -157,34 +158,35 @@ void CompInfo::add_aiger_buffer(DNF &Gates,int gate_ind)
   P R I N T _ F U N C _ T Y P E
 
   ================================*/
-void print_func_type(Gate &G) 
+void CompInfo::print_func_type(Gate &G,unsigned message_level) 
 {
 
+  messaget::mstreamt &Ms = M->get_mstream(message_level);
   switch (G.func_type) {
   case CONST:
-    printf("CONST");
+    Ms << "CONST";
     break;
   case BUFFER:
-    printf("BUFFER");
+    Ms << "BUFFER";
     break;
   case AND:
-    printf("AND");
+    Ms << "AND";
     break;
   case OR:
-    printf("OR");
+    Ms << "OR";
     break;
   case TRUTH_TABLE:
-    printf("TRUTH_TABLE");
+    Ms << "TRUTH_TABLE";
     break;
   case COMPLEX:
-    printf("COMPLEX");
+    Ms << "COMPLEX";
     break;
   default:
-    printf("wrong value of func_type\n");
-    exit(100);
+    Ms <<"wrong value of func_type\n";
+    throw(ERROR1);
   }
 
-  printf("\n");
+  Ms << M->eom;
 
 } /* end of function print_func_type */
 
diff --git a/src/ic3/my_printf.cc b/src/ic3/my_printf.cc
index e577468af..a44accc77 100644
--- a/src/ic3/my_printf.cc
+++ b/src/ic3/my_printf.cc
@@ -14,34 +14,44 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <queue>
 #include <map>
 #include <iostream>
+#include <iomanip>
+
+#include "minisat/core/Solver.h"
+#include "minisat/simp/SimpSolver.h"
+
 #include "dnf_io.hh"
-const int factor = 1000;
+#include "ccircuit.hh"
+#include "m0ic3.hh"
+
+const int group_factor = 1000;
 
 /*================================================
 
     P R I N T _ N U M _ W I T H _ C O M M A S
 
   ================================================*/
-void print_num_with_commas(const int &num)
+void CompInfo::print_num_with_commas(unsigned message_level,const int &num)
 {
 
+  messaget::mstreamt &Ms = M->get_mstream(message_level);
   CUBE parts;
   int Num = num;
   while (true) {
-     int remainder = Num % factor;
-      int quotient = Num / factor;
+     int remainder = Num % group_factor;
+      int quotient = Num / group_factor;
       parts.push_back(remainder);
       if (quotient == 0) break;
       Num = quotient;
     }
 
-  size_t parts_size=parts.size();
-  for (size_t i=0; i < parts_size; i++)
-    {if (i ==  0) printf("%d",parts[parts_size-i-1]);
-      else printf("%03d",parts[parts_size-i-1]);
+  size_t num_of_parts=parts.size();
+  for (size_t i=0; i < num_of_parts; i++) {
+    if (i ==  0) Ms << parts[num_of_parts-i-1];
+    else Ms << std::setfill('0') <<  std::setw(3)
+		   << parts[num_of_parts-i-1];
      
-      if (i != 0) printf(",");
-    }
+    if (i != num_of_parts-1) Ms << ",";
+  }
 } /* end of function print_num_with_commas */
 
 /*=====================================================
@@ -54,22 +64,33 @@ void print_num_with_commas(const int &num)
   with commas
 
   =====================================================*/
-void my_printf(const char *format,...)
+void CompInfo::my_printf(unsigned message_level,const char *format,...)
 {
 
   va_list ap;
 
   va_start(ap,format); // n is the last parameter before the '...' 
                        // in the function header
+
+  bool flushed = false;
+  messaget::mstreamt &Ms = M->get_mstream(message_level);
   while (*format) {
     int c = *format++;
-    if (c != '%') {printf("%c",c); continue;}
+    if (c == '\n') {
+      Ms << M->eom;
+      flushed = true;
+      continue;}
+    
+    if (c != '%') {
+      Ms << (char) c;
+      continue;
+    }
     int spec = *format++;
     assert(spec == 'm');
     int num = va_arg(ap,int);
-    print_num_with_commas(num);      
-    //    printf("%d",num);    
+    print_num_with_commas(message_level,num);      
   }
   va_end(ap);
 
+  if (!flushed) Ms << M->eom;
 } /* end of function my_printf */
diff --git a/src/ic3/next_time_frame.cc b/src/ic3/next_time_frame.cc
index 8c2f93ac8..568089b89 100644
--- a/src/ic3/next_time_frame.cc
+++ b/src/ic3/next_time_frame.cc
@@ -31,14 +31,13 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 int CompInfo::next_time_frame()
 {
 
-  if (verbose == 0) {
-    printf("-------------\n");
-    printf("next_time_frame\n");
-    printf("tf_lind = %d\n",tf_lind);
-    printf("F.size() = %d, #inact. clauses %d\n",(int) F.size(),num_inact_cls);
-  }
-  
-
+ 
+  M->status() << "-------------" << M->eom;
+  M->status() << "next_time_frame" << M->eom;
+  M->status() << "tf_lind = " << tf_lind << M->eom;
+  M->status() << "F.size() = " << F.size() <<  ", #inact. clauses "
+	    << num_inact_cls << M->eom;
+ 
   int ret_val = 2;
   
   add_time_frame();
@@ -72,8 +71,7 @@ int CompInfo::next_time_frame()
     CNF G;  
     int min_tf;
     exclude_state_cube(G,min_tf,Gst_cube,Inps);
-    if (verbose > 0) 
-      if (min_tf < tf_lind - 1) printf("min_tf = %d\n",min_tf);
+   
     Time_frames[tf_lind].num_pbss++;
     if (time_to_terminate()) return(3);
     
@@ -84,13 +82,6 @@ int CompInfo::next_time_frame()
     // no counterexample
    
     assert(Pr_queue.size() == 0);
-    if (verbose >= 3) {
-      if (G.size() == 1) {
-	printf("inductive clause F[%d] is generated: ",(int) F.size());
-	std::cout << G[0] << std::endl;}
-      else printf("%d inductive CLAUSES are generated\n",(int) G.size());
-    }
-
     accept_new_clauses(Bst_sat,G);
   }
 
diff --git a/src/ic3/o1utput.cc b/src/ic3/o1utput.cc
index 0539526ab..7077584d2 100644
--- a/src/ic3/o1utput.cc
+++ b/src/ic3/o1utput.cc
@@ -10,6 +10,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <map>
 #include <algorithm>
 #include <iostream>
+#include <fstream>
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -24,11 +25,13 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 void CompInfo::fprint_cex2()
 {
 
-  char fname[MAX_NAME];
-  strcpy(fname,out_file);
-  strcat(fname,".cex.cnf");  
+  std::string fname(out_file + ".cex.cnf");
   
-  print_dnf(Cex,fname);
+  bool success = print_dnf(Cex,fname);
+  if (!success) {
+    M->error() << "cannot open file " << fname << M->eom;
+    throw ERROR2;
+  }
 
 } /* end of function fprint_cex2 */
 
@@ -41,24 +44,25 @@ void CompInfo::fprint_cex2()
 void CompInfo::fprint_cex1()
 {
 
-  char fname[MAX_NAME];
-  strcpy(fname,out_file);
-  strcat(fname,".cex.txt");  
-  FILE *fp = fopen(fname,"w");
-  assert(fp != NULL);
+  std::string fname(out_file + ".cex.txt");
+
+  std::ofstream Out_str(fname.c_str(),std::ios::out);
+  if (!Out_str) {
+    M->error() << "cannot open file " << fname << M->eom;
+    throw(ERROR2);}
 
   for (size_t i=0; i < Cex.size(); i++) {
-    fprintf(fp,"S%zu: ",i);
+    Out_str << "S" << i << ": ";
     CUBE &C = Cex[i];
     for (size_t k=0; k < C.size(); k++) {
-      if (k!=0) fprintf(fp," ");
-      if (C[k] > 0) fprintf(fp," ");
-      fprintf(fp,"%d",C[k]);
+      if (k!=0) Out_str << " ";
+      if (C[k] > 0) Out_str << " ";
+      Out_str << C[k];
     }
-    fprintf(fp,"\n");
+    Out_str << "\n";
   }
 
-  fclose(fp);
+  Out_str.close();
 
 } /* end of function fprint_cex1 */
 
@@ -78,11 +82,15 @@ void CompInfo::print_invariant(bool only_new_clauses)
   if (Cex.size() == 0)
     assert(Time_frames[inv_ind].num_bnd_cls == 0);
   add_dnf(Res,H);
-  char fname[MAX_NAME];
-  strcpy(fname,out_file);
-  if (inv_ind < 0) strcat(fname,".clauses.cnf");
-  else strcat(fname,".inv.cnf");  
-  print_dnf(Res,fname);
+  std::string fname(out_file);
+  
+  if (inv_ind < 0) fname += ".clauses.cnf";
+  else fname +=".inv.cnf";
+  bool success = print_dnf(Res,fname);
+  if (!success) {
+    M->error() << "cannot open file " << fname << M->eom;
+    throw(ERROR2);
+  }
 
 } /* end of function print_invariant */
 
@@ -94,10 +102,7 @@ void CompInfo::print_invariant(bool only_new_clauses)
 void CompInfo::print_fclauses()
 {
 
-
-  char fname[MAX_NAME];
-  strcpy(fname,out_file);
-  strcat(fname,".clauses.cnf"); 
+  std::string fname(out_file + ".clauses.cnf");
 
   CNF Res;
 
@@ -106,6 +111,10 @@ void CompInfo::print_fclauses()
     Res.push_back(F[i]);
   }
 
-  print_dnf(Res,fname);
+  bool success = print_dnf(Res,fname);
+  if (!success) {
+    M->error() << "cannot open file " << fname << M->eom;
+    throw(ERROR2);
+  }
 
 } /* end of function print_fclauses */
diff --git a/src/ic3/p1arameters.cc b/src/ic3/p1arameters.cc
index 1c536e27b..25028f313 100644
--- a/src/ic3/p1arameters.cc
+++ b/src/ic3/p1arameters.cc
@@ -11,8 +11,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <algorithm>
 #include <iostream>
 
-#include <ebmc/ebmc_base.h>
-
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -32,7 +30,7 @@ void ic3_enginet::read_parameters()
 
   if (cmdline.isset("h")) {
     print_header();
-    exit(0);
+    throw(EARLY_EXIT);
   }
 
   if (cmdline.isset("property")) 
@@ -55,9 +53,11 @@ void ic3_enginet::read_parameters()
 void ic3_enginet::print_header()
 {
 
-  printf("ebmc verilog_file --ic3 [--prop nm] [--constr]\n");
-  printf("prop nm - check property with name 'nm'\n");
-  printf("constr  - use constraints listed in 'verilog_file.cnstr'\n");
+  messaget *M = Ci.M;
+  M->status() << "ebmc verilog_file --ic3 [--prop nm] [--constr]"  << M->eom;
+  M->status() << "prop nm - check property with name 'nm'"  << M->eom;
+  M->status() << "constr  - use constraints listed in 'verilog_file.cnstr'"
+	      << M->eom;
 } /* end of function print_header */
 
 /*=====================================
@@ -71,7 +71,7 @@ void CompInfo::init_parameters()
   print_inv_flag = false;
   print_only_ind_clauses = 0;
   print_cex_flag = 0;
-  strcpy(out_file,"res");
+  out_file = "res";
   verbose = 0;
   gcount_max = -1;
   fin_tf = -1;
diff --git a/src/ic3/p2ush_clauses_forward.cc b/src/ic3/p2ush_clauses_forward.cc
index 84a0688a3..4a589073a 100644
--- a/src/ic3/p2ush_clauses_forward.cc
+++ b/src/ic3/p2ush_clauses_forward.cc
@@ -23,11 +23,9 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
   ===========================================*/
 void CompInfo::push_clauses_forward(bool triv_time_frame)
 {
-  if (verbose == 0) {
-    printf("%*c",3,' ');
-    printf("push_clauses_forward\n");  
-  }
-
+  
+  M->status() << "pushing clauses forward" << M->eom;
+  
   int min_tf = 1;
 
   assert(tf_lind>=0 && (size_t) tf_lind < Time_frames.size());
@@ -92,7 +90,8 @@ void CompInfo::push_clauses_forward(bool triv_time_frame)
 
     if (Time_frames[i].num_bnd_cls == 0) {
       inv_ind = i;
-      printf("All clauses of Bnd[%d] are pushed forward\n",inv_ind);
+      M->status() << "All clauses of Bnd[" << inv_ind
+		  << "] are pushed forward" << M->eom;
       break;}
    
   }
diff --git a/src/ic3/r0ead_input.cc b/src/ic3/r0ead_input.cc
index 767bf1a51..9d34dbe93 100644
--- a/src/ic3/r0ead_input.cc
+++ b/src/ic3/r0ead_input.cc
@@ -16,9 +16,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include "dnf_io.hh"
 #include "ccircuit.hh"
 #include "m0ic3.hh"
-
-
-#include <ebmc/ebmc_base.h>
 #include <util/cmdline.h>
 #include "ebmc_ic3_interface.hh"
 
@@ -38,11 +35,10 @@ void ic3_enginet::read_ebmc_input()
   
   assert(Ci.N->noutputs == 1);
   assert(Ci.N->nlatches > 0);
-  
+
   Ci.order_gates();
   std::string empty;
   Ci.gen_cnfs(empty.c_str(), false);
- 
 
   Ci.form_var_nums();
  
@@ -83,18 +79,18 @@ void ic3_enginet::form_circ_from_ebmc()
   form_invs();
   Ci.form_consts(N);
  
-  add_spec_buffs(N);
+  add_spec_buffs(N,*Ci.M);
 
   add_pseudo_inps(N);
  
-  fill_fanout_lists(N);
-  assign_gate_type(N,Out_names,true);
+  fill_fanout_lists(N,*Ci.M);
+  assign_gate_type(N,Out_names,true,*Ci.M);
   //   assign topological levels and other flags
-  assign_levels_from_inputs(N);
+  assign_levels_from_inputs(N,*Ci.M);
   // check_levels_from_inputs(N,true);
   set_trans_output_fun_flags(N);
-  set_feeds_latch_flag(N,true,true);
-  assign_levels_from_outputs(N);
+  set_feeds_latch_flag(N,true,true,*Ci.M);
+  assign_levels_from_outputs(N,*Ci.M);
   // check_levels_from_outputs(N,true);
 
 } /* end of function form_circ_from_ebmc */
@@ -117,15 +113,13 @@ void ic3_enginet::form_inputs()
     for (size_t j=0; j < var.bits.size(); j++) {  
       literalt lit =var.bits[j].current;
       int lit_val = lit.get();
-      //      printf("lit_val = %d\n",lit_val);
       CCUBE Name;
       if (orig_names) {
 	bool ok = form_orig_name(Name,lit);
 	assert(ok);}      
       else {
-	char Inp_name[MAX_NAME];
-	sprintf(Inp_name,"i%d",lit_val);   
-	conv_to_vect(Name,Inp_name);
+	std::string Inp_name("i" + std::to_string(lit_val));
+        Name = conv_to_vect(Inp_name);
       }
       Ci.Inps.insert(lit_val);
       add_input(Name,N,N->ninputs);
@@ -211,8 +205,7 @@ void ic3_enginet::add_verilog_conv_constrs()
 {
 
   for(literalt lit : netlist.constraints) {
-    if (lit.is_constant()) continue;
-    std::cout << "constraint literal " << lit.get() << "\n";
+    if (lit.is_constant()) continue;   
      Ci.Init_clits.insert(lit.get());
   }
 
diff --git a/src/ic3/r1ead_input.cc b/src/ic3/r1ead_input.cc
index a9633aef2..369f613bb 100644
--- a/src/ic3/r1ead_input.cc
+++ b/src/ic3/r1ead_input.cc
@@ -14,7 +14,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 #include <solvers/prop/aig_prop.h>
 #include <trans-netlist/instantiate_netlist.h>
-#include <ebmc/ebmc_base.h>
 
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
@@ -24,6 +23,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 #include "ebmc_ic3_interface.hh"
 
+
 /*====================================
 
       F I N D _ P R O P _ L I T
@@ -34,9 +34,11 @@ void ic3_enginet::find_prop_lit()
 
   propertyt Prop;
   bool found = find_prop(Prop);
-
   assert(found);
-  assert(Prop.expr.id()==ID_sva_always);    
+
+  if (Prop.expr.id()!=ID_sva_always) {
+    throw("unsupported property - only SVA always is implemented");
+  }
 
   assert(Prop.expr.operands().size()==1);
 
@@ -44,9 +46,10 @@ void ic3_enginet::find_prop_lit()
 
   found = banned_expr(Oper);
   if (found) {
-    printf("verification of properties of this type by IC3\n");
-    printf("is not implemented yet\n");
-    exit(100);
+    messaget *M = Ci.M;
+    M->error() << "verification of properties of this type by IC3" << M->eom;
+    M->error() << "is not implemented yet" << M->eom;
+    throw(ERROR1);
   }
   assert(Oper.type().id()==ID_bool);
  
@@ -58,14 +61,10 @@ void ic3_enginet::find_prop_lit()
   prop_l=instantiate_convert(aig_prop, netlist.var_map, Oper, ns,
 			     get_message_handler());
 
-  // int var_num = prop_l.var_no();
-  // printf("var_num = %d\n",var_num);
+ 
   
   if (prop_l.is_false()) Ci.const_flags = Ci.const_flags | 1;
-  else if (prop_l.is_true()) Ci.const_flags = Ci.const_flags | 2;
-
-  // print_lit(std::cout,prop_l);
-  // printf("\n");
+  else if (prop_l.is_true()) Ci.const_flags = Ci.const_flags | 2;  
   
 } /* end of function find_prop_lit */
 
@@ -110,9 +109,7 @@ void ic3_enginet::form_latched_gates()
     for (size_t j=0; j < var.bits.size(); j++) {
       literalt lit =var.bits[j].current;
       int init_val = Latch_val[lit.var_no()];
-      literalt next_lit = var.bits[j].next;
-      // int lit_val = next_lit.get();
-      // printf("next st. var: %d\n",lit_val);
+      literalt next_lit = var.bits[j].next;    
       add_new_latch(Latches,init_val,lit,next_lit);
     }
   }
@@ -149,7 +146,7 @@ void ic3_enginet::form_invs()
     Gate &G = N->get_gate(Gate_inds.back());
     G.F.push_back(C);
 
-    finish_gate(N,Gate_inds.back());
+    finish_gate(N,Gate_inds.back(),*Ci.M);
   }
 
 } /* end of function form_invs */
@@ -176,7 +173,7 @@ void ic3_enginet::add_new_latch(NamesOfLatches &Latches, int init_val,
  
  
   int pin_num = assign_output_pin_number(N->Pin_list,Latch_name,
-               N->Gate_list,true);
+					 N->Gate_list,true,*Ci.M);
   Ci.upd_gate_constr_tbl(pres_lit.get(),pin_num);
  
  
@@ -200,10 +197,11 @@ void ic3_enginet::add_new_latch(NamesOfLatches &Latches, int init_val,
 
 // we don't accept files in which the output of a latch is also a primary input
     if (G.gate_type == INPUT){
-      printf("the output of latch  ");  
-      print_name1(Latch_name,true);
-      printf("is also an input variable\n");
-      exit(1);
+      messaget *M = Ci.M;
+      M->error() << "the output of latch  ";
+      M->error() << cvect_to_str(Latch_name) << M->eom;
+      M->error() << "is also an input variable" << M->eom;
+      throw(ERROR1);
     }
   }
   
@@ -242,17 +240,30 @@ void conv_to_vect(CCUBE &Name1,const char *Name0)
     Name1.push_back(Name0[i]);
 } /* end of function conv_to_vect */
 
+
 /*===============================
 
      C O N V _ T O _ V E C T
 
   =============================*/
-void conv_to_vect(CCUBE &Name1,std::string &Name0)
+CCUBE conv_to_vect(std::string &Name)
 {
-  Name1.clear();
-  for (size_t i=0; i < Name0.size(); i++) 
-    Name1.push_back(Name0[i]);
-  
+
+  CCUBE V(Name.begin(),Name.end());
+  return(V);  
+
+} /* end of function conv_to_vect */
+
+/*===============================
+
+     C O N V _ T O _ V E C T
+
+  =============================*/
+CCUBE conv_to_vect(const std::string &Name)
+{
+ 
+  CCUBE V(Name.begin(),Name.end());
+  return(V);  
 
 } /* end of function conv_to_vect */
 
diff --git a/src/ic3/r2ead_input.cc b/src/ic3/r2ead_input.cc
index 28bfe627f..d81d58a5c 100644
--- a/src/ic3/r2ead_input.cc
+++ b/src/ic3/r2ead_input.cc
@@ -12,8 +12,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <algorithm>
 #include <iostream>
 
-#include <ebmc/ebmc_base.h>
-
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -36,7 +34,7 @@ void CompInfo::start_new_gate(CUBE &Gate_inds,Circuit *N,CDNF &Pin_names)
  
 
   int gate_ind = assign_output_pin_number(N->Pin_list,Pin_names.back(),
-                                          N->Gate_list,false);
+                                          N->Gate_list,false,*M);
 
   N->ngates++; // increment the number of gates 
 
@@ -88,7 +86,7 @@ void ic3_enginet::form_inv_names(CDNF &Pin_names,int lit)
 {
   
   assert ((lit & 1) == 0);
-  char Buff[MAX_NAME];
+  
   CCUBE Dummy;
   Pin_names.push_back(Dummy);
   Pin_names.push_back(Dummy);
@@ -100,30 +98,39 @@ void ic3_enginet::form_inv_names(CDNF &Pin_names,int lit)
     return;
   }
 
-
+  
   SCUBE &Inps = Ci.Inps;
 
+  std::string Name;
   if (Inps.find(lit) != Inps.end()) {
-    sprintf(Buff,"i%d",lit);
-    conv_to_vect(Pin_names[0],Buff);
-    sprintf(Buff,"ni%d",lit);
-    conv_to_vect(Pin_names[1],Buff);
+    {
+      Name = "i" + std::to_string(lit);
+      Pin_names[0] = conv_to_vect(Name);
+   
+      Name = "ni" + std::to_string(lit);
+      Pin_names[1] = conv_to_vect(Name);
+    }
     return;
   }
 
   SCUBE &Lats = Ci.Lats;
   if (Lats.find(lit) != Lats.end()) {
-    sprintf(Buff,"l%d",lit);
-    conv_to_vect(Pin_names[0],Buff);
-    sprintf(Buff,"nl%d",lit);
-    conv_to_vect(Pin_names[1],Buff);
+    {  
+      Name = "l" + std::to_string(lit);
+      Pin_names[0] = conv_to_vect(Name);
+  
+      Name = "nl" + std::to_string(lit);
+      Pin_names[1] = conv_to_vect(Name);
+    }
     return;
   }
 
-  sprintf(Buff,"a%d",lit);
-  conv_to_vect(Pin_names[0],Buff);
-  sprintf(Buff,"na%d",lit);
-  conv_to_vect(Pin_names[1],Buff);
+
+  Name = "a" + std::to_string(lit);
+  Pin_names[0] = conv_to_vect(Name);
+  Name = "na" + std::to_string(lit);
+  Pin_names[1] = conv_to_vect(Name);
+
    
 
 } /* end of function form_inv_names */
@@ -152,35 +159,46 @@ void ic3_enginet::form_next_symb(CCUBE &Name,literalt &next_lit)
   }
 
 
-  char Buff[MAX_NAME];
+  
+  
   int nlit;
  
 
   nlit = next_lit.get();
+
+ 
+  std::string Str_name;
   if (next_lit.sign()) {   
     if (orig_names) {
       form_neg_orig_name(Name,next_lit);
       return;}
     Ci.Invs.insert(nlit-1);
-    if (Ci.Inps.find(nlit-1) != Ci.Inps.end()) 
-      sprintf(Buff,"ni%d",nlit-1);
-    else  if (Ci.Lats.find(nlit-1) != Ci.Lats.end()) 
-      sprintf(Buff,"nl%d",nlit-1);
-    else sprintf(Buff,"na%d",nlit-1);
-    conv_to_vect(Name,Buff);
+    if (Ci.Inps.find(nlit-1) != Ci.Inps.end())
+      Str_name = "ni" + std::to_string(nlit-1);
+    else  if (Ci.Lats.find(nlit-1) != Ci.Lats.end())
+      Str_name = "nl" + std::to_string(nlit-1);
+    else 
+      Str_name = "na" + std::to_string(nlit-1);
+    Name = conv_to_vect(Str_name);
     return;
   }
+ 
 
 
   if (orig_names) {
     form_orig_name(Name,next_lit);
     return;
   }
-     
-  if (Ci.Inps.find(nlit) != Ci.Inps.end()) sprintf(Buff,"i%d",nlit);
-  else if (Ci.Lats.find(nlit) != Ci.Lats.end()) sprintf(Buff,"l%d",nlit);
-  else sprintf(Buff,"a%d",nlit);
-  conv_to_vect(Name,Buff);
+
+
+  if (Ci.Inps.find(nlit) != Ci.Inps.end())
+    Str_name = "i" + std::to_string(nlit);
+  else if (Ci.Lats.find(nlit) != Ci.Lats.end())
+    Str_name = "l" + std::to_string(nlit);
+  else
+    Str_name = "a" + std::to_string(nlit);
+  Name = conv_to_vect(Str_name);
+  
 
 } /* end of function form_next_symb */
 
@@ -218,10 +236,12 @@ void CompInfo::check_conv_tbl(CUBE &Vars,CUBE &Tbl,bool pres_svars)
     int var_ind = Vars[i]-1;
     if (Tbl[var_ind] == -1) {
       if (pres_svars) 
-	printf("no match for present state variable %d\n",var_ind+1);
+	M->error() << "no match for present state variable " << var_ind+1
+		  << M->eom;
       else 
-	printf("no match for next state variable %d\n",var_ind+1);
-      exit(1);
+	M->error() << "no match for next state variable "<< var_ind+1
+		  << M->eom;
+      throw(ERROR1);
     }
   }
 
diff --git a/src/ic3/r3ead_input.cc b/src/ic3/r3ead_input.cc
index 5d08150e8..20552a65d 100644
--- a/src/ic3/r3ead_input.cc
+++ b/src/ic3/r3ead_input.cc
@@ -12,8 +12,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <algorithm>
 #include <iostream>
 
-#include <ebmc/ebmc_base.h>
-
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -64,9 +62,9 @@ void ic3_enginet::add_gate_out_name(CCUBE &Name,literalt &lit,CUBE &Pol)
     form_orig_name(Name,lit);
     return;
   }
-  char Buff[MAX_NAME];
-  sprintf(Buff,"a%d",lit1);
-  conv_to_vect(Name,Buff);
+
+  std::string Str_name("a" + std::to_string(lit1));
+  Name = conv_to_vect(Str_name);
 
 } /* end of function add_gate_out_name */
 
@@ -108,18 +106,19 @@ void ic3_enginet::add_gate_inp_name(CCUBE &Name,literalt &lit,CUBE &Pol)
     return;
   }
 
-  char Buff[MAX_NAME];
+ 
+  std::string Str_name;
   if (Ci.Inps.find(lit1) != Ci.Inps.end()) {
-    sprintf(Buff,"i%d",lit1);
-    conv_to_vect(Name,Buff);
+    Str_name = "i" + std::to_string(lit1);
+    Name = conv_to_vect(Str_name);
   }
   else if (Ci.Lats.find(lit1) != Ci.Lats.end()) {
-    sprintf(Buff,"l%d",lit1);
-    conv_to_vect(Name,Buff);
+    Str_name = "l" + std::to_string(lit1);
+    Name = conv_to_vect(Str_name);
   }
   else {
-    sprintf(Buff,"a%d",lit1);
-    conv_to_vect(Name,Buff);
+    Str_name = "a" + std::to_string(lit1);
+    Name = conv_to_vect(Str_name);
   }
 
 } /* end of function add_gate_inp_name */
@@ -147,11 +146,7 @@ void ic3_enginet::form_gate_pin_names(CDNF &Pin_names,CUBE &Pol,
   literalt gt_lit(node_ind,false);
 
   add_gate_out_name(Pin_names[2],gt_lit,Pol);
-  // print_name1(Pin_names[2]);
-  // printf(": "); print_name1(Pin_names[0]);
-  // printf(" "); print_name1(Pin_names[1],true);
-  // printf(" Pin_names[0].size() = %d, Pin_names[1].size() = %d\n",(int) Pin_names[0].size(),
-  // 	 (int) Pin_names[1].size());
+  
 } /* end of function from_gate_pin_names */
 
 /*===============================
@@ -167,12 +162,7 @@ void ic3_enginet::form_gates()
 
   for (size_t i=0; i <  Nodes.size(); i++) {  
     aigt::nodet &Nd = Nodes[i];
-    if (Nd.is_var()) {
-      // printf("skipping a var node\n");
-      // literalt gt_lit(i,false);
-      // unsigned lit_val = gt_lit.get();
-      // printf("lit_val = %u\n",lit_val);
-      // printf("i = %zu\n",i);
+    if (Nd.is_var()) {   
       continue;
     }
     CDNF Pin_names;
@@ -182,7 +172,7 @@ void ic3_enginet::form_gates()
     Ci.start_new_gate(Gate_inds,N,Pin_names);
     upd_gate_constrs(i,Gate_inds);
     Ci.form_gate_fun(N,Gate_inds.back(),Pol);
-    finish_gate(N,Gate_inds.back());
+    finish_gate(N,Gate_inds.back(),*Ci.M);
   }
   
 
@@ -214,31 +204,33 @@ void ic3_enginet::form_outp_buf(CDNF &Out_names)
   CCUBE Dummy;
   Pin_names.push_back(Dummy);
   Pin_names.push_back(Dummy);
-  char Buff[MAX_NAME];
+
+  std::string Str_name;
+ 
   if (prop_l.is_false())  {
     Ci.const_false_prop = true;
-    sprintf(Buff,"c0");
-    conv_to_vect(Pin_names[0],Buff);
+    conv_to_vect(Pin_names[0],"c0");
     goto NEXT;  }
   if (prop_l.is_true()) {
     Ci.const_true_prop = true;
-    sprintf(Buff,"c1");
-    conv_to_vect(Pin_names[0],Buff);
+    conv_to_vect(Pin_names[0],"c1");
     goto NEXT;
   }
-  
+
+ 
   if (orig_names) 
     form_orig_name(Pin_names[0],prop_l,prop_l.sign());
   else {
-    if (latch) sprintf(Buff,"l%d",olit);
-    else sprintf(Buff,"a%d",olit);
-    conv_to_vect(Pin_names[0],Buff);
+    if (latch)
+      Str_name = "l" + std::to_string(olit);
+    else
+      Str_name = "a" + std::to_string(olit);
+    Pin_names[0] = conv_to_vect(Str_name);
   }
 
  NEXT:
-  char buff[MAX_NAME];
-  sprintf(buff,"%s",Ci.prop_name.c_str());
-  conv_to_vect(Pin_names[1],buff);
+ 
+  Pin_names[1] = conv_to_vect(Ci.prop_name);
   Out_names.push_back(Pin_names[1]);
 
   Circuit *N = Ci.N;
@@ -255,7 +247,7 @@ void ic3_enginet::form_outp_buf(CDNF &Out_names)
   Gate &G = N->get_gate(Gate_inds.back());
   G.F.push_back(C);
 
-  finish_gate(N,Gate_inds.back());
+  finish_gate(N,Gate_inds.back(),*Ci.M);
 
 } /* end of function form_outp_buf */
 
@@ -274,7 +266,7 @@ void CompInfo::form_consts(Circuit *N)
     conv_to_vect(Pin_names[0],"c0");
     CUBE Gate_inds;
     start_new_gate(Gate_inds,N,Pin_names);
-    finish_gate(N,Gate_inds.back());
+    finish_gate(N,Gate_inds.back(),*M);
   }
 
   if (const_flags & 2) {
@@ -287,7 +279,7 @@ void CompInfo::form_consts(Circuit *N)
     CUBE C;
     Gate &G = N->get_gate(Gate_inds.back());
     G.F.push_back(C);
-    finish_gate(N,Gate_inds.back());
+    finish_gate(N,Gate_inds.back(),*M);
   }
 
 } /* end of functin form_consts */
diff --git a/src/ic3/r4ead_input.cc b/src/ic3/r4ead_input.cc
index d9abcf276..a14f96502 100644
--- a/src/ic3/r4ead_input.cc
+++ b/src/ic3/r4ead_input.cc
@@ -12,8 +12,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <algorithm>
 #include <iostream>
 
-#include <ebmc/ebmc_base.h>
-
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -106,9 +104,8 @@ void ic3_enginet::form_latch_name(CCUBE &Latch_name,literalt &lit)
     assert(ok);        
     return; }
 
-  char Buff[MAX_NAME];
-  sprintf(Buff,"l%d",lit.get());
-  conv_to_vect(Latch_name,Buff);
+  std::string Str_name("l" + std::to_string(lit.get()));
+  Latch_name = conv_to_vect(Str_name);
 } /* end of function form_latch_name */
 
 
@@ -152,7 +149,7 @@ void print_names_of_latches(NamesOfLatches &Latches)
   for (pnt = Latches.begin(); pnt != Latches.end(); pnt++) {
     CCUBE A = pnt->first;
     print_name(&A);
-    printf("\n"); 
+    std::cout << "\n"; 
   }
 } /* end of function print_names_of_latches */
 
@@ -188,14 +185,13 @@ void ic3_enginet::ebmc_form_latches()
       literalt lit =var.bits[j].current;
       int var_num = lit.var_no();
       Latch_val[var_num] = 2; // set the value of the latch to a don't care
-      //      printf("latch val: %d\n",var_num);
     }
   }
 
   if (Latch_val.size() == 0) {
-    printf("there are no latches\n");
-    //    printf("Nondet_vars.size() = %d\n",(int) Nondet_vars.size());
-    exit(100);
+    messaget *M = Ci.M;
+    M->error() << "there are no latches" << M->eom;
+    throw(ERROR1);
   }
   // set initial values
   bvt Ist_lits;
@@ -206,11 +202,12 @@ void ic3_enginet::ebmc_form_latches()
     int var_num = lit.var_no();
     if (Latch_val.find(var_num) == Latch_val.end()) {
       p();
-      printf("Latch %d is not found\n",var_num);
-      printf("Latch_val.size() = %zu\n",Latch_val.size());
-      printf("Ist_lits.size() = %zu\n",Ist_lits.size());
-      printf("i = %zu\n",i);
-      exit(100);
+      messaget *M = Ci.M;
+      M->error() << "Latch " << var_num << " is not found" << M->eom;
+      M->error() << "Latch_val.size() = " << Latch_val.size() << M->eom;
+      M->error() << "Ist_lits.size() = " << Ist_lits.size() << M->eom;
+      M->error() << "i = " << i << M->eom;
+      throw(ERROR1);
     }
     if (lit.sign()) Latch_val[var_num] = 0;
     else Latch_val[var_num] = 1;
@@ -244,17 +241,15 @@ void ic3_enginet::gen_ist_lits(bvt &Ist_lits)
       continue;
     if (var_num >= Nodes.size()) {
       p();
-      printf("var_num = %zd\n",var_num);
-      printf("Nodes.size() = %zu\n",Nodes.size());
-      exit(100);
+      messaget *M = Ci.M;
+      M->error() << "var_num = " << var_num << M->eom;
+      M->error() << "Nodes.size() = " << Nodes.size() << M->eom;
+      throw(ERROR1);
     }
     aigt::nodet &Nd = Nodes[var_num];
 
     if (Nd.is_var()) {
-      Ist_lits.push_back(lit);
-      // literalt gt_lit(var_num,false);
-      // unsigned lit_val = gt_lit.get();
-      // printf("init st: lit_val = %u\n",lit_val);
+      Ist_lits.push_back(lit);    
       continue;
     }
 
diff --git a/src/ic3/r5ead_input.cc b/src/ic3/r5ead_input.cc
index 85fd6f9aa..d39fb712c 100644
--- a/src/ic3/r5ead_input.cc
+++ b/src/ic3/r5ead_input.cc
@@ -12,8 +12,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <algorithm>
 #include <iostream>
 
-#include <ebmc/ebmc_base.h>
-
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -44,67 +42,7 @@ bool ic3_enginet::banned_expr(exprt &expr) {
   return(false);
 } /* end of function expr_ident */
 
-/*====================================
-
-      P R I N T _ E X P R _ I D
 
-  ==================================*/
-void ic3_enginet::print_expr_id(exprt &expr)
-{
-
-  bool found = false;
-  printf("-------------\n");
-  if(expr.id()==ID_and) {
-    printf("ID_and\n");
-    found = true; }
-  if (expr.id()==ID_or) {
-    printf("ID_or\n");
-    found = true; }
-  if (expr.id()==ID_not) {
-    printf("ID_not\n");
-    found = true; }
-  if (expr.id()==ID_implies) {
-    printf("ID_implies\n");
-    found = true; }
-  if (expr.id()==ID_AG) {
-    printf("ID_AG\n");
-    found = true; }
-  if (expr.id()==ID_sva_always){
-    printf("ID_sva_always\n");
-    found = true; }
-  if (expr.id()==ID_sva_overlapped_implication) {
-    printf("ID_sva_overlapped_implication\n");
-    found = true; }
-  if (expr.id()==ID_sva_non_overlapped_implication) {
-    printf("ID_sva_non_overlapped_implication\n");
-    found = true; }
-  if (expr.id()==ID_sva_nexttime){
-    printf("ID_sva_nexttime\n");
-    found = true; }
-  if (expr.id()==ID_sva_eventually){
-    printf("ID_sva_eventually\n");
-    found = true; }
-  if (expr.id()==ID_sva_until) {
-    printf("ID_sva_until\n");
-    found = true;}
-  if (expr.id()==ID_sva_s_until) {
-    printf("ID_sva_s_until\n");
-    found = true;  }
-  if (expr.id()==ID_sva_until_with) {
-    printf("ID_sva_until_with\n");
-    found = true; }
-  if (expr.id()==ID_sva_s_until_with) {
-    printf("ID_sva_s__until_with\n");
-    found = true; }
- 
-  if (!found) {
-    printf("unknown expression\n");
-    exit(100);
-  }
-
-  printf("\n");
-
-} /* end of function print_expr_id */
 
 /*==========================================
 
@@ -137,14 +75,15 @@ bool ic3_enginet::form_orig_name(CCUBE &Name,literalt &lit,bool subtract)
 
   int var_num = lit.var_no();
   if (Gn[var_num].size() > 0) {
-    conv_to_vect(Name,Gn[lit.var_no()]);
+    Name = conv_to_vect(Gn[lit.var_no()]);
     return(true);
   }
 
-  char buf[MAX_NAME];
-  if (subtract) sprintf(buf,"a%d",lit.get()-1);
-  else sprintf(buf,"a%d",lit.get());   
-  conv_to_vect(Name,buf);
+  std::string Str_name;
+ 
+  if (subtract) Str_name = "a" + std::to_string(lit.get()-1);
+  else Str_name = "a" + std::to_string(lit.get());
+  Name = conv_to_vect(Str_name);
   return(false);
 } /* end of function form_orig_name */
 
@@ -159,7 +98,6 @@ void CompInfo::assign_value()
 
   // assign value to input literals
 
-  //  std::cout << "Constr_ilits-> " << Constr_ilits << std::endl;
   for (size_t i=0; i < Constr_ilits.size(); i++) {
     int lit = Constr_ilits[i];
     size_t var_ind = abs(lit)-1;
@@ -210,9 +148,11 @@ void CompInfo::form_constr_lits()
 	bool cond = (pnt->second.tran_coi || pnt->second.fun_coi);
 	if (cond == false) {
 	  p();
-	  printf("pnt->second.tran_coi = %d\n",pnt->second.tran_coi);
-	  printf("pnt->second.fun_coi = %d\n",pnt->second.fun_coi);
-	  exit(100);
+	  M->error() << "pnt->second.tran_coi = " << pnt->second.tran_coi
+		    << M->eom;
+	  M->error() << "pnt->second.fun_coi =" << pnt->second.fun_coi
+		    << M->eom;
+	  throw(ERROR1);
 	}
 	if (pnt->second.tran_coi)  Fun_coi_lits.push_back(lit);
 	if (pnt->second.fun_coi) Tr_coi_lits.push_back(lit);}
diff --git a/src/ic3/r6ead_input.cc b/src/ic3/r6ead_input.cc
index dc3175f34..2cbd8631c 100644
--- a/src/ic3/r6ead_input.cc
+++ b/src/ic3/r6ead_input.cc
@@ -21,7 +21,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <solvers/prop/aig_prop.h>
 #include <trans-netlist/instantiate_netlist.h>
 #include <util/cmdline.h>
-#include <ebmc/ebmc_base.h>
 #include "ebmc_ic3_interface.hh"
 
 /*===================================
@@ -53,18 +52,13 @@ void read_next_name(CCUBE &Name,bool &neg,FILE *fp)
 void ic3_enginet::read_constraints(const std::string &source_name)
 {
 
-  char fname[MAX_NAME];
-  int size = source_name.size();
-  assert(size < MAX_NAME-10);
-  source_name.copy(fname,size);
-  fname[size] = 0;
-  
-  strcat(fname,".cnstr");
+  std::string fname(source_name+".cnstr");
 
-  FILE *fp = fopen(fname,"r");
+  FILE *fp = fopen(fname.c_str(),"r");
   if (fp == NULL) {
-    printf("file %s listing constraints is missing\n",fname);
-    exit(100);
+    Ci.M->error() << "file " << fname << " listing constraints is missing"
+	       << Ci.M->eom;
+    throw ERROR1;
   }
 
   while (true) {
@@ -129,11 +123,9 @@ void ic3_enginet::form_orig_names()
       if (l_c.is_constant()) continue;
       unsigned ind = l_c.var_no();
       irep_idt Lname = it->first;
-      std::string Sname = short_name(Lname);
-      if (var.bits.size() > 1) {
-	char buf[100];
-	sprintf(buf,"[%zu]",j);
-	Sname += buf;
+      std::string Sname(short_name(Lname));
+      if (var.bits.size() > 1) {             
+	Sname +=  "[" + std::to_string(j) + "]";
       }
 
       assert(ind < Nodes.size());
@@ -152,20 +144,20 @@ void ic3_enginet::form_orig_names()
 void ic3_enginet::print_nodes()
 {
 
-  printf("\n-----  Nodes ------\n");
+  std::cout << "\n-----  Nodes ------\n";
   aigt::nodest &Nodes = netlist.nodes;
   for (size_t i=0; i <= Nodes.size(); i++) {  
     aigt::nodet &Nd = Nodes[i];
     if (Nd.is_var()) {
-      printf("Nd%zu: (var)\n",i);
+      std::cout << "Nd" << i << " (var)\n";
       continue;
     }
     
-    printf("Nd%zu = ",i);
+    std::cout << "Nd" << i << " = ";
     print_lit2(Nd.a.var_no(),Nd.a.sign());
-    printf(" & ");
+    std::cout <<  " & ";
     print_lit2(Nd.b.var_no(),Nd.b.sign());
-    printf("\n");    
+    std::cout << "\n";
 
   }
 
@@ -193,8 +185,8 @@ void ic3_enginet::print_lit1(unsigned var,bool sign)
 void ic3_enginet::print_lit2(unsigned var,bool sign)
 {
 
-  if (sign) printf("!");
-  printf("v%d",var);
+  if (sign) std::cout << "!";
+  std::cout << "v" << var;
 
 } /* end of function print_lit2 */
 
@@ -203,7 +195,6 @@ void ic3_enginet::print_lit2(unsigned var,bool sign)
        S H O R T _ N A M E
 
   ==============================*/
-
 std::string short_name(const irep_idt &Lname)
 {
   std::string Sname;
diff --git a/src/ic3/r7ead_input.cc b/src/ic3/r7ead_input.cc
index 8b53ec6b6..d217d5f64 100644
--- a/src/ic3/r7ead_input.cc
+++ b/src/ic3/r7ead_input.cc
@@ -20,7 +20,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 #include <solvers/prop/aig_prop.h>
 #include <trans-netlist/instantiate_netlist.h>
-#include <ebmc/ebmc_base.h>
 #include "ebmc_ic3_interface.hh"
 
 
@@ -33,7 +32,7 @@ void ic3_enginet::print_var_map(std::ostream &out)
 {
 
 
-  printf("\n-----  Var Map ------\n");
+  std::cout << "\n-----  Var Map ------\n";
 
   var_mapt &vm = netlist.var_map;
   for(var_mapt::mapt::const_iterator it=vm.map.begin();
@@ -115,8 +114,6 @@ void ic3_enginet::add_pseudo_inps(Circuit *N)
   for (size_t i=0; i < Gate_list.size();i++) {
     Gate &G=Gate_list[i];
     if (G.flags.active) continue;
-    // printf("inactive gate: ");
-    // print_name1(G.Gate_name,true);
 
     G.func_type = BUFFER;
     G.gate_type = INPUT;
@@ -154,9 +151,8 @@ void ic3_enginet::form_init_constr_lits()
     literalt l_c=var.bits[0].current;
     if (l_c.is_constant()) continue;
     irep_idt Lname = it->first;
-    std::string Sname = short_name(Lname);
-    CCUBE K;
-    conv_to_vect(K,Sname);    
+    std::string Sname(short_name(Lname));
+    CCUBE K = conv_to_vect(Sname);
     if (Ci.Cgate_names.find(K) != Ci.Cgate_names.end())  {
       literalt lit = l_c;
       if (Ci.Cgate_names[K] != l_c.sign()) lit = !l_c;
diff --git a/src/ic3/s0hared_consts.hh b/src/ic3/s0hared_consts.hh
new file mode 100644
index 000000000..827620b7e
--- /dev/null
+++ b/src/ic3/s0hared_consts.hh
@@ -0,0 +1,4 @@
+// termination values
+const int ERROR1 = 100; // a general error
+const int ERROR2 = 101; // an input/output error
+const int EARLY_EXIT = 50; // normal early exit
diff --git a/src/ic3/s1tat.cc b/src/ic3/s1tat.cc
index d73cc7c61..74220b1ba 100644
--- a/src/ic3/s1tat.cc
+++ b/src/ic3/s1tat.cc
@@ -17,7 +17,6 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include "ccircuit.hh"
 #include "m0ic3.hh"
 
-
 /*==============================
 
   P R I N T _ S T A T
@@ -26,39 +25,43 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 void CompInfo::print_stat()
 {
 
-  printf("num of time frames = %d\n",max_num_tfs);
-  if (inv_ind >= 0)   printf("inv_ind = %d\n",inv_ind);
-  my_printf("#inputs = %m, #outputs = %m, #latches = %m, #gates = %m\n",
-	    N->ninputs,N->noutputs,N->nlatches, N->ngates);
-  printf("total number of generated clauses is %d\n",(int) F.size()- 
-         (int) Ist.size() + init_ind_cls());
 
+  unsigned ms_lev = messaget::M_STATISTICS;
+  M->statistics() << "num of time frames = " << max_num_tfs << M->eom;
+  if (inv_ind >= 0)   M->statistics() << "inv_ind = " << inv_ind << M->eom;
+  my_printf(ms_lev,"#inputs = %m, #outputs = %m, #latches = %m, #gates = %m\n",
+	    N->ninputs,N->noutputs,N->nlatches, N->ngates);
+  M->statistics() << "total number of generated clauses is " <<  F.size()- 
+    Ist.size() + init_ind_cls() << M->eom;
 
-  my_printf("orig_ind_cls = %m, succ_impr = %m, failed_impr = %m\n",
+  my_printf(ms_lev,"orig_ind_cls = %m, succ_impr = %m, failed_impr = %m\n",
             orig_ind_cls,succ_impr,failed_impr);
   
 
   // print the total average size
 
-  printf("Aver. clause size = %.1f\n",average());
+  M->statistics() << std::fixed;
+  M->statistics().precision(1);
+  M->statistics() << "Aver. clause size = " << average() << M->eom;
 
-  printf("max. num. improv. of an ind. clause is %d\n",max_num_impr);
-  my_printf("#add1 = %m, #add2 = %m, #replaced = %m, #restore = %m\n",
+  M->statistics() << "max. num. improv. of an ind. clause is " << max_num_impr << M->eom;
+  my_printf(ms_lev,"#add1 = %m, #add2 = %m, #replaced = %m, #restore = %m\n",
             num_add1_cases,num_add2_cases,num_replaced_cases,num_restore_cases);
   print_sat_stat();
 
   print_flags();
 
-  printf("muliplier = %.2f\n",multiplier);
+  M->statistics().precision(2);
+  M->statistics() << "muliplier = " << multiplier << M->eom;
 
   print_lifting_stat();
-  my_printf("root_state_cnt = %m, new_state_cnt = %m, old_state_cnt = %m",
+  my_printf(ms_lev,"root_state_cnt = %m, new_state_cnt = %m, old_state_cnt = %m",
             root_state_cnt,new_state_cnt,old_state_cnt);
-  my_printf(" (triv = %m, rem = %m)\n",triv_old_st_cnt,
+  my_printf(ms_lev," (triv = %m, rem = %m)\n",triv_old_st_cnt,
             old_state_cnt-triv_old_st_cnt);
 
  
-  my_printf("#CTGs = %m, #excluded CTGS = %m\n",tot_ctg_cnt,succ_ctg_cnt);
+  my_printf(ms_lev,"#CTGs = %m, #excluded CTGS = %m\n",tot_ctg_cnt,succ_ctg_cnt);
 } /* end of function print_stat */
 
 
@@ -111,8 +114,8 @@ void CompInfo::print_one_sat_stat(SatSolver &S)
   if (Name_table.find(S.Name) == Name_table.end()) 
     return;
 
-  std::cout << S.Name << ": ";
-  printf("%d calls\n",S.tot_num_calls);
+  M->statistics() << S.Name << ": ";
+  M->statistics() << S.tot_num_calls <<  " calls" << M->eom;
 
 } /* end of function print_one_sat_stat */
 
@@ -124,43 +127,11 @@ void CompInfo::print_one_sat_stat(SatSolver &S)
   ========================================*/
 void CompInfo::print_time_frame_stat()
 {
-
-  if (verbose > 0) {
-    printf("------------------\n");
-    printf("finished time frame number %d\n",(int) Time_frames.size()-1);
-  }
-
-  TimeFrame &Tf = Time_frames[tf_lind];
-  if (verbose > 0) 
-    printf("new derived clauses Bnd[%d]=%d, Bnd[%d]=%d\n",tf_lind,
-           Tf.num_bnd_cls,tf_lind+1,
-	   Time_frames[tf_lind+1].num_bnd_cls);
-
-
-  if (verbose > 0)  {
-    printf("num_pbs-s: %d\n",Tf.num_pbss);
-
-    printf("Cti-s:\n");
-    int count = 0;
-    for (int i=tf_lind; i >=0; i--) {
-      if (Time_frames[i].num_rcnt_ctis == 0) continue;
-      if (count++ > 0) printf(", ");    
-      printf("Tf[%d] = %d",i,Time_frames[i].num_rcnt_ctis);
-      if (count % 10 == 0) printf("\n"); 
-    }
-
-    if (verbose > 0)
-      if (count % 10 != 0)  printf("\n");
-  }
- 
+    
   int time_frame_calls;
-  if (verbose > -1) print_time_frame_sat_stat(time_frame_calls);
+  print_time_frame_sat_stat(time_frame_calls);
 
-  if (verbose > 0) 
-    my_printf("F.size() = %m, num. inact. clauses  = %m\n",(int) F.size(), 
-              num_inact_cls);
-  //  printf("num. seen (redund) cls = %d (%d)\n",Tf.num_seen_cls,
-  // Tf.num_redund_cls);
+ 
 } /* end of function print_time_frame_stat*/
 
 
@@ -172,13 +143,14 @@ void CompInfo::print_time_frame_stat()
 void CompInfo::print_time_frame_sat_stat(int &time_frame_calls)
 {
 
+  unsigned ms_lev = messaget::M_STATISTICS;
   time_frame_calls = 0;
 
   for (size_t i=0; i < Time_frames.size(); i++) 
     time_frame_calls += Time_frames[i].Slvr.num_calls;
 
-  my_printf("Time frame SAT-solvers: %m calls\n",time_frame_calls); 
-  my_printf("Push clause SAT-solving: %m calls\n",num_push_clause_calls);
+  my_printf(ms_lev,"Time frame SAT-solvers: %m calls\n",time_frame_calls); 
+  my_printf(ms_lev,"Push clause SAT-solving: %m calls\n",num_push_clause_calls);
 
 } /* end of function print_time_frame_sat_stat */
 
@@ -190,6 +162,7 @@ void CompInfo::print_time_frame_sat_stat(int &time_frame_calls)
 void CompInfo::print_all_calls(int time_frame_calls)
 {
 
+  unsigned ms_lev = messaget::M_STATISTICS;
   int all_calls = time_frame_calls;
   if (Name_table.find(Gen_sat.Name) != Name_table.end()) 
     all_calls += Gen_sat.tot_num_calls;
@@ -205,7 +178,7 @@ void CompInfo::print_all_calls(int time_frame_calls)
 
 
 
-  my_printf("all solvers: %m calls\n",all_calls);
+  my_printf(ms_lev,"all solvers: %m calls\n",all_calls);
 
 } /* end of function print_all_calls */
 
diff --git a/src/ic3/s3tat.cc b/src/ic3/s3tat.cc
index 5f74f1052..89dba24d0 100644
--- a/src/ic3/s3tat.cc
+++ b/src/ic3/s3tat.cc
@@ -30,8 +30,10 @@ void CompInfo::print_lifting_stat()
 
   float av_bc_size = length_bstate_cubes / num_bstate_cubes;
   float av_gc_size = length_gstate_cubes / num_gstate_cubes;
-  printf("#svars = %d, aver. bst. cube = %.1f, aver. gst. cube = %.1f\n",
-	 (int) Pres_svars.size(),av_bc_size,av_gc_size);
+  M->statistics() << std::fixed;
+  M->statistics().precision(1);
+  M->statistics() << "#svars = " << Pres_svars.size() << ", aver. bst. cube = "
+	    << av_bc_size << ", aver. gst. cube = " << av_gc_size << M->eom;
  
 
 } /* end of function print_lifting_stat */
@@ -45,23 +47,23 @@ void CompInfo::print_lifting_stat()
 void CompInfo::print_flags()
 {
 
-  printf("rem_subsumed_flag = %d\n",rem_subsumed_flag);
+  M->statistics() << "rem_subsumed_flag = " << rem_subsumed_flag << M->eom;
 
   //  LIT_PICK_HEUR
   // 
-  printf("lit_pick_heur = ");
+  M->statistics() << "lit_pick_heur = ";
   switch (lit_pick_heur) {
   case RAND_LIT:
-    printf("RAND_LIT\n");
+    M->statistics() << "RAND_LIT" << M->eom;
     break;
   case INACT_LIT:
-    printf("INACT_LIT\n");
+    M->statistics() << "INACT_LIT" << M->eom;
     break;
   case INACT_VAR:
-    printf("INACT_VAR\n");
+    M->statistics() << "INACT_VAR" << M->eom;
     break;
   case FIXED_ORDER:
-    printf("FIXED_ORDER\n");
+    M->statistics() << "FIXED_ORDER" << M->eom;
     break;
   default:
     assert(false);
@@ -70,16 +72,16 @@ void CompInfo::print_flags()
 
   //  ACT_UPD_MODE
   // 
-  printf("act_upd_mode = ");
+  M->statistics() << "act_upd_mode = ";
   switch (act_upd_mode) {
   case NO_ACT_UPD:
-    printf("NO_ACT_UPD\n");
+    M->statistics() << "NO_ACT_UPD" << M->eom;
     break;
   case TF_ACT_UPD:
-    printf("TF_ACT_UPD\n");
+    M->statistics() << "TF_ACT_UPD" << M->eom;
     break;
   case MINISAT_ACT_UPD:
-    printf("MINISAT_ACT_UPD\n");
+    M->statistics() << "MINISAT_ACT_UPD" << M->eom;
     break;
   default:
     assert(false);
@@ -88,9 +90,9 @@ void CompInfo::print_flags()
   //  print sort modes
   // 
 
-  printf("sorted objects = ");
-  if (sorted_objects == LITS) printf("LITS\n");
-  else if (sorted_objects == VARS) printf("VARS\n");
+  M->statistics() << "sorted objects = ";
+  if (sorted_objects == LITS) M->statistics() << "LITS" << M->eom;
+  else if (sorted_objects == VARS) M->statistics() << "VARS" << M->eom;
   else assert(false);
 
   print_induct_lift_sort_mode("lift_sort_mode",lift_sort_mode);
@@ -98,10 +100,10 @@ void CompInfo::print_flags()
   print_induct_lift_sort_mode("ind_cls_sort_mode",ind_cls_sort_mode);
 
   print_gate_sort_mode();
-  printf("selector = %d\n",selector);
-  printf("ctg_flag = %d\n",ctg_flag);
-  printf("constr_flag = %d\n",constr_flag);
-  printf("standard_mode = %d\n",standard_mode);
+  M->statistics() << "selector = " << selector  << M->eom;
+  M->statistics() << "ctg_flag = " << ctg_flag  << M->eom;
+  M->statistics() << "constr_flag = " << constr_flag  << M->eom;
+  M->statistics() << "standard_mode = " << standard_mode  << M->eom;
  
 
 
@@ -116,17 +118,17 @@ void CompInfo::print_flags()
   =========================================================*/
 void CompInfo::print_induct_lift_sort_mode(const char *mode_name,int sort_mode) 
 {
-  printf("%s = ",mode_name);
+  M->statistics() << std::string(mode_name) << "= ";
   switch (sort_mode) {
   case NO_SORT:
-    printf("NO_SORT\n");
+    M->statistics() << "NO_SORT" << M->eom;
     break;
   case FULL_SORT:
-    printf("FULL_SORT\n");
+    M->statistics() << "FULL_SORT" << M->eom;
     break;
   case PART_SORT:
-    printf("PART_SORT\n");
-    printf("    max_num_elems = %zu\n",max_num_elems);
+    M->statistics() << "PART_SORT" << M->eom;
+    M->statistics() << "max_num_elems = " << max_num_elems << "" << M->eom;
     break;
   default:
     assert(false);
@@ -141,25 +143,25 @@ void CompInfo::print_induct_lift_sort_mode(const char *mode_name,int sort_mode)
 void CompInfo::print_gate_sort_mode()
 {
 
-  printf("gate_sort_mode = ");
+  M->statistics() << "gate_sort_mode = ";
   switch (gate_sort_mode) {
   case INIT_SORT:
-    printf("INIT_SORT");
+    M->statistics() << "INIT_SORT";
     break;
   case INPS_FIRST:
-    printf("INPS_FIRST");
+    M->statistics() << "INPS_FIRST";
     break;
   case OUTS_FIRST:
-    printf("OUTS_FIRST");
+    M->statistics() << "OUTS_FIRST";
     break;
   case RAND_SORT:
-    printf("RAND_SORT");
+    M->statistics() << "RAND_SORT";
     break;
   default:
     assert(false);
   }
 
-  printf("\n");
+  M->statistics()  << M->eom;
 
 } /* end of function print_gate_sort_mode */
 
diff --git a/src/ic3/seq_circ/a2dd_gate.cc b/src/ic3/seq_circ/a2dd_gate.cc
index 43a0520d0..389a9effc 100644
--- a/src/ic3/seq_circ/a2dd_gate.cc
+++ b/src/ic3/seq_circ/a2dd_gate.cc
@@ -13,9 +13,10 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <queue>
 #include <assert.h>
 #include <stdio.h>
+
 #include "dnf_io.hh"
 #include "ccircuit.hh"
-
+#include "s0hared_consts.hh"
 
 
 /*==========================================================
@@ -62,7 +63,8 @@ int assign_input_pin_number1(std::map<CCUBE,int> &pin_list,
   a new gate is added to gate_list
   =========================================================*/
 int assign_output_pin_number(std::map<CCUBE,int> &pin_list,
-			     CCUBE &name,GCUBE &gate_list,bool latch)
+			     CCUBE &name,GCUBE &gate_list,bool latch,
+			     messaget &M)
 {int pin_num;
   Gate G;
 
@@ -80,10 +82,9 @@ int assign_output_pin_number(std::map<CCUBE,int> &pin_list,
   else { /* an 'old' pin */
     pin_num=pin_list[name]; // add to input list the current gate input      
     if (gate_list[pin_num].flags.active == 1) {
-      printf("two gates have the same name "); 
-      print_name1(name); 
-      printf("\n");
-      exit(1);         
+      M.error() << "two gates have the same name " << M.eom; 
+      M.error() << cvect_to_str(name) << M.eom;
+      throw(ERROR1);   
     }
   }
   return(pin_num);
diff --git a/src/ic3/seq_circ/a3dd_gate.cc b/src/ic3/seq_circ/a3dd_gate.cc
index ec6b6ac52..015af4cb9 100644
--- a/src/ic3/seq_circ/a3dd_gate.cc
+++ b/src/ic3/seq_circ/a3dd_gate.cc
@@ -6,6 +6,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
 #include <iostream>
+#include <sstream>
 #include <list>
 #include <vector>
 #include <set>
@@ -14,6 +15,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <algorithm>
 #include <queue>
 
+
 #include <stdio.h>
 #include <assert.h>
 #include "dnf_io.hh"
@@ -31,15 +33,12 @@ void gen_fake_name(CCUBE &fake_name,int ind)
 
   fake_name.clear();
   fake_name.push_back(1); // add a non-character symbol
-  char buf[MAX_NAME];
-
-  sprintf(buf,"%d",ind);
-
-  for(int i=0; ;i++) {
-    if (buf[i] == 0) break;
-    fake_name.push_back(buf[i]);
-  }
   
+  std::string Str(std::to_string(ind));
+
+  for(size_t i=0;i < Str.size();i++) 
+    fake_name.push_back(Str[i]);
+    
 
 } /* end of function gen_fake_name */
 
diff --git a/src/ic3/seq_circ/a4dd_spec_buffs.cc b/src/ic3/seq_circ/a4dd_spec_buffs.cc
index e1663f7a5..74aa03ad2 100644
--- a/src/ic3/seq_circ/a4dd_spec_buffs.cc
+++ b/src/ic3/seq_circ/a4dd_spec_buffs.cc
@@ -24,12 +24,12 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
   A D D _ O N E _ S P E C _ B U F F
 
   ==========================================*/
-void add_one_spec_buff(Circuit *N,int ind) 
+void add_one_spec_buff(Circuit *N,int ind,messaget &M) 
 {
   int gate_ind = spec_buff_gate_ind(N,ind);
   start_spec_buff(N,gate_ind);
   add_spec_buff_cube(N,gate_ind);
-  finish_spec_buff(N,gate_ind);
+  finish_spec_buff(N,gate_ind,M);
 
 } /* end of function add_one_spec_buff */
 
diff --git a/src/ic3/seq_circ/a5dd_spec_buffs.cc b/src/ic3/seq_circ/a5dd_spec_buffs.cc
index 40bbf03e8..fee5bf359 100644
--- a/src/ic3/seq_circ/a5dd_spec_buffs.cc
+++ b/src/ic3/seq_circ/a5dd_spec_buffs.cc
@@ -7,6 +7,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
 #include <iostream>
+#include <sstream>
 #include <vector>
 #include <set>
 #include <map>
@@ -16,7 +17,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <stdio.h>
 #include "dnf_io.hh"
 #include "ccircuit.hh"
-
+#include "s0hared_consts.hh"
 
 
 /*===================================
@@ -24,7 +25,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
     F I N I S H _ S P E C _ B U F F 
 
   ==================================*/
-void finish_spec_buff(Circuit *N,int gate_ind)
+void finish_spec_buff(Circuit *N,int gate_ind,messaget &M)
 {
 
   Gate &G = N->get_gate(gate_ind);
@@ -35,8 +36,9 @@ void finish_spec_buff(Circuit *N,int gate_ind)
   DNF &R = G.R;
 
   if ((F.size()+ R.size()) != 1) {
-    printf("wrong buffer\n");
-    std::cout << G.Gate_name << std::endl;;
+    M.error() << "wrong buffer " << M.eom;
+    M.error() << cvect_to_str(G.Gate_name) << M.eom;
+    throw(ERROR1);
   }
 
   assert(F.size() == 1);
@@ -94,17 +96,16 @@ void form_output_name(CCUBE &Name,Circuit *N,int gate_ind)
 {
   Name =  N->Spec_buff_name;
 
-  char buff[MAX_NAME];
+  
   Gate &G = N->get_gate(gate_ind);
 
   assert(G.spec_buff_ind >= 0);
 
-  sprintf(buff,"%d",G.spec_buff_ind);
+  std::string Str(std::to_string(G.spec_buff_ind));
+
+  for(size_t i=0;i < Str.size();i++) 
+    Name.push_back(Str[i]);
 
-  for (int i=0; ; i++) {
-    if (buff[i] == 0) break;
-    Name.push_back(buff[i]);
-  }
 } /* end of function form_output_name */
 
 /*==================================
@@ -142,7 +143,7 @@ void start_spec_buff(Circuit *N,int gate_ind)
   A D D _ S P E C _ B U F F S
 
   =================================*/
-void add_spec_buffs(Circuit *N) 
+void add_spec_buffs(Circuit *N,messaget &M) 
 {
 
   if (N->num_spec_buffs == 0) return;
@@ -150,7 +151,7 @@ void add_spec_buffs(Circuit *N)
   gen_spec_buff_name(N);
 
   for (int i=0; i < N->num_spec_buffs; i++) 
-    add_one_spec_buff(N,i);
+    add_one_spec_buff(N,i,M);
 
 } /* end of function add_spec_buffs */
 
diff --git a/src/ic3/seq_circ/c2irc_util.cc b/src/ic3/seq_circ/c2irc_util.cc
index bd5d701ae..2469d504a 100644
--- a/src/ic3/seq_circ/c2irc_util.cc
+++ b/src/ic3/seq_circ/c2irc_util.cc
@@ -6,6 +6,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
 #include <iostream>
+#include <fstream>
 #include <vector>
 #include <set>
 #include <map>
@@ -13,7 +14,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <queue>
 #include "dnf_io.hh"
 #include "ccircuit.hh"
-
+#include "s0hared_consts.hh"
 
 /*===================================
 
@@ -22,7 +23,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
   ====================================*/
 void print_gate_name(Gate &G)
 {
-  printf("gate "); 
+  std::cout << "gate "; 
   print_name1(G.Gate_name);
 
 }/* end of function print_gate_name */
@@ -36,7 +37,7 @@ void print_gate_name(Gate &G)
 void print_name(CCUBE *name)
 {
   for (size_t i=0; i < name->size();i++)
-    printf("%c",(*name)[i]);
+    std::cout << (*name)[i];
 
 }/* end of function print_name */
 
@@ -45,29 +46,29 @@ void print_name(CCUBE *name)
   P R I N T _ G A T E _ T Y P E 
 
   ==========================================*/
-void  print_gate_type(FILE *fp,Circuit *N,Gate &G)
+void  print_gate_type(std::ofstream &Out_str,Circuit *N,Gate &G)
 {
   switch (G.gate_type) {
   case INPUT:
-    fprintf(fp,"INPUT\n");
+    Out_str << "INPUT\n";
     break;
   case GATE:
     if (!N->output_gate(G))
-      fprintf(fp,"INTERNAL gate\n");
+      Out_str << "INTERNAL gate\n";
     else if (N->ext_gate(G))
-      fprintf(fp,"EXTERNAL gate\n");
+      Out_str << "EXTERNAL gate\n";
     else if (N->ext_int_gate(G))
-      fprintf(fp,"EXTERNAL INTERANL gate\n");
+      Out_str << "EXTERNAL INTERANL gate\n";
     break;
   case LATCH:
-    fprintf(fp,"LATCH\n");
+    Out_str << "LATCH\n";
     break;
   case UNDEFINED:
-    fprintf(fp,"UNDEFINED gate\n");
+    Out_str << "UNDEFINED gate\n";
     break;
   default:
-    fprintf(fp,"wrong switch value\n");
-    exit(1);
+    Out_str << "wrong switch value\n";
+    throw(ERROR1);
   }
 
 
@@ -81,9 +82,9 @@ void  print_gate_type(FILE *fp,Circuit *N,Gate &G)
 void print_name1(CCUBE &name,bool cr)
 {
   for (size_t i=0; i < name.size();i++)
-    printf("%c",name[i]);
+    std::cout << name[i];
 
-  if (cr) printf("\n");
+  if (cr) std::cout << "\n";
 
 }/* end of function print_name1 */
 
@@ -124,16 +125,16 @@ void  print_levels(Circuit *N)
   fill_up_levels(N,Level_gates);
 
   for (size_t i=0; i < Level_gates.size(); i++) {
-    printf("level %zu:  ",i);
+    std::cout << "level " << i << ":  ";
     CUBE &Level = Level_gates[i];
  
     for (size_t j=0; j < Level.size();j++) {
       Gate &G = Gate_list[Level[j]];
       print_name1(G.Gate_name);
-      printf("(%zu)", G.Fanout_list.size());
-      printf(" ");
+      std::cout << "(" << G.Fanout_list.size() << ")";
+      std::cout << " ";
     }
-    printf("\n");
+    std::cout << "\n";
   }
 
 } /* end of function print_levels */
@@ -143,9 +144,9 @@ void  print_levels(Circuit *N)
   F P R I N T _ N A M E 
 
   ================================*/
-void fprint_name(FILE *fp,CCUBE &name)
+void fprint_name(std::ofstream &Out_str,CCUBE &name)
 {
   for (size_t i=0; i < name.size();i++)
-    fprintf(fp,"%c",name[i]);
+    Out_str << name[i];
 
 }/* end of function fprint_name */
diff --git a/src/ic3/seq_circ/ccircuit.hh b/src/ic3/seq_circ/ccircuit.hh
index d037a6748..a93fb3d12 100644
--- a/src/ic3/seq_circ/ccircuit.hh
+++ b/src/ic3/seq_circ/ccircuit.hh
@@ -6,6 +6,7 @@ Module: Basic types (gate, circuit and so on)
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
+#include <util/message.h>
 struct ConstrGateInfo {
   unsigned neg_lit:1;
   unsigned fun_coi:1;
@@ -142,17 +143,15 @@ public:
   void print_fanout_distrib(CUBE &A);
   void find_remaining_red_latches();
   void clean_latches();
-  void print_names1(FILE *fp,CUBE &gates,bool latch_flag);
-  void print_latch1(FILE *fp,Gate &G);
-  void print_gate1(FILE *fp,Gate &G);
+  void print_names1(std::ofstream &Out_str,CUBE &gates,bool latch_flag);
+  void print_latch1(std::ofstream &Out_str,Gate &G);
+  void print_gate1(std::ofstream &Out_str,Gate &G);
   void find_eq_class_reps();
   void finish_marking_red_latches();
   int find_rep(Gate &G);
   void print_no_fanout_gates();
 };
 
-#define MAX_LINE 10000
-
 
 
 #define n() {printf("\n");}
@@ -163,40 +162,33 @@ public:
 // constants
 //
 const int  NAMES_MAX = 10;
-const int MAX_NAME = 100;
 
 //
 //  functions   
 //
 void clear_labels(Circuit *N);
-void print_gate(FILE *fp,Circuit *N,Gate &G);
+void print_gate(std::ofstream &Out_str,Circuit *N,Gate &G);
 void print_gate_name(Gate &G);
 void print_gate_name1(Gate &G);
-void fprint_name(FILE *fp,CCUBE &name);
+void fprint_name(std::ofstream &Out_sr,CCUBE &name);
 void  print_levels(Circuit *N);
 void print_name1(CCUBE &name,bool cr = false);
 void print_subcircuit(Circuit *N,CCUBE &name);
 void rename_gates(Circuit *N,char C);
-void print_tr_rel(Circuit *N,char *root);
-void print_tr_rel_header(Circuit *N,FILE *Tr_rel,char *root);
 void print_st_vars(Circuit *N,char *root);
 void print_inp_vars(Circuit *N,char *root);
-void print_const(FILE *fp,Circuit *N,Gate &G);
+void print_const(std::ofstream &Out_str,Circuit *N,Gate &G);
 void self_looping_latches(Circuit *N);
 bool feeds_only_property(Circuit *N,Gate &G);
 bool feeds_only_latches_or_property(Circuit *N,Gate &G);
 void print_latch_stat(Circuit *N);
 void form_spec_latches(Circuit *N,CUBE &Spec_latches);
-void add_spec_latches(FILE *Tr_rel,Circuit *N,CUBE &Spec_latches);
 int get_fanout_latch(Circuit *N,CUBE &Fanout_gates);
-void print_gates_for_spec_latches(FILE *Tr_rel,Circuit *N,CUBE &Spec_latches);
-void print_latch_fed_by_input(FILE *Tr_rel,Gate &G1,Gate &G,int loc_ind);
-void print_latch_fed_by_const(FILE *Tr_rel,Gate &G1,Gate &G,int loc_ind);
 void my_printf(char *format,...);
 void remove_unobserv_gates(Circuit *N);
 void print_header1(Circuit *N);
 void print_names2(Circuit *N,CUBE &gates);
-void print_func_type(Gate &G);
-
+void  print_gate_type(std::ofstream &Out_str,Circuit *N,Gate &G);
+std::string cvect_to_str(CCUBE &A);
 #include "more_fun_prot.hh"
 
diff --git a/src/ic3/seq_circ/finish_gate.cc b/src/ic3/seq_circ/finish_gate.cc
index 7e1b2d7fb..837df6d0b 100644
--- a/src/ic3/seq_circ/finish_gate.cc
+++ b/src/ic3/seq_circ/finish_gate.cc
@@ -14,7 +14,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <stdio.h>
 #include "dnf_io.hh"
 #include "ccircuit.hh"
-
+#include "s0hared_consts.hh"
 
 
 /*==============================================
@@ -53,18 +53,18 @@ void finish_constant(Gate &G)
   The function fills up the polarities
   and sets the function  type
   =========================================*/
-void finish_buffer(Gate &G)
+void finish_buffer(Gate &G,messaget &M)
 {G.func_type = BUFFER;
 
   DNF &F = G.F;
   DNF &R = G.R;
 
   if ((F.size()+ R.size()) != 1) {
-    printf("wrong buffer\n");
+    std::cout << "wrong buffer\n";
     std::cout << G.Gate_name << std::endl;
-    printf("F.size() = %d\n",(int) F.size());
-    printf("R.size() = %d\n",(int) R.size());
-    exit(100);
+    std::cout << "F.size() = " << F.size() << "\n";
+    std::cout << "R.size() = " << R.size() << "\n";
+    throw(ERROR1);
   }
 
   // direct output
@@ -280,7 +280,7 @@ void finish_unknown_gate(Gate &G)
   In particular it determines gate type and fills up
   the polarities
   ==================================================*/
-void finish_gate(Circuit *N,int &gate_ind)
+void finish_gate(Circuit *N,int &gate_ind,messaget &M)
 {
 
   Gate &G=  N->Gate_list[gate_ind];
@@ -292,7 +292,7 @@ void finish_gate(Circuit *N,int &gate_ind)
 
   // is it a BUFFER?
   if (G.ninputs == 1) {
-    finish_buffer(G);
+    finish_buffer(G,M);
     return;
   }
  
diff --git a/src/ic3/seq_circ/l0ast_touch.cc b/src/ic3/seq_circ/l0ast_touch.cc
index 879ab0ef2..ebcc005c5 100644
--- a/src/ic3/seq_circ/l0ast_touch.cc
+++ b/src/ic3/seq_circ/l0ast_touch.cc
@@ -16,7 +16,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <stdio.h>
 #include "dnf_io.hh"
 #include "ccircuit.hh"
-
+#include "s0hared_consts.hh"
 
 /*========================================
 
@@ -28,7 +28,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
   as gates nor inputs
  
   ====================================-====*/
-void fill_fanout_lists(Circuit *N)
+void fill_fanout_lists(Circuit *N,messaget &M)
 {
 
   GCUBE &Gate_list = N->Gate_list;
@@ -44,13 +44,12 @@ void fill_fanout_lists(Circuit *N)
       //  check if G1 is a hanging input 
 
       if (G1.flags.active == 0) {
-	std::cout << "**   when processing the inputs of the gate ";
-        print_name1(G.Gate_name); 
-        std::cout << std::endl;
-	std::cout << "it is found that  gate ";
-        print_name1(G1.Gate_name);
-        std::cout << " is not defined" << std::endl;
-	//	exit(100);
+	M.error() << "**   when processing the inputs of the gate ";
+        M.error() << cvect_to_str(G.Gate_name) << M.eom;
+	M.error() << "it is found that  gate ";
+        M.error() << cvect_to_str(G1.Gate_name);
+        M.error() << " is not defined" << M.eom;
+	throw(ERROR1);
       }     
     }
   }
@@ -64,15 +63,16 @@ void fill_fanout_lists(Circuit *N)
  
   The function checks if there are "hanging" inputs
   ====================================================*/
-void  check_fanout_free_inputs(Circuit *N)
+void  check_fanout_free_inputs(Circuit *N,messaget &M)
 {CUBE &Inputs= N->Inputs;
 
   for (size_t i=0; i < Inputs.size();i++) {
     Gate &I =  N->Gate_list[Inputs[i]];
     if (I.Fanout_list.size() == 0) {
-      std::cout << "input "; 
-      print_name1(I.Gate_name); 
-      std::cout << " does not fan out\n";
+      M.error() << "input "; 
+      M.error() << cvect_to_str(I.Gate_name); 
+      M.error() << " does not fan out" << M.eom;
+      throw(ERROR1);
     }
 
   }
@@ -87,16 +87,15 @@ void  check_fanout_free_inputs(Circuit *N)
   the 'G.flags.output' flag if G is a primary output
  
   ======================================================*/
-void assign_gate_type(Circuit *N,CDNF &Out_names,bool rem_dupl_opt)
+void assign_gate_type(Circuit *N,CDNF &Out_names,bool rem_dupl_opt,messaget &M)
 { 
  
   for (size_t i=0; i < Out_names.size();i++) {
     CCUBE &name = Out_names[i];
     if (N->Pin_list.find(name) == N->Pin_list.end()) {
-      std::cout << "false output "; 
-      print_name(&name); 
-      std::cout << std::endl;
-      exit(1);
+      M.error() << "false output "; 
+      M.error() << cvect_to_str(name) << M.eom;
+      throw(ERROR1);
     }
     int gate_num = N->Pin_list[name];
     N->Outputs.push_back(gate_num); // record the gate as a circuit output
@@ -120,10 +119,10 @@ void assign_gate_type(Circuit *N,CDNF &Out_names,bool rem_dupl_opt)
       continue;
     if (!rem_dupl_opt)
       if (G.Fanout_list.size() == 0) {
-	std::cout << "gate "; 
-	print_name1(G.Gate_name); 
-	std::cout << " does not fan out\n";
-	exit(1);
+	M.error() << "gate "; 
+	M.error() << cvect_to_str(G.Gate_name); 
+	M.error() << " does not fan out" << M.eom;
+	throw(ERROR1);
       }
     G.gate_type = GATE;
   }
@@ -234,7 +233,7 @@ void set_trans_output_fun_flags(Circuit *N)
   Otherwise, returns 'false'
 
   ===============================================*/
-bool feeds_only_one_latch(Circuit *N,Gate &G)
+bool feeds_only_one_latch(Circuit *N,Gate &G,messaget &M)
 { int num_of_latches = 0;
   CUBE Latches;
 
@@ -248,15 +247,14 @@ bool feeds_only_one_latch(Circuit *N,Gate &G)
   }
  
   if (num_of_latches != 1) {
-    printf("error when checking the fanout of the gate ");
-    print_name1(G.Gate_name); printf("\n");
-    printf("total number of latches is %d\n",num_of_latches);
+    M.error() << "error when checking the fanout of the gate ";
+    M.error() << cvect_to_str(G.Gate_name) << M.eom;
+    M.error() << "total number of latches is " << num_of_latches << M.eom;
     for (size_t i=0; i < Latches.size(); i++) {
       Gate &G1 = N->get_gate(Latches[i]);
-      print_gate_name(G1);
-      printf("\n");
+      M.error() << cvect_to_str(G1.Gate_name) << M.eom;
     }
-    exit(1);
+    throw(ERROR1);
   }
   return(num_of_latches == 1);
 } /* end of function feeds_only_one_latch */
@@ -270,7 +268,8 @@ bool feeds_only_one_latch(Circuit *N,Gate &G)
   latch
 
   =============================================*/
-void set_feeds_latch_flag(Circuit *N,bool ignore_errors,bool rem_dupl_opt)
+void set_feeds_latch_flag(Circuit *N,bool ignore_errors,bool rem_dupl_opt,
+			  messaget &M)
 {
   for (size_t i=0; i < N->Latches.size();i++)   { 
     int gate_ind = N->Latches[i];
@@ -278,7 +277,7 @@ void set_feeds_latch_flag(Circuit *N,bool ignore_errors,bool rem_dupl_opt)
     int gate_ind1 = G.Fanin_list[0];
     Gate &G1 = N->get_gate(gate_ind1);
     if (!ignore_errors)
-      if (!rem_dupl_opt) assert(feeds_only_one_latch(N,G1));
+      if (!rem_dupl_opt) assert(feeds_only_one_latch(N,G1,M));
     G1.flags.feeds_latch = 1;
   }
 
diff --git a/src/ic3/seq_circ/l1ast_touch.cc b/src/ic3/seq_circ/l1ast_touch.cc
index 2b0abc4e4..52d4f2eaa 100644
--- a/src/ic3/seq_circ/l1ast_touch.cc
+++ b/src/ic3/seq_circ/l1ast_touch.cc
@@ -15,7 +15,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <stdio.h>
 #include "dnf_io.hh"
 #include "ccircuit.hh"
-
+#include "s0hared_consts.hh"
 
 
 
@@ -47,7 +47,7 @@ void print_levels_from_outputs(Circuit *N)
   for (size_t i=0; i < N->Gate_list.size();i++) {
     Gate &G =  N->Gate_list[i];
     print_name1(G.Gate_name);
-    printf(": %d\n",G.level_from_outputs);
+    std::cout << ": " << G.level_from_outputs << "\n";
   }
 
  
@@ -66,7 +66,7 @@ void print_levels_from_outputs(Circuit *N)
   are not assigned levels are added to the stack.
   =================================================================*/
 int check_levels_of_outputs(Gate &G,Circuit *N,int &level,
-			    CUBE &stack,bool &all_latches)
+			    CUBE &stack,bool &all_latches,messaget &M)
 { CUBE &Fanout_list = G.Fanout_list;
   
 
@@ -88,7 +88,7 @@ int check_levels_of_outputs(Gate &G,Circuit *N,int &level,
    
       if (G1.flags.label != 0) {
 	print_name1(G1.Gate_name); 
-        printf(" is visited but no level is assigned\n");
+        M.error() <<  "is visited but no level is assigned" << M.eom;
 	return(0); // G1 is in the stack, there is a loop in the circuit
       }
 
@@ -113,7 +113,7 @@ int check_levels_of_outputs(Gate &G,Circuit *N,int &level,
   returns 0 if the subcircuit contains a cycle. Otherwise
   it returns 1
   =====================================================================*/
-int assign_levels_from_outputs1(Circuit *N,int inp_num)
+int assign_levels_from_outputs1(Circuit *N,int inp_num,messaget &M)
 {CUBE stack;
   int level;
 
@@ -137,7 +137,7 @@ int assign_levels_from_outputs1(Circuit *N,int inp_num)
     }
     
     bool all_latches;
-    if (check_levels_of_outputs(G,N,level,stack,all_latches) == 0)
+    if (check_levels_of_outputs(G,N,level,stack,all_latches,M) == 0)
       return(0); // the subcircuit contains a cycle
     
     if (level >= 0) {
@@ -170,26 +170,26 @@ int assign_levels_from_outputs1(Circuit *N,int inp_num)
   3) N->max_levels is already set (when computing levels
   from inputs)
   ================================================================*/
-void assign_levels_from_outputs(Circuit *N)
+void assign_levels_from_outputs(Circuit *N,messaget &M)
 {
   clear_labels(N); 
 
   for (size_t i=0; i < N->Inputs.size();i++) {
-    if (assign_levels_from_outputs1(N,N->Inputs[i]) == 0) {
-      std::cout << "Circuit '"; 
-      print_name1(N->Circuit_name); 
-      std::cout << "' has a cycle\n";
-      exit(1);
+    if (assign_levels_from_outputs1(N,N->Inputs[i],M) == 0) {
+      M.error() << "Circuit '"; 
+      M.error() << cvect_to_str(N->Circuit_name); 
+      M.error() << "' has a cycle" << M.eom;
+      throw(ERROR1);
     }
   }
 
  
   for (size_t i=0; i < N->Latches.size();i++) {
-    if (assign_levels_from_outputs1(N,N->Latches[i]) == 0) {
-      std::cout << "Circuit '"; 
-      print_name1(N->Circuit_name); 
-      std::cout << "' has a cycle\n";
-      exit(1);
+    if (assign_levels_from_outputs1(N,N->Latches[i],M) == 0) {
+      M.error() << "Circuit '"; 
+      M.error() << cvect_to_str(N->Circuit_name); 
+      M.error() << "' has a cycle" << M.eom;
+      throw(ERROR1);
     }
   }
 
@@ -284,23 +284,23 @@ int assign_levels_from_inputs1(Circuit *N,int out_num)
  
   The function also checks if N is asyclic. 
   ==============================================================*/
-void assign_levels_from_inputs(Circuit *N)
+void assign_levels_from_inputs(Circuit *N,messaget &M)
 {
   clear_labels(N); 
 
   for (size_t i=0; i < N->Outputs.size();i++)
     if (assign_levels_from_inputs1(N,N->Outputs[i]) == 0) {
-      std::cout << "Circuit '"; 
-      print_name1(N->Circuit_name); 
-      std::cout << "' has a cycle\n";
-      exit(1);
+      M.error() << "Circuit '";
+      M.error() << cvect_to_str(N->Circuit_name); 
+      M.error() << "' has a cycle" << M.eom;
+      throw(ERROR1);
     }
 
   for (size_t i=0; i < N->Latches.size();i++)
     if (assign_levels_from_inputs1(N, N->Latches[i]) == 0) {
-      std::cout << "Circuit '"; 
-      print_name1(N->Circuit_name); 
-      std::cout << "' has a cycle\n";
-      exit(1);
+      M.error() << "Circuit '";
+      M.error() << cvect_to_str(N->Circuit_name); 
+      M.error() << "' has a cycle" << M.eom;
+      throw(ERROR1);
     }
 }/* end of function assign_levels_from_inputs */
diff --git a/src/ic3/seq_circ/more_fun_prot.hh b/src/ic3/seq_circ/more_fun_prot.hh
index 49514b269..6e594b012 100644
--- a/src/ic3/seq_circ/more_fun_prot.hh
+++ b/src/ic3/seq_circ/more_fun_prot.hh
@@ -1,28 +1,32 @@
 void add_input(CCUBE &name,Circuit *N,int inp_gate_num);
-void finish_gate(Circuit *N,int &gate_ind);
-void fill_fanout_lists(Circuit *N);
-void assign_gate_type(Circuit *N,CDNF &Out_names,bool rem_dupl_opt);
-void  assign_levels_from_inputs(Circuit *N);
-void  assign_levels_from_outputs(Circuit *N);
-void  print_names(FILE *fp,Circuit *N,CUBE &gates);
+void finish_gate(Circuit *N,int &gate_ind,messaget &M);
+void fill_fanout_lists(Circuit *N,messaget &M);
+void assign_gate_type(Circuit *N,CDNF &Out_names,bool rem_dupl_opt,messaget &M);
+void  assign_levels_from_inputs(Circuit *N,messaget &M);
+void  assign_levels_from_outputs(Circuit *N,messaget &M);
+void  print_names(std::ofstream &Out_str,Circuit *N,CUBE &gates);
 void print_name(CCUBE *name);
 Circuit *create_circuit(void);
 void init_gate_fields(Gate &G);
-int assign_output_pin_number(std::map<CCUBE,int> &pin_list,CCUBE &name,GCUBE &gate_list,bool latch);
-int assign_input_pin_number1(std::map<CCUBE,int> &pin_list,CCUBE &name,GCUBE &gate_list);
-int assign_input_pin_number2(NamesOfLatches &Latches,Circuit *N,CCUBE &name,GCUBE &gate_list);
+int assign_output_pin_number(std::map<CCUBE,int> &pin_list,CCUBE &name,
+			     GCUBE &gate_list,bool latch,messaget &M);
+int assign_input_pin_number1(std::map<CCUBE,int> &pin_list,CCUBE &name,
+			     GCUBE &gate_list);
+int assign_input_pin_number2(NamesOfLatches &Latches,Circuit *N,CCUBE &name,
+			     GCUBE &gate_list);
 void set_trans_output_fun_flags(Circuit *N);
-void set_feeds_latch_flag(Circuit *N,bool ignore_errors,bool rem_dupl_opt);
+void set_feeds_latch_flag(Circuit *N,bool ignore_errors,bool rem_dupl_opt,
+			  messaget &M);
 void fill_up_levels(Circuit *N, DNF &Level_gates);
-void circ_print_header(FILE *fp,Circuit *N);
-void print_latch(FILE *fp,Circuit *N,Gate &G);
+void circ_print_header(std::ofstream &Out_str,Circuit *N);
+void print_latch(std::ofstream &Out_str,Circuit *N,Gate &G);
 void gen_fake_name(CCUBE &fake_name,int ind);
-void add_spec_buffs(Circuit *N);
-void add_one_spec_buff(Circuit *N,int ind);
+void add_spec_buffs(Circuit *N,messaget &M);
+void add_one_spec_buff(Circuit *N,int ind,messaget &M);
 int spec_buff_gate_ind(Circuit *N,int ind);
 void start_spec_buff(Circuit *N,int gate_ind);
 void add_spec_buff_cube(Circuit *N,int gate_ind);
-void finish_spec_buff(Circuit *N,int gate_ind);
+void finish_spec_buff(Circuit *N,int gate_ind,messaget &M);
 void gen_spec_buff_name(Circuit *N);
 void set_input_polarity(CUBE &C,Gate &G);
 
diff --git a/src/ic3/seq_circ/p1rint_blif.cc b/src/ic3/seq_circ/p1rint_blif.cc
index 69eeb0c06..233f2b64a 100644
--- a/src/ic3/seq_circ/p1rint_blif.cc
+++ b/src/ic3/seq_circ/p1rint_blif.cc
@@ -5,6 +5,7 @@ Module:  Printing circuit in the BLIF format (Part 1)
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 ******************************************************/
 #include <iostream>
+#include <fstream>
 #include <list>
 #include <vector>
 #include <set>
@@ -24,11 +25,11 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
  Prints out circuit N in the blif format
 ====================================*/
-void print_blif(FILE *fp,Circuit *N)
+void print_blif(std::ofstream &Out_str,Circuit *N)
 {
   
   // print first three comands 
-  circ_print_header(fp,N);
+  circ_print_header(Out_str,N);
  //  print out the gates
 
   for (size_t i=0; i < N->Gate_list.size();i++)
@@ -37,18 +38,18 @@ void print_blif(FILE *fp,Circuit *N)
        {case INPUT: 
             break;
        case LATCH:
-	 print_latch(fp,N,G);
+	 print_latch(Out_str,N,G);
          break;
        case GATE:
-         if (G.func_type == CONST) print_const(fp,N,G);
-         else  print_gate(fp,N,G);
+         if (G.func_type == CONST) print_const(Out_str,N,G);
+         else  print_gate(Out_str,N,G);
          break;
        default: 
          assert(false); // we shouldn't reach this line
        }
    }
  //  print out the '.end' command
- fprintf(fp,".end\n");
+ Out_str << ".end\n";
 
 }/* end of function print_blif */
 
@@ -58,14 +59,18 @@ void print_blif(FILE *fp,Circuit *N)
       P R I N T _ L A T C H
 
 =======================================*/
-void print_latch(FILE *fp,Circuit *N,Gate &G)
+void print_latch(std::ofstream &Out_str,Circuit *N,Gate &G)
 {
- fprintf(fp,".latch ");
- print_names(fp,N,G.Fanin_list);
- fprintf(fp," "); fprint_name(fp,G.Gate_name);
+ Out_str << ".latch ";
+ print_names(Out_str,N,G.Fanin_list);
+ Out_str << " ";
+ fprint_name(Out_str,G.Gate_name);
 
  assert((G.init_value >= 0) && (G.init_value <= 4));
- fprintf(fp," %d\n",G.init_value);
+ if (G.init_value == 0)  Out_str <<  " 0\n";
+ else if (G.init_value == 1) Out_str << " 1\n";
+ else if (G.init_value == 2) Out_str << " 2\n";
+ else Out_str << " 3\n";
 
 
 }/*end of function print_latch */
@@ -76,22 +81,22 @@ void print_latch(FILE *fp,Circuit *N,Gate &G)
         P R I N T _ N A M E S
 
 ===========================================*/
-void print_names(FILE *fp,Circuit *N,CUBE &gates)
+void print_names(std::ofstream &Out_str,Circuit *N,CUBE &gates)
 {int count=0;
 
- for (size_t i=0; i < gates.size();i++)
-   {count++;
+  for (size_t i=0; i < gates.size();i++) {
+    count++;
     Gate &G =  N->Gate_list[gates[i]];
-    fprint_name(fp,G.Gate_name);
+    fprint_name(Out_str,G.Gate_name);
     if (i != gates.size()-1) // put a space if it is not the last name
-       fprintf(fp," ");
-// every NAMES_MAX names we add the extension symbol 
- // unless it is the last name 
-    if ((count == NAMES_MAX) && (i != gates.size()-1)) 
-      {count = 0; 
-       fprintf(fp,"\\\n");
-      }
-   }
+      Out_str << " ";
+  // every NAMES_MAX names we add the extension symbol 
+  // unless it is the last name 
+  if ((count == NAMES_MAX) && (i != gates.size()-1)) {
+    count = 0; 
+    Out_str << "\\\n";
+  }
+}
 
 } /* end of function print_names */
 
@@ -100,7 +105,7 @@ void print_names(FILE *fp,Circuit *N,CUBE &gates)
           P R I N T _ C U B E 
 
 =================================*/
-void print_cube(FILE *fp,CUBE &C,int ninputs)
+void print_cube(std::ofstream &Out_str,CUBE &C,int ninputs)
 {CCUBE L;
 
  for (int i=0; i < ninputs; i++)
@@ -115,13 +120,13 @@ void print_cube(FILE *fp,CUBE &C,int ninputs)
  for (size_t i=0; i < L.size();i++)
    {switch (L[i])
      {case 0:
-        fprintf(fp,"0");
+        Out_str << "0";
         break;
       case 1:
-        fprintf(fp,"1");
+        Out_str << "1";
         break;
       case 2:
-        fprintf(fp,"-");
+        Out_str << "-";
         break;
      }
    }
@@ -131,14 +136,14 @@ void print_cube(FILE *fp,CUBE &C,int ninputs)
       P R I N T _ C O N S T
 
 =======================================*/
-void print_const(FILE *fp,Circuit *N,Gate &G)
+void print_const(std::ofstream &Out_str,Circuit *N,Gate &G)
 {
   // print the .names command
- fprintf(fp,".names ");
- fprint_name(fp,G.Gate_name);
- fprintf(fp,"\n");
+ Out_str << ".names ";
+ fprint_name(Out_str,G.Gate_name);
+ Out_str << "\n";
  
- if (G.F.size() == 1) fprintf(fp,"1\n");
+ if (G.F.size() == 1) Out_str << "1\n";
 
 }/* end of function print_const */
 /*=======================================
@@ -146,24 +151,25 @@ void print_const(FILE *fp,Circuit *N,Gate &G)
       P R I N T _ G A T E
 
 =======================================*/
-void print_gate(FILE *fp,Circuit *N,Gate &G)
+void print_gate(std::ofstream &Out_str,Circuit *N,Gate &G)
 {
   // print the .names command
- fprintf(fp,".names ");
- print_names(fp,N,G.Fanin_list);
- fprintf(fp," "); fprint_name(fp,G.Gate_name);
- fprintf(fp,"\n");
+ Out_str << ".names ";
+ print_names(Out_str,N,G.Fanin_list);
+ Out_str << " ";
+ fprint_name(Out_str,G.Gate_name);
+ Out_str << "\n";
 
  // print the cubes of the ON-set
 
  for (size_t i=0; i < G.F.size();i++) {
-   print_cube(fp,G.F[i],G.ninputs);
-   fprintf(fp," 1\n");
+   print_cube(Out_str,G.F[i],G.ninputs);
+   Out_str << " 1\n";
  }
  // print the cubes of the OFF-set
  for (size_t i=0; i < G.R.size();i++) {
-   print_cube(fp,G.R[i],G.ninputs);
-   fprintf(fp," 0\n");
+   print_cube(Out_str,G.R[i],G.ninputs);
+   Out_str << " 0\n";
  }   
 
 
@@ -176,21 +182,24 @@ void print_gate(FILE *fp,Circuit *N,Gate &G)
  The function prints the head
  of a blif file
 ======================================*/
-void circ_print_header(FILE *fp,Circuit *N)
+void circ_print_header(std::ofstream &Out_str,Circuit *N)
 {
 // print out the '.model' command
- fprintf(fp,".model ");
- fprint_name(fp,N->Circuit_name);
- fprintf(fp,"\n");
+ Out_str << ".model ";
+ if (N->Circuit_name.size() > 0)
+   fprint_name(Out_str,N->Circuit_name);
+ else
+   Out_str << "seq_circ";
+ Out_str << "\n";
 
  // print out the '.inputs' command
- fprintf(fp,".inputs ");
- print_names(fp,N,N->Inputs);
- fprintf(fp,"\n");
+ Out_str << ".inputs ";
+ print_names(Out_str,N,N->Inputs);
+ Out_str << "\n";
  // print out the '.outputs' command
- fprintf(fp,".outputs ");
- print_names(fp,N,N->Outputs);
- fprintf(fp,"\n");
+ Out_str << ".outputs ";
+ print_names(Out_str,N,N->Outputs);
+ Out_str << "\n";
 }/* end of function circ_print_header */
 
 
diff --git a/src/ic3/seq_circ/p2rint_blif.cc b/src/ic3/seq_circ/p2rint_blif.cc
index 3aee55857..2ced3bd71 100644
--- a/src/ic3/seq_circ/p2rint_blif.cc
+++ b/src/ic3/seq_circ/p2rint_blif.cc
@@ -5,6 +5,7 @@ Module:  Printing circuit in the BLIF format (Part 2)
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 ******************************************************/
 #include <iostream>
+#include <fstream>
 #include <list>
 #include <vector>
 #include <set>
@@ -17,6 +18,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <assert.h>
 #include "dnf_io.hh"
 #include "ccircuit.hh"
+#include "s0hared_consts.hh"
 
 /*=======================================
 
@@ -26,17 +28,17 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
  function guarantees that all latches
  are printed out one by one
 ========================================*/
-void print_blif2(FILE *fp,Circuit *N)
+void print_blif2(std::ofstream &Out_str,Circuit *N,messaget &M)
 {
   
   // print first three commands 
-  circ_print_header(fp,N);
+  circ_print_header(Out_str,N);
  
   //  print out latches
   CUBE &Latches = N->Latches;
   for (size_t i=0; i < Latches.size(); i++)  {
     Gate &G = N->get_gate(Latches[i]);
-    print_latch(fp,N,G);
+    print_latch(Out_str,N,G);
   }
  
   for (size_t i=0; i < N->Gate_list.size();i++) {
@@ -46,22 +48,22 @@ void print_blif2(FILE *fp,Circuit *N)
        case LATCH:
 	break;
       case GATE:
-	if (G.func_type == CONST) print_const(fp,N,G);
-	else  print_gate(fp,N,G);
+	if (G.func_type == CONST) print_const(Out_str,N,G);
+	else  print_gate(Out_str,N,G);
 	break;
       case UNDEFINED: 
 	p();
-	printf("type of gate ");
-	print_name(&G.Gate_name);
-	printf(" is UNDEFINED\n");
-	exit(100);
+	M.error() << "type of gate ";
+	M.error() << cvect_to_str(G.Gate_name);
+	M.error() << " is UNDEFINED" << M.eom;
+	throw(ERROR1);
       default:
 	assert(false);
       }
   }
 
  //  print out the '.end' command
- fprintf(fp,".end\n");
+  Out_str << ".end\n";
 
 }/* end of function print_blif2 */
 
@@ -70,12 +72,15 @@ void print_blif2(FILE *fp,Circuit *N)
    P R I N T _ B L I F 3
 
 ==========================*/
-void print_blif3(const char *fname, Circuit *N)
+void print_blif3(const char *fname, Circuit *N,messaget &M)
 {
 
-  FILE *fp = fopen(fname,"w");
-  assert(fp!= NULL);
-  print_blif2(fp,N);
-  fclose(fp);
+  std::ofstream Out_str(fname,std::ios::out);
+  if (!Out_str) {
+    M.error() << "cannot open file " << std::string(fname) << M.eom;
+    throw(ERROR2);}
+  
+  print_blif2(Out_str,N,M);
+  Out_str.close();
 
 } /* end of function print_blif3 */
diff --git a/src/ic3/u0til.cc b/src/ic3/u0til.cc
index 761b337e7..9d504d070 100644
--- a/src/ic3/u0til.cc
+++ b/src/ic3/u0til.cc
@@ -11,6 +11,8 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <algorithm>
 #include <iostream>
 #include <sys/resource.h>
+
+
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -106,8 +108,9 @@ void CompInfo::part_sort(CLAUSE &C1,CLAUSE &C, std::vector <ActInd> &V) {
 
   if (C.size() != C1.size()) {
     p();
-    printf("C.size() = %d, C1.size() = %d\n",(int) C.size(), (int) C1.size());
-    exit(100);
+    M->error() << "C.size() = " << C.size() << ", C1.size() = " <<  C1.size()
+	       << M->eom;
+    throw(ERROR1);
   }
   
 } /* end of function part_sort */
@@ -146,19 +149,20 @@ void array_to_set(SCUBE &A,CUBE &B)
   P R I N T _ B N D _ S E T S 1
 
   ===================================*/
-void CompInfo::print_bnd_sets1()
+void CompInfo::print_bnd_sets1(unsigned message_level)
 {
 
+  messaget::mstreamt &Ms = M->get_mstream(message_level);
   for (size_t i=0; i < Time_frames.size(); i++) {
-    printf("Bnd[%zu]: ",i);
+    Ms << "Bnd[" << i << "]: ";
     int count = 0;
     for (size_t j=0; j < F.size(); j++) {
       if (Clause_info[j].active == 0) continue;
       if (Clause_info[j].span != i) continue;
-      if (count++ > 0) printf(" ");
-      printf("%zu",j);
+      if (count++ > 0) Ms << " ";
+      Ms << j;
     }
-    printf("\n");
+    Ms << M->eom;
   }
 } /* end of function print_bnd_sets1 */
 
diff --git a/src/ic3/u1til.cc b/src/ic3/u1til.cc
index 47ed70f97..0f39cc8da 100644
--- a/src/ic3/u1til.cc
+++ b/src/ic3/u1til.cc
@@ -16,7 +16,41 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include "ccircuit.hh"
 #include "m0ic3.hh"
 
+/*=================================
+
+      C V E C T _ T O _ S T R
+
+  =================================*/
+std::string cvect_to_str(CCUBE &A)
+{
+
+  std::string Res;
+
+  for (size_t i=0; i < A.size(); i++) {
+    if (i > 0) Res += " ";
+    Res += std::to_string(A[i]);
+  }
+
+  return(Res);
+} /* end of function cvect_to_str */
+
+/*=================================
+
+      I V E C T _ T O _ S T R
+
+  =================================*/
+std::string ivect_to_str(CUBE &A)
+{
+
+  std::string Res;
+
+  for (size_t i=0; i < A.size(); i++) {
+    if (i > 0) Res += " ";
+    Res += std::to_string(A[i]);
+  }
 
+  return(Res);
+} /* end of function ivect_to_str */
 
 /*=================================
 
@@ -111,46 +145,7 @@ bool CompInfo::update_fclause(int clause_ind,int tf_ind)
 
 
 
-/*==========================
-
-  R E A D _ N U M B E R S
-
-  =========================*/
-void read_numbers(char *buf,int &num1,int &num2)
-{
-  int pnt=0;
-
-  char loc_buf[MAX_NAME+1];
-
-  // read in the first number
-  int loc_pnt = 0;
-  while (true)
-    {char c = buf[pnt++];
-     if (c == ' ') break;
-     loc_buf[loc_pnt++] = c;
-    }
-
-  loc_buf[loc_pnt] = 0;
-  num1 = atoi(loc_buf);
 
-  // skip spaces
-  while (true)
-    {char c = buf[pnt];
-     if (c == ' ') pnt++;
-     else break;
-    }
-
-    // read in the second number
-  loc_pnt = 0;
-  while (true)
-    {char c = buf[pnt++];
-     if (c == ' ')  break;
-     if (c == '\n') break;
-     loc_buf[loc_pnt++] = c;
-    }
-loc_buf[loc_pnt] = 0;
- num2 = atoi(loc_buf);
-} /* end of function read_numbers */
 
 /*========================
 
@@ -161,7 +156,7 @@ void my_assert(bool cond)
 {
   if (!cond) {
     p();
-    exit(100);
+    throw(ERROR1);
   }
 } /* end of function my_assert */
 
diff --git a/src/ic3/v0erify.cc b/src/ic3/v0erify.cc
index 0119292b0..daa688dde 100644
--- a/src/ic3/v0erify.cc
+++ b/src/ic3/v0erify.cc
@@ -32,7 +32,7 @@ bool CompInfo::ver_trans_inv()
   if (!ok) return(false);
   ok = ver_invar(H,Old_nums);
   if (!ok) return(false);
-  printf("inductive invariant verification is ok\n");
+  M->result() << "inductive invariant verification is ok" << M->eom;
   return(true);
 } /* end of function ver_trans_inv */
 
@@ -44,7 +44,7 @@ bool CompInfo::ver_trans_inv()
 bool CompInfo::ver_invar(CNF &H,CUBE &Old_nums)
 {
 
-  std::string Name = "Gen_sat";
+  std::string Name("Gen_sat");
   init_sat_solver(Gen_sat,max_num_vars,Name);
 
   // add property
@@ -60,11 +60,11 @@ bool CompInfo::ver_invar(CNF &H,CUBE &Old_nums)
 
   bool sat_form = check_sat1(Gen_sat);
   if (sat_form) {
-    printf("bad state is reachable: ");
+    M->error() << "bad state is reachable: ";
     CUBE St,Nst,Pst;
     extr_cut_assgns1(Nst,Next_svars,Gen_sat);
     conv_to_pres_state(St,Nst);
-    std::cout << St << std::endl;
+    M->error() << ivect_to_str(St) << M->eom;
     return(false);
   }
   
@@ -91,14 +91,15 @@ bool CompInfo::ver_ind_clauses2(CNF &H,CUBE &Old_nums)
     add_negated_assumps1(Assmps,C);   
     bool sat_form = check_sat2(Gen_sat,Assmps);
     if (sat_form) {
-      printf("inductive invariant verification failed\n");
-      printf("Inv & T does not imply F'[%d]\n",Old_nums[i]);
-      printf("F[%d]-> ",Old_nums[i]); 
-      std::cout << H[i] << std::endl;
-      printf("F'[%d]-> ",Old_nums[i]); 
-      std::cout << C << std::endl;
+      M->error() << "inductive invariant verification failed" << M->eom;
+      M->error() << "Inv & T does not imply F'[" << Old_nums[i] << "]"
+		 << M->eom;
+      M->error() << "F[" << Old_nums[i] << "]-> "; 
+      M->error() << H[i] << M->eom;
+      M->error() << "F'[" << Old_nums[i] << "]-> ";
+      M->error() << C << M->eom;
       CUBE St0,St1;
-      print_bnd_sets1();    
+      print_bnd_sets1(messaget::M_ERROR);    
       return(false);
     }
   }
@@ -139,8 +140,8 @@ bool CompInfo::ver_prop()
 
   bool sat_form = check_sat1(Gen_sat);
   if (sat_form) {
-    printf("inductive invariant verification failed\n");
-    printf("Ist does not imply Prop\n");
+    M->error() << "inductive invariant verification failed" << M->eom;
+    M->error() << "Ist does not imply Prop" << M->eom;
     return(false);
   }
 
@@ -156,7 +157,7 @@ bool CompInfo::ver_prop()
 bool CompInfo::ver_ini_states(CNF &H)
 {
 
-  std::string Name = "Gen_sat";
+  std::string Name("Gen_sat");
   init_sat_solver(Gen_sat,max_num_vars,Name);
   
   accept_new_clauses(Gen_sat,Ist);  
@@ -203,9 +204,9 @@ bool CompInfo::ver_ind_clauses1(CNF &H)
    
     bool sat_form = check_sat2(Gen_sat,Assmps);
     if (sat_form) {
-      printf("inductive invariant verification failed\n");  
-      printf("clause F[%zu] excludes an initial state: ", i);
-      std::cout << H[i] << std::endl;
+      M->error() << "inductive invariant verification failed" << M->eom;
+      M->error() << "clause F[" << i << "] excludes an initial state: ";
+      M->error() << ivect_to_str(H[i]) << M->eom;
       return(false);
     }
   }
diff --git a/src/ic3/v1erify.cc b/src/ic3/v1erify.cc
index 64a8c31d0..0b44ea8f6 100644
--- a/src/ic3/v1erify.cc
+++ b/src/ic3/v1erify.cc
@@ -24,7 +24,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
    In contrast to 'gen_form1' this
    function returns array 'Old_nums'
-   specifying the indexes of clauses
+   specifying the indices of clauses
    of H in F.
 
   ===================================*/
@@ -54,10 +54,10 @@ bool CompInfo::ver_cex()
   assert(Cex.size() > 0);
 
   bool ok = check_init_state(Cex[0]);
-  printf("Cex.size() = %d\n",(int) Cex.size());
+  M->result() << "Cex.size() = " << Cex.size() << M->eom;
   if (!ok) return(false);
 
-  std::string Name = "Gen_sat";
+  std::string Name("Gen_sat");
   if (Cex.size() == 1) goto FINISH;
   
   init_sat_solver(Gen_sat,max_num_vars,Name);
@@ -66,8 +66,8 @@ bool CompInfo::ver_cex()
   for (size_t i=0; i < Cex.size()-1; i++) {
     bool ok = check_transition(Cex[i],Cex[i+1]);
     if (!ok) {
-      printf("verfication failed\n");
-      printf("wrong transition S%zu -> S%zu\n",i,i+1);
+      M->error() << "verfication failed" << M->eom;
+      M->error() << "wrong transition S" << i << "-> S" << i+1 << M->eom;
       return(false);
     }
   }
@@ -78,7 +78,7 @@ bool CompInfo::ver_cex()
   if (!ok) return(false);
 
  FINISH:
-  printf("cex verification is ok\n");
+  M->result() << "cex verification is ok" << M->eom;
   return(true);
 } /* end of function ver_cex */
 
@@ -91,7 +91,7 @@ bool CompInfo::ver_cex()
 bool CompInfo::check_bad_state(CUBE &St)
 {
 
-  std::string Name = "Gen_sat";
+  std::string Name("Gen_sat");
   init_sat_solver(Gen_sat,max_num_vars,Name);
   add_neg_prop(Gen_sat);
   add_constr_lits2(Gen_sat);
@@ -99,10 +99,10 @@ bool CompInfo::check_bad_state(CUBE &St)
   add_assumps1(Assmps,St);
   bool sat_form = check_sat2(Gen_sat,Assmps);
   if (sat_form == false) {
-    printf("cex verification failed\n");
-    printf("last state of Cex is a good one\n");
-    std::cout << "St-> " << St << std::endl;
-    printf("sat_form = %d\n",sat_form);
+    M->error() << "cex verification failed" << M->eom;
+    M->error() << "last state of Cex is a good one" << M->eom;
+    M->error() << "St-> " << ivect_to_str(St) << M->eom;;
+    M->error() << "sat_form = " << sat_form << M->eom;
     return(false); }
 
   delete_solver(Gen_sat);
@@ -140,7 +140,7 @@ bool CompInfo::check_transition(CUBE &St0,CUBE &St1)
 bool CompInfo::check_init_state(CUBE &St)
 {
 
-  std::string Name = "Gen_sat";
+  std::string Name("Gen_sat");
   init_sat_solver(Gen_sat,max_num_vars,Name);
 
   accept_new_clauses(Gen_sat,Ist);
@@ -150,8 +150,8 @@ bool CompInfo::check_init_state(CUBE &St)
   
   bool sat_form = check_sat2(Gen_sat,Assmps);
   if (sat_form == false) {
-    printf("cex verification failed\n");
-    printf("Cex starts with a non-initial state\n");
+    M->error() << "cex verification failed" << M->eom;
+    M->error() << "Cex starts with a non-initial state" << M->eom;
     return(false);
   }