From 2d1ca87147b659493c683782812e5ceec681df97 Mon Sep 17 00:00:00 2001
From: eigold <eu.goldberg@gmail.com>
Date: Mon, 5 Jun 2017 09:17:13 -0400
Subject: [PATCH] made the required %d->%zu replacements

---
 src/ic3/ebmc_ic3_interface.hh |  1 +
 src/ic3/m1ain.cc              |  4 +++-
 src/ic3/m4y_aiger_print.cc    | 10 +++++-----
 src/ic3/r1ead_input.cc        |  3 +++
 src/ic3/r3ead_input.cc        |  5 -----
 src/ic3/r7ead_input.cc        | 31 +++++++++++++++++++++++++++++++
 6 files changed, 43 insertions(+), 11 deletions(-)

diff --git a/src/ic3/ebmc_ic3_interface.hh b/src/ic3/ebmc_ic3_interface.hh
index 9fb97e8e0..ec48ef74a 100644
--- a/src/ic3/ebmc_ic3_interface.hh
+++ b/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);
diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc
index d37334d08..1b6086748 100644
--- a/src/ic3/m1ain.cc
+++ b/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();
diff --git a/src/ic3/m4y_aiger_print.cc b/src/ic3/m4y_aiger_print.cc
index 57ca654fe..be2b2f660 100644
--- a/src/ic3/m4y_aiger_print.cc
+++ b/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);
       }
     }
diff --git a/src/ic3/r1ead_input.cc b/src/ic3/r1ead_input.cc
index c604c29e0..39b2b9b02 100644
--- a/src/ic3/r1ead_input.cc
+++ b/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;
   
diff --git a/src/ic3/r3ead_input.cc b/src/ic3/r3ead_input.cc
index 47280a929..5d08150e8 100644
--- a/src/ic3/r3ead_input.cc
+++ b/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;
diff --git a/src/ic3/r7ead_input.cc b/src/ic3/r7ead_input.cc
index 706293268..e131d1263 100644
--- a/src/ic3/r7ead_input.cc
+++ b/src/ic3/r7ead_input.cc
@@ -23,6 +23,37 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #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