made the required %d->%zu replacements

src/ic3/ebmc_ic3_interface.hh

@@ -43,6 +43,7 @@ public:
   void print_lit1(unsigned var,bool sign);
   void print_lit2(unsigned var,bool sign);
   void print_nodes();
+  void print_var_map();
   void form_orig_names();
   void form_neg_orig_name(CCUBE &Name,literalt &next_lit);
   bool form_orig_name(CCUBE &Name,literalt &lit,bool subtract = false);

src/ic3/m1ain.cc

@@ -79,8 +79,10 @@ int ic3_enginet::operator()()
   const1 = false;
   orig_names = false;
 
-
+  // print_nodes();
+  // print_var_map();
   read_ebmc_input();
+  //print_blif3("tst.blif",Ci.N);
   if (cmdline.isset("aiger")) {
     printf("converting to aiger format\n");
     Ci.print_aiger_format();

src/ic3/m4y_aiger_print.cc

@@ -176,8 +176,8 @@ void CompInfo::print_aiger_header(FILE *fp,int max_var,int num_gates)
   fprintf(fp,"aag ");
 
   fprintf(fp,"%d ",max_var); 
-  fprintf(fp,"%d ",N->ninputs);
-  fprintf(fp,"%d ",N->nlatches);
+  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");
@@ -220,9 +220,9 @@ void CompInfo::check_circuit(int &num_buffs,int &num_consts)
       cond |= (G.func_type == CONST);
       if (!cond)      {
         p();
-	printf("i = %d\n",i);
-	printf("N->Gate_list.size() = %d\n",(int) N->Gate_list.size());
-	printf("G.ninputs = %d\n",G.ninputs);
+	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);
       }
     }

src/ic3/r1ead_input.cc

@@ -58,6 +58,9 @@ 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;
 

src/ic3/r3ead_input.cc

@@ -205,11 +205,6 @@ void ic3_enginet::form_outp_buf(CDNF &Out_names)
   if (prop_l.is_constant() == 0)
     if (prop_l.sign()) 
        olit--;
-
-
-
-
-
 
   assert(Ci.Inps.find(olit) == Ci.Inps.end());
   bool latch = false;

src/ic3/r7ead_input.cc

@@ -23,6 +23,37 @@ Author: Eugene Goldberg, [email protected]
 #include <ebmc/ebmc_base.h>
 #include "ebmc_ic3_interface.hh"
 
+/*=====================================
+
+       P R I N T _ V A R _ M A P
+
+  =====================================*/
+void ic3_enginet::print_var_map()
+{
+
+
+  var_mapt &vm = netlist.var_map;
+
+  for(var_mapt::mapt::const_iterator it=vm.map.begin();
+      it!=vm.map.end(); it++)    {
+    const var_mapt::vart &var=it->second;
+    if (var.is_input()) printf("input: ");
+    else if (var.is_latch()) printf("latch: ");
+    else if (var.is_nondet()) printf("nondet: ");
+    else if (var.is_wire()) printf("wire:" );
+    else assert(false);
+
+    for (size_t j=0; j < var.bits.size(); j++) {
+      if (j > 0) printf(", ");
+      literalt lit =var.bits[j].current;
+      unsigned lit_val = lit.get();
+      printf("[%zu] = %u",j,lit_val);
+    }
+    printf("\n");
+  }
+
+
+} /* end of function print_var_map */
 /*=========================================
 
         A D D _ P S E U D O _ I N P S