diff --git a/regression/ebmc/ic3/exmp1/test.desc b/regression/ebmc/ic3/exmp1/test.desc
index 5b1c18842..dce1ecb36 100644
--- a/regression/ebmc/ic3/exmp1/test.desc
+++ b/regression/ebmc/ic3/exmp1/test.desc
@@ -2,6 +2,6 @@ CORE
 pdtvispeterson.sv
 --ic3
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp2/test.desc b/regression/ebmc/ic3/exmp2/test.desc
index 6a9e58e91..6fbd5915a 100644
--- a/regression/ebmc/ic3/exmp2/test.desc
+++ b/regression/ebmc/ic3/exmp2/test.desc
@@ -2,6 +2,6 @@ CORE
 bobcount.sv
 --ic3
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp3/test.desc b/regression/ebmc/ic3/exmp3/test.desc
index be741a611..c0d5ce9d8 100644
--- a/regression/ebmc/ic3/exmp3/test.desc
+++ b/regression/ebmc/ic3/exmp3/test.desc
@@ -2,6 +2,6 @@ CORE
 viseisenberg.sv
 --ic3
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp4/test.desc b/regression/ebmc/ic3/exmp4/test.desc
index f3efd98e9..5eabfd3f1 100644
--- a/regression/ebmc/ic3/exmp4/test.desc
+++ b/regression/ebmc/ic3/exmp4/test.desc
@@ -2,6 +2,6 @@ CORE
 visbakery.sv
 --ic3
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp5/test.desc b/regression/ebmc/ic3/exmp5/test.desc
index f78158b8e..6802810bd 100644
--- a/regression/ebmc/ic3/exmp5/test.desc
+++ b/regression/ebmc/ic3/exmp5/test.desc
@@ -2,6 +2,6 @@ CORE
 ringp0.sv
 --ic3
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp6/test.desc b/regression/ebmc/ic3/exmp6/test.desc
index 0c98ae529..3e54ad980 100644
--- a/regression/ebmc/ic3/exmp6/test.desc
+++ b/regression/ebmc/ic3/exmp6/test.desc
@@ -2,6 +2,6 @@ CORE
 eijks208o.sv
 --ic3
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp7/test.desc b/regression/ebmc/ic3/exmp7/test.desc
index 7b5cb874e..7934594c4 100644
--- a/regression/ebmc/ic3/exmp7/test.desc
+++ b/regression/ebmc/ic3/exmp7/test.desc
@@ -1,7 +1,7 @@
 CORE
 bobmiterbm1multi.sv
---ic3 --prop 1032
+--ic3 --property bobmiterbm1multi.property.1033
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp8/test.desc b/regression/ebmc/ic3/exmp8/test.desc
index 960ae2f44..65d962e4b 100644
--- a/regression/ebmc/ic3/exmp8/test.desc
+++ b/regression/ebmc/ic3/exmp8/test.desc
@@ -1,7 +1,7 @@
 CORE
 bobmiterbm1multi.sv
---ic3 --prop 1079
+--ic3 --property bobmiterbm1multi.property.1080
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp9/test.desc b/regression/ebmc/ic3/exmp9/test.desc
index 56fcdb081..cf94b9c03 100644
--- a/regression/ebmc/ic3/exmp9/test.desc
+++ b/regression/ebmc/ic3/exmp9/test.desc
@@ -1,7 +1,7 @@
 CORE
 sm98a7multi.sv
---ic3 --prop 1 --constr
+--ic3 --property sm98a7multi.property.2 --constr
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/non_inductive1/test.desc b/regression/ebmc/ic3/non_inductive1/test.desc
index a289ecd21..6a37b38ca 100644
--- a/regression/ebmc/ic3/non_inductive1/test.desc
+++ b/regression/ebmc/ic3/non_inductive1/test.desc
@@ -1,6 +1,7 @@
 CORE
 non_inductive.sv
---ic3 --prop 0
+--ic3 --property main.property.p0
 ^property HOLDS$
-^verification is ok
+^inductive invariant verification is ok
 --
+^inductive invariant verification failed
diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
index efe425b8b..719aa85b7 100644
--- a/src/ebmc/Makefile
+++ b/src/ebmc/Makefile
@@ -9,7 +9,7 @@ SRC = diameter.cpp main.cpp diatest.cpp show_properties.cpp \
 OBJ+= $(CBMC)/src/util/util$(LIBEXT) \
       $(CBMC)/src/langapi/langapi$(LIBEXT) \
       $(CBMC)/src/ansi-c/string_constant$(OBJEXT) \
-      $(CBMC)/src/ansi-c/c_types$(OBJEXT) \
+      $(CBMC)/src/util/c_types$(OBJEXT) \
       $(CBMC)/src/solvers/solvers$(LIBEXT) \
       $(CBMC)/src/big-int/big-int$(LIBEXT) \
       ../trans-netlist/trans-netlist$(LIBEXT) \
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index fb88c8d13..eb81aeb26 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -262,8 +262,12 @@ void ebmc_parse_optionst::help()
     " --k-induction                     do k-induction with k=bound\n"
     " --bdd                             use (unbounded) BDD engine\n"
     " --ic3 [options]                   use IC3 engine with options described below\n"
-    "       --prop <nr>                   check property number <nr>\n"
-    "       --constr                      use constraints specified in 'file.cnstr'\n"
+    "       --property <nm>                  check property named <nm>\n"
+    "       --constr                         use constraints specified in 'file.cnstr'\n"
+    "       --h                              print out help information\n"
+    "       --new-mode                       new mode is switched on\n"
+    "       --aiger                          print out the instance in aiger format\n"
+    
     //" --interpolation                   use bit-level interpolants\n"
     //" --interpolation-word              use word-level interpolants\n"
     //" --diameter                        perform recurrence diameter test\n"
diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h
index dfd3123d5..12b5da456 100644
--- a/src/ebmc/ebmc_parse_options.h
+++ b/src/ebmc/ebmc_parse_options.h
@@ -32,7 +32,7 @@ class ebmc_parse_optionst:public parse_options_baset
     "(reset):"
     "(version)(verilog-rtl)(verilog-netlist)"
     "(compute-interpolant)(interpolation)(interpolation-vmcai)"
-    "(ic3)(prop):(constr)(h)"
+    "(ic3)(property):(constr)(h)(new-mode)(aiger)"
     "(interpolation-word)(interpolator):(bdd)"
     "(smt1)(smt2)(boolector)(z3)(cvc4)(yices)(mathsat)(prover)(lifter)"
     "(aig)(stop-induction)(stop-minimize)(start):(coverage)(naive)"
diff --git a/src/hw-cbmc/hw_cbmc_parse_options.cpp b/src/hw-cbmc/hw_cbmc_parse_options.cpp
index 3f1c9102d..7ae05c7d7 100644
--- a/src/hw-cbmc/hw_cbmc_parse_options.cpp
+++ b/src/hw-cbmc/hw_cbmc_parse_options.cpp
@@ -250,6 +250,9 @@ Function: hw_cbmc_parse_optionst::help
 
 void hw_cbmc_parse_optionst::help()
 {
+  std::cout <<
+    "* *  hw-cbmc is protected in part by U.S. patent 7,225,417  * *";
+
   cbmc_parse_optionst::help();
 
   std::cout <<
diff --git a/src/ic3/Makefile b/src/ic3/Makefile
index 04a541e89..4e637cc5f 100644
--- a/src/ic3/Makefile
+++ b/src/ic3/Makefile
@@ -30,7 +30,8 @@ SEQ_CIRC = $(OBJ_DIR)/p1rint_blif.o $(OBJ_DIR)/p2rint_blif.o $(OBJ_DIR)/finish_g
            $(OBJ_DIR)/circuit.o $(OBJ_DIR)/a4dd_spec_buffs.o  $(OBJ_DIR)/a5dd_spec_buffs.o  \
            $(OBJ_DIR)/l0ast_touch.o $(OBJ_DIR)/l1ast_touch.o 
      
-OBJ_ROOT = $(OBJ_DIR)/r7ead_input.o $(OBJ_DIR)/r6ead_input.o  \
+OBJ_ROOT = $(OBJ_DIR)/m5y_aiger_print.o \
+           $(OBJ_DIR)/m4y_aiger_print.o  $(OBJ_DIR)/r7ead_input.o $(OBJ_DIR)/r6ead_input.o  \
            $(OBJ_DIR)/g2ate_ord.o $(OBJ_DIR)/i4nit_sat_solvers.o $(OBJ_DIR)/l1ift_states.o \
            $(OBJ_DIR)/r5ead_input.o  $(OBJ_DIR)/r4ead_input.o $(OBJ_DIR)/c4oi.o \
            $(OBJ_DIR)/c5tg.o $(OBJ_DIR)/c2tg.o $(OBJ_DIR)/r3ead_input.o \
diff --git a/src/ic3/README b/src/ic3/README
index 26cb931fa..4ae33869f 100644
--- a/src/ic3/README
+++ b/src/ic3/README
@@ -2,12 +2,8 @@
    a variation of Aaron Bradley's IC3.  It is incorporated into
    ebmc. To invoke IC3, run
 
-   ebmc verilog_file --ic3
+   ebmc verilog_file --ic3 [options]
 
-*) Integration is not over yet. This current version is missing two
-   features that has been implemented in the stand-alone version.
-   The current version assumes that the input verilog file specifies
-   only one property and has no constraints.
 
 
   
diff --git a/src/ic3/aux_types.hh b/src/ic3/aux_types.hh
index 7cf160a6e..1b781ed03 100644
--- a/src/ic3/aux_types.hh
+++ b/src/ic3/aux_types.hh
@@ -98,27 +98,39 @@ struct OblTableElem {
 typedef std::vector <OblTableElem> OblTable;
 
 
+
 //
 //  PrQueue
 //
 struct PqElem {
-  int tf_ind; // time frame index
+  int tf_ind; // time frame index, the same value as in OblTableElem
+  int dist; //  the same value as in OblTableElem
   int tbl_ind; // index of this element in 'Obl_table'
+  int sort_mode; // specifies the sorting mode
 };
 
 
-class pq_compare
-{
+class pq_compare {
 public:
   bool operator() (PqElem &A, PqElem &B)
   {
-    return (A.tf_ind  > B.tf_ind);
+    if (A.tf_ind  > B.tf_ind) return(true);
+    if (A.tf_ind  < B.tf_ind) return(false);
+    if (A.dist > B.dist) return(true);
+    if (A.sort_mode == 0) return(false);
+    if (A.sort_mode == 1) {
+      if (A.tbl_ind > B.tbl_ind) return(true);
+      else return(false);}
+    assert(A.sort_mode == 2);
+    if (A.tbl_ind < B.tbl_ind) return(true);
+    else return(false);
   }
 };
 
 typedef std::priority_queue<PqElem,std::vector <PqElem>, pq_compare> PrQueue;
 
 
+
 //
 //   ClauseInfo
 //
@@ -172,7 +184,10 @@ struct TimeFrame
 
   int num_rcnt_ctis; // number of Cti-s generated in the current time frame 
                      // when processing the latest time frame
-  
+
+  int num_seen_cls; // number of new cti or ctg clauses that are already in formula F
+  int num_redund_cls; // number of new cti/ctg clauses that are already in formula F
+                      // and cannot be added to any time frame
  
 };
 
diff --git a/src/ic3/build_prob/g0en_cnf.cc b/src/ic3/build_prob/g0en_cnf.cc
index 47066943f..e6ad322b0 100755
--- a/src/ic3/build_prob/g0en_cnf.cc
+++ b/src/ic3/build_prob/g0en_cnf.cc
@@ -86,8 +86,8 @@ void CompInfo::gen_out_fun(DNF &H,int shift,bool short_version)
     if (G.gate_type == INPUT) continue;
     if (G.gate_type == LATCH) continue;
 // skip the gates that are not part of the output function
-    if (G.flags.output_function == 0) 
-      if (G.flags.fun_constr == 0) continue; 
+    if (G.flags.output_function == 0)
+       if ((G.flags.fun_constr == 0) && (G.flags.tran_constr == 0)) 
     if (short_version)
 // skip the gates that are shared by transition relation and out function
       if (G.flags.transition) continue; 
diff --git a/src/ic3/build_prob/g2en_cnf.cc b/src/ic3/build_prob/g2en_cnf.cc
index 5ba8c75b9..fcc3f7c47 100644
--- a/src/ic3/build_prob/g2en_cnf.cc
+++ b/src/ic3/build_prob/g2en_cnf.cc
@@ -202,7 +202,9 @@ void CompInfo::set_constr_flag()
     bool tran_flag,fun_flag;
 
     gen_constr_coi(Gates,tran_flag,fun_flag,Stack);
-    assert(tran_flag || fun_flag);
+    tran_flag = true;
+    fun_flag = true;  
+  
     mark_constr_gates(Gates,tran_flag,fun_flag);
     if (tran_flag) Constr_gates[gate_ind].tran_coi = 1;
     else Constr_gates[gate_ind].tran_coi = 0;
diff --git a/src/ic3/build_prob/g3en_cnf.cc b/src/ic3/build_prob/g3en_cnf.cc
index 9585ef1ae..159c4ac1c 100644
--- a/src/ic3/build_prob/g3en_cnf.cc
+++ b/src/ic3/build_prob/g3en_cnf.cc
@@ -66,10 +66,10 @@ void CompInfo::gen_constr_coi(CUBE &Gates,bool &tran_flag,bool &fun_flag,
       fun_flag = true;
       skip = true;
     }
-    if (G.flags.transition > 0) {
+
+    if (G.flags.transition > 0) 
       tran_flag = true;
-      skip = true;
-    }
+     
     if (skip) continue;
     Gates.push_back(gate_ind);    
 
diff --git a/src/ic3/c0ex.cc b/src/ic3/c0ex.cc
index 0bb080017..de94ba292 100644
--- a/src/ic3/c0ex.cc
+++ b/src/ic3/c0ex.cc
@@ -59,6 +59,9 @@ bool CompInfo::check_one_state_cex()
 
   add_bad_states(Gen_sat);
 
+  // add constraints
+  accept_constrs(Gen_sat);
+
 
   bool sat_form = check_sat1(Gen_sat);
   bool ok = true;
@@ -157,13 +160,34 @@ void CompInfo::add_neg_prop(SatSolver &Slvr)
   accept_new_clause(Slvr,C);
 } /* end of function add_neg_prop */
 
-/*=====================================
+/*==================================
 
-  A D D _ B A D _ S T A T E S
+    A D D _ B A D _ S T A T E S
 
-  ====================================*/
+  ================================*/
 void CompInfo::add_bad_states(SatSolver &Slvr)
 {
   add_neg_prop(Slvr);
 
 } /* end of function add_bad_states */
+
+/*===================================
+
+    A C C E P T _ C O N S T R S
+
+ ==================================*/
+void CompInfo::accept_constrs(SatSolver &Slvr)
+{
+  for (size_t i=0; i < Constr_ilits.size(); i++) {
+    CLAUSE U;
+    U.push_back(Constr_ilits[i]);
+    accept_new_clause(Slvr,U);
+  }
+
+  SCUBE::iterator pnt;
+  for (pnt = Constr_nilits.begin(); pnt != Constr_nilits.end(); pnt++) {
+    CLAUSE U;
+    U.push_back(*pnt);
+    accept_new_clause(Slvr,U);
+  }
+} /* end of function add_bad_states */
diff --git a/src/ic3/c2tg.cc b/src/ic3/c2tg.cc
index a85b210a6..db890f8d0 100644
--- a/src/ic3/c2tg.cc
+++ b/src/ic3/c2tg.cc
@@ -78,3 +78,21 @@ int CompInfo::latest_succ_tf_ind(int tf_ind,CLAUSE &C)
 
   return(tf_lind);
 } /* end of function latest_succ_tf_ind */
+
+/*=======================================
+
+         F O R M _ N X T _ C U B E
+
+  =====================================*/
+void CompInfo::form_nxt_cube(CUBE &Nxt_cube,CLAUSE &C)
+{
+
+  for (size_t i=0;i < C.size(); i++) {
+    int var_ind = abs(C[i])-1;
+    int nxt_var_ind = Pres_to_next[var_ind];
+    assert(nxt_var_ind >=0);
+    int lit = (C[i] > 0)?-(nxt_var_ind+1):(nxt_var_ind+1);
+    Nxt_cube.push_back(lit);
+  }
+
+} /* end of function form_nxt_cube */
diff --git a/src/ic3/c5tg.cc b/src/ic3/c5tg.cc
index 599c8c7a4..1db309f4b 100644
--- a/src/ic3/c5tg.cc
+++ b/src/ic3/c5tg.cc
@@ -81,8 +81,11 @@ void CompInfo::lift_ctg_state(CUBE &Ctg_cube,CUBE &Ctg_st,CUBE &Inps,
   add_assumps1(Assmps,Inps);
   
 
-  Mlit act_lit;  
-  add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube);
+  Mlit act_lit;
+  if (standard_mode) 
+    add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube,false);
+  else
+    add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube,true);
  
   Assmps.push(act_lit);
   add_assumps2(Assmps,Ctg_st);
diff --git a/src/ic3/e1xclude_state.cc b/src/ic3/e1xclude_state.cc
index 05fb3417a..697746d60 100644
--- a/src/ic3/e1xclude_state.cc
+++ b/src/ic3/e1xclude_state.cc
@@ -44,35 +44,34 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0)
       printf("Pr_queue.size() = %d\n",(int) Pr_queue.size());
     }
 
-    int obl_tf = Pr_queue.top().tf_ind;
+    int curr_tf = Pr_queue.top().tf_ind;
     int tbl_ind = Pr_queue.top().tbl_ind;
     
     if (verbose > 1)
-      printf("obl_tf = %d, tbl_ind = %d, min_tf = %d\n",obl_tf,tbl_ind, min_tf);
+      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;
 
 
-    if (obl_tf == 0) 
+    if (curr_tf == 0) 
       if (cont_init_states(St_cube)) return;
 
     int dist = Obl_table[tbl_ind].dist;
     int st_ind = tf_lind + 1 - dist;
-
-    curr_tf = obl_tf;
+    
     int succ_ind = Obl_table[tbl_ind].succ_ind;
-
-    bool ok = oblig_is_active(obl_tf+1,St_cube);
+  
+    bool ok = oblig_is_active(curr_tf+1,St_cube);
 
     if (!ok) {
       if (st_descr == OLD_STATE) triv_old_st_cnt++;
       Pr_queue.pop();     
-      if (succ_ind < 0) form_res_cnf(G,obl_tf+1,St_cube);
+      if (succ_ind < 0) form_res_cnf(G,curr_tf+1,St_cube);
       continue;}
 
    
-    if (obl_tf < min_tf) min_tf = obl_tf;
+    if (curr_tf < min_tf) min_tf = curr_tf;
 
     
    
@@ -87,21 +86,30 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0)
 	std::cout  << C << std::endl;
       }
 
- 
-      if (obl_tf + 2 < tf_lind + 1) {
-	CUBE Inps = Obl_table[tbl_ind].Inp_assgn;
-	add_new_elem(St_cube,Inps,obl_tf+2,dist,succ_ind,OLD_STATE);
+      if (succ_ind == -1) 
+	G.push_back(C);
+            
+  // the set of obligations is not empty yet
+      
+      int tf_ind1 = curr_tf+1;
+
+      if (standard_mode)
+	tf_ind1 = push_on_the_fly(curr_tf+1,C,st_descr);
+
+      add_fclause1(C,tf_ind1,st_descr);
+
+      if (standard_mode) {
+	if (tf_ind1 <= tf_lind) {
+	  CUBE Inps = Obl_table[tbl_ind].Inp_assgn;
+	  add_new_elem(St_cube,Inps,tf_ind1,dist,succ_ind,OLD_STATE);
+	}
       }
+      else
+	if (tf_ind1 < tf_lind) {
+	  CUBE Inps = Obl_table[tbl_ind].Inp_assgn;
+	  add_new_elem(St_cube,Inps,tf_ind1+1,dist,succ_ind,OLD_STATE);
+	}
      
-      
-      if (succ_ind == -1) {
-	G.push_back(C);
-	add_fclause1(C,curr_tf+1,st_descr);	 
-	continue;
-      } 
-	 
-      // the set of obligations is not empty yet      
-      add_fclause1(C,curr_tf+1,st_descr);
       continue;
     }
     
diff --git a/src/ic3/e2xclude_state.cc b/src/ic3/e2xclude_state.cc
index edc90188a..ae2639a2a 100644
--- a/src/ic3/e2xclude_state.cc
+++ b/src/ic3/e2xclude_state.cc
@@ -69,6 +69,7 @@ bool CompInfo::find_ind_subclause_cti(CLAUSE &C,SatSolver &Slvr,
     }
 
     // inductive clause is not found yet
+    if (standard_mode) return(false);
     CUBE St;
     extr_cut_assgns1(St,Pres_svars,Slvr);
 
@@ -151,7 +152,7 @@ void CompInfo::adjust_clause1(CLAUSE &C,CUBE &St)
     printf("%*c",9,' ');
     printf("expand_clause\n");
   }
-  htable_lits.change_marker(); // increment or reset the hash table marker 
+  htable_lits.change_marker(); 
   htable_lits.started_using();
 
   int marker = htable_lits.marker;
diff --git a/src/ic3/e3xclude_state.cc b/src/ic3/e3xclude_state.cc
index 64da1ef54..11c2b3237 100644
--- a/src/ic3/e3xclude_state.cc
+++ b/src/ic3/e3xclude_state.cc
@@ -32,7 +32,6 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf,
   }
 
 
-  SatSolver &Slvr = Time_frames[curr_tf].Slvr; 
   int impr_count = 0;
   C = C0;
   if (C.size() == 1) return;
@@ -46,12 +45,13 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf,
   if (C0.size()  < max_tries) 
     max_tries = C0.size();
   size_t num_tries = 0;
-
+  size_t loc_failed = 0;
+  
   while (true) {
     if (num_tries > max_tries) 
       return;
     
-    if (Curr.size() <= Tried.size())
+    if (Curr.size() <= loc_failed)
       return;
 
     int lit = pick_lit_to_remove(Curr,Tried,curr_tf);
@@ -65,27 +65,23 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf,
     if (!ok) {
       Curr.push_back(lit);
       num_tries++;
+      loc_failed++;
       if (ctg_flag) Failed_lits.insert(lit);
       continue;
     }
        
 
     CLAUSE C1;
-    if ((ctg_flag == false) || (curr_tf == 0)) {  
-      if (grl_heur == NO_JOINS)
-	ok = triv_ind_cls_proc(C1,Curr,curr_tf);
-      else {
-	assert(grl_heur == WITH_JOINS);
-	ok = find_ind_subclause_cti(C1,Slvr,Curr,st_descr);
-      }
-    }
+    if ((ctg_flag == false) || (curr_tf == 0)) 
+      ok = triv_ind_cls_proc(C1,Curr,curr_tf);
     else 
       ok =  find_ind_subclause_ctg(C1,curr_tf,Curr,st_descr,
-                 rec_depth,Failed_lits);
+				   rec_depth,Failed_lits);
  
 
     if (!ok) {
       failed_impr++;
+      loc_failed++;
       if (ctg_flag) Failed_lits.insert(lit);
       Curr.push_back(lit);
       num_tries++;
@@ -99,6 +95,10 @@ void CompInfo::incr_short(CLAUSE &C,CLAUSE &C0,int curr_tf,
     if (C.size() == 1) return;
     Curr = C1;
     num_tries = 0;
+    if (!standard_mode) {
+      Tried.clear();
+      loc_failed = 0;
+    }
     Tried.clear();
     if (C1.size() < max_tries) max_tries = C1.size();
   }
diff --git a/src/ic3/e4xclude_state.cc b/src/ic3/e4xclude_state.cc
index 66464c41f..ee84b0f1d 100644
--- a/src/ic3/e4xclude_state.cc
+++ b/src/ic3/e4xclude_state.cc
@@ -119,7 +119,7 @@ bool CompInfo::cont_init_states(CUBE &St_cube) {
 bool CompInfo::oblig_is_active(int tf_ind,CUBE &St_cube)
 {
 
-  if (tf_ind >  tf_lind) return(false);
+  if ((size_t) tf_ind >= Time_frames.size()) return(false);
 
   SatSolver &Slvr = Time_frames[tf_ind].Slvr;
 
@@ -163,6 +163,9 @@ void CompInfo::add_new_elem(CUBE &St_cube,CUBE &Inp_assgn,
   PqElem El1;
   El1.tf_ind = tf_ind;
   El1.tbl_ind = Obl_table.size()-1;
+  El1.dist = dist;
+  El1.sort_mode = 1;
+  
   Pr_queue.push(El1);
 
 } /* end of function add_new_elem */
diff --git a/src/ic3/e5xclude_state.cc b/src/ic3/e5xclude_state.cc
index edf7f2cf6..875160118 100644
--- a/src/ic3/e5xclude_state.cc
+++ b/src/ic3/e5xclude_state.cc
@@ -159,12 +159,13 @@ bool CompInfo::find_ind_subclause_ctg(CLAUSE &C,int curr_tf,CLAUSE &C0,
     release_lit(Slvr,~act_lit);
 
     CUBE Ctg_cube;
-  
     bool succ;
-    if ((ctg_cnt < max_ctg_cnt) && (rec_depth < max_rec_depth))    {
-      CUBE Nxt_cube;
-      use_coi_to_drop_svars(Nxt_cube,Nxt_st,tf_lind-curr_tf-1);
-      lift_ctg_state(Ctg_cube,Ctg_st,Inps,Nxt_cube);
+    CUBE Nxt_cube;
+    form_nxt_cube(Nxt_cube,C);
+  
+    lift_ctg_state(Ctg_cube,Ctg_st,Inps,Nxt_cube);
+    bool cond = (ctg_cnt < max_ctg_cnt) && (rec_depth < max_rec_depth);
+    if (cond && (curr_tf > 1))    { 
       ctg_cnt++;
       tot_ctg_cnt++;
       succ = exclude_ctg(Ctg_cube,curr_tf,rec_depth);
@@ -173,7 +174,7 @@ bool CompInfo::find_ind_subclause_ctg(CLAUSE &C,int curr_tf,CLAUSE &C0,
 	continue;
       }
     }
-    // else Ctg_cube = Ctg_st;
+   
 
     bool ok;
     ok = adjust_clause2(C,Ctg_cube,Failed_lits);
diff --git a/src/ic3/ebmc_ic3_interface.hh b/src/ic3/ebmc_ic3_interface.hh
index e082a56d9..11169996b 100644
--- a/src/ic3/ebmc_ic3_interface.hh
+++ b/src/ic3/ebmc_ic3_interface.hh
@@ -1,5 +1,6 @@
 typedef std::vector<std::string> GateNames;
 typedef std::map<int,int> LatchVal;
+typedef std::map<int,int> NondetVars;
 //
 class ic3_enginet:public ebmc_baset
 {
@@ -15,6 +16,7 @@ public:
   GateNames Gn;
   literalt prop_l;
   LatchVal Latch_val;
+  NondetVars Nondet_vars;
   bool const0,const1;
   bool orig_names;
 
@@ -41,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(std::ostream &out);
   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);
@@ -54,7 +57,11 @@ public:
   void form_init_constr_lits();
   void store_constraints(const std::string &fname);
   void read_constraints(const std::string &fname);
-
+  void add_pseudo_inps(Circuit *N);
+  void print_lit(std::ostream& out,literalt a);
+  std::string print_string(const irep_idt &id);
+  void add_verilog_conv_constrs();
+  
 protected:
   netlistt netlist;
  
diff --git a/src/ic3/l0ift_states.cc b/src/ic3/l0ift_states.cc
index 517c78150..fafe53a1e 100644
--- a/src/ic3/l0ift_states.cc
+++ b/src/ic3/l0ift_states.cc
@@ -42,7 +42,7 @@ void CompInfo::lift_good_state(CUBE &Gst_cube,CUBE &Prs_st,
   
   
   Mlit act_lit;  
-  add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube);
+  add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube,true);
  
   Assmps.push(act_lit);
 
@@ -139,7 +139,8 @@ void CompInfo::gen_state_cube(CUBE &St_cube,CUBE &St,SatSolver &Slvr)
   A D D _ C L S _ E X C L _ S T _ C U B E
 
   ===========================================*/
-void CompInfo::add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St)
+void CompInfo::add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St,
+				    bool add_cnstr_lits)
 {
   CLAUSE C;
   act_lit = IctMinisat::mkLit(Slvr.Mst->newVar(),false);
@@ -155,12 +156,17 @@ void CompInfo::add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St)
  
   // add literals constraining internal variables
 
-  for (size_t i=0; i < Tr_coi_lits.size(); i++) {
-    int lit = Tr_coi_lits[i];
-    int var_ind = abs(lit)-1;
-    assert (Var_info[var_ind].type == INTERN);
-    C.push_back(-lit);
+  if (add_cnstr_lits) {
+    SCUBE::iterator pnt;
+    for (pnt = Constr_nilits.begin(); pnt != Constr_nilits.end(); pnt++) {
+      int lit = *pnt;
+      int var_ind = abs(lit)-1;
+      if (Var_info[var_ind].type != INTERN) continue;
+      C.push_back(-lit);
+    }
   }
+ 
+  
 
   accept_new_clause(Slvr,C);
   
diff --git a/src/ic3/m0ic3.hh b/src/ic3/m0ic3.hh
index f96ca7466..e6a31e385 100644
--- a/src/ic3/m0ic3.hh
+++ b/src/ic3/m0ic3.hh
@@ -23,8 +23,10 @@ public:
                  // generate CNF formulas. For every input gate and latch
                  // Ordering[i] == i
  
-  size_t prop_ind; // specifies the index of the property to be checked 
-                   // to be implemented for the integrated version
+  std::string prop_name; // specifies the name of the property to be checked 
+  bool const_true_prop; // if 'true', the property is a constant 'true'
+  bool const_false_prop; // if true, the property is a constant 'false'
+ 
    
   CUBE Gate_to_var; // gate_to_var[gate_ind] gives the variable assigned to 
                     // the output of gate 'gate_ind'
@@ -161,7 +163,10 @@ public:
   
 
  // --------------- Parameters controlling algorithm's behavior
- 
+
+  bool standard_mode; // if true, the algorithm simulates Bradley's version
+                      // of ic3 published in 2013
+  
   bool print_inv_flag; // if true, the invariant found by the program 
                        // (if any) is printed out
   char print_cex_flag; // 0 - counterexample (cex) is not printed out, 
@@ -260,6 +265,7 @@ public:
   void form_consts(Circuit *N);
   void form_constr_lits();
   void add_constrs();
+  void print_aiger_format();
 
 protected:
 
@@ -394,8 +400,8 @@ const int RAND_SORT = 3;
 const char OLD_STATE = 0;
 const char NEW_STATE = 1;
 const char ROOT_STATE = 2;
-const char PUSH_STATE = 3;
-const char CTG_STATE = 4;
+const char CTG_STATE = 3;
+const char PUSH_STATE = 4;
 const char UNKNOWN_STATE = 5;
 
 // values of 'grl_heur'
diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc
index e9b5bcb03..65e2ba3ea 100644
--- a/src/ic3/m1ain.cc
+++ b/src/ic3/m1ain.cc
@@ -79,8 +79,16 @@ int ic3_enginet::operator()()
   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());
 
diff --git a/src/ic3/m2ethods.hh b/src/ic3/m2ethods.hh
index e2c933630..0473f4504 100644
--- a/src/ic3/m2ethods.hh
+++ b/src/ic3/m2ethods.hh
@@ -9,7 +9,7 @@ void form_short_property();
 void form_bad_states();
 void form_bad_states0(CNF &Bstates);
 void exclude_state_cube(CNF &G,int &min_tf,CUBE &St,CUBE &Inps);
-void push_clauses_forward();
+void push_clauses_forward(bool triv_time_frame);
 void init_time_frame_solver(int tf_ind);
 void init_bst_sat_solver();
 void init_lbs_sat_solver();
@@ -128,7 +128,7 @@ bool check_sat2(SatSolver &Slvr,MvecLits &Assmps);
 void add_negated_assumps1(MvecLits &Assmps,CLAUSE &C);
 void add_negated_assumps2(MvecLits &Assmps,CLAUSE &C,bool sort);
 void gen_assump_clause(CLAUSE &C,SatSolver &Slvr,MvecLits &Assmps);
-void add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St);
+void add_cls_excl_st_cube(Mlit &act_lit,SatSolver &Slvr,CUBE &St,bool add_cnstr_lits);
 void add_temp_clause(Mlit &act_lit,SatSolver &Slvr,CLAUSE &C);
 void simplify_tf_solvers();
 void print_tf_assgns(int tf_ind);
@@ -185,7 +185,9 @@ void add_last_cube(DNF &F);
 void form_property_gates(CUBE &Gates);
 void print_files(char *root);
 int init_ind_cls();
-
+void form_nxt_cube(CUBE &Nxt_cube,CLAUSE &C);
+int push_on_the_fly(int last_ind,CLAUSE &C,char st_desc);
+void accept_constrs(SatSolver &Slvr);
 //
 //  form CNF formulas
 void add_or_gate_cubes(DNF &F,int gate_ind,int shift);
@@ -205,5 +207,19 @@ void gate_sort_inps_first();
 void gate_sort_outs_first();
 void rand_gate_order();
 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);
+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 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);
+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);
diff --git a/src/ic3/m4y_aiger_print.cc b/src/ic3/m4y_aiger_print.cc
new file mode 100644
index 000000000..be2b2f660
--- /dev/null
+++ b/src/ic3/m4y_aiger_print.cc
@@ -0,0 +1,231 @@
+/******************************************************
+
+Module: Printing circuit in text version of aiger format  
+        (Part 1)
+
+Author: Eugene Goldberg, eu.goldberg@gmail.com
+
+******************************************************/
+#include <queue>
+#include <set>
+#include <map>
+#include <algorithm>
+#include <iostream>
+
+#include <ebmc/ebmc_base.h>
+
+#include "minisat/core/Solver.h"
+#include "minisat/simp/SimpSolver.h"
+
+#include "dnf_io.hh"
+#include "ccircuit.hh"
+#include "m0ic3.hh"
+
+/*====================================
+
+ P R I N T _ A I G E R _ F O R M A T
+
+  ====================================*/
+void CompInfo::print_aiger_format()
+{
+
+  int num_consts;
+  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";
+
+  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);
+} /* end of function print_aiger_format */
+
+/*=======================================
+
+     F O R M _ A I G E R _ G A T E S
+
+  =======================================*/
+int CompInfo::form_aiger_gates(DNF &Gates)
+{
+
+  int ind = -1;
+  assert(N->Outputs.size() == 1);
+  size_t out_gate_ind = N->Outputs[0];
+  for (size_t i=0; i < N->Gate_list.size(); i++) {
+    Gate &G = N->Gate_list[i];
+    if (G.gate_type == INPUT) continue;
+    if (G.gate_type == LATCH) continue;
+    if (G.func_type == CONST) continue;
+    assert(G.ninputs <= 2);
+    if (i == out_gate_ind)
+      ind = Gates.size();
+    if (G.func_type == AND) {
+       add_aiger_and_gate(Gates,i);
+       continue;
+    }
+    assert(G.func_type == BUFFER);
+    add_aiger_buffer(Gates,i);
+  }
+  assert(ind >= 0);
+  return(ind);
+
+} /* end of function form_aiger_gates */
+/*=================================
+
+    F I N D _ A I G E R _ L I T 1
+
+  ================================*/
+int CompInfo::find_aiger_lit1(int gate_ind,char polarity)
+{
+
+  Gate &G = N->get_gate(gate_ind);
+
+  if (G.func_type == CONST) {
+    if (G.F.size() > 0) return(1);
+    else {
+      assert(F.size() == 0);
+      return(0);
+    }
+  }
+
+  int lit = (gate_ind+1) << 1;
+  if (polarity) return(lit+1);
+  else return(lit);
+
+} /* end of function find_aiger_lit1 */
+
+/*=================================
+
+    F I N D _ A I G E R _ L I T 2
+
+  ================================*/
+int CompInfo::find_aiger_lit2(int gate_ind,char polarity)
+{
+
+
+  int lit = (gate_ind+1) << 1;
+  if (polarity) return(lit+1);
+  else return(lit);
+
+} /* end of function find_aiger_lit2 */
+
+/*========================================
+
+    P R I N T _ A I G E R _ L A T C H E S
+
+  ======================================*/
+void CompInfo::print_aiger_latches(FILE *fp)
+{
+
+  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);
+    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);
+    if (G.init_value == 2) {
+      fprintf(fp,"%d\n",lit);
+      continue;}
+    assert((G.init_value == 0) || (G.init_value == 1));
+    fprintf(fp,"%d\n",G.init_value);
+  }
+
+} /* end of function print_aiger_latches */
+
+
+/*========================================
+
+    P R I N T _ A I G E R _ I N P S
+
+  ======================================*/
+void CompInfo::print_aiger_inps(FILE *fp)
+{
+
+  for (size_t i=0; i < N->Inputs.size(); i++) {
+    int gate_ind = N->Inputs[i];
+    fprintf(fp,"%d\n",(gate_ind+1)<<1);
+  }
+
+} /* end of function print_aiger_inps */
+
+
+/*========================================
+
+    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)
+{
+
+  fprintf(fp,"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());
+} /* end of function print_aiger_header*/
+
+
+
+
+/*==============================
+
+    C H E C K _ C I R C U I T
+
+  ===============================*/
+void CompInfo::check_circuit(int &num_buffs,int &num_consts)
+{
+
+  num_consts = 0;
+  num_buffs = 0;
+  for (size_t i=0; i < N->Gate_list.size(); i++) {
+    Gate &G = N->Gate_list[i];
+    if (G.gate_type == INPUT) continue;
+    if (G.gate_type == LATCH) continue;
+    assert(G.gate_type == GATE);
+    bool cond = (G.func_type == AND);
+    cond |= (G.func_type == BUFFER);
+    cond |= (G.func_type == CONST);
+    if (!cond) {
+      p();
+      print_func_type(G);
+      exit(100);
+    } 
+
+    if (G.func_type == CONST) num_consts++;
+    if (G.func_type == BUFFER) num_buffs++;
+    
+    if (G.ninputs != 2) {
+      bool cond = (i == N->Gate_list.size()-2);
+      cond |= (G.func_type == BUFFER);
+      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);
+      }
+    }
+  }
+  
+} /* end of function check_circuit */
diff --git a/src/ic3/m5y_aiger_print.cc b/src/ic3/m5y_aiger_print.cc
new file mode 100644
index 000000000..1387f7cef
--- /dev/null
+++ b/src/ic3/m5y_aiger_print.cc
@@ -0,0 +1,190 @@
+/******************************************************
+
+Module: Printing circuit in text version of aiger format  
+        (Part 2)
+
+Author: Eugene Goldberg, eu.goldberg@gmail.com
+
+******************************************************/
+#include <queue>
+#include <set>
+#include <map>
+#include <algorithm>
+#include <iostream>
+
+#include <ebmc/ebmc_base.h>
+
+#include "minisat/core/Solver.h"
+#include "minisat/simp/SimpSolver.h"
+
+#include "dnf_io.hh"
+#include "ccircuit.hh"
+#include "m0ic3.hh"
+
+/*===========================================
+
+     P R I N T _ A I G E R _ C O N S T R S
+
+  ============================================*/
+void CompInfo::print_aiger_constrs(FILE *fp)
+{
+
+  ConstrGates::iterator pnt;
+
+  for (pnt = Constr_gates.begin(); pnt!= Constr_gates.end(); pnt++) {
+    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);
+  }
+} /* end of function print_aiger_constrs */
+
+/*============================================
+
+     P R I N T _ A I G E R _ G A T E S
+
+  ==========================================*/
+void CompInfo::print_aiger_gates(FILE *fp,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]);
+  }
+
+} /* end of function print_aiger_gates */
+
+/*===============================
+
+       A D D _ T R I P L E T
+
+  ==============================*/
+void CompInfo::add_triplet(DNF &Gates,int olit,int lit0,int lit1)
+{
+
+  CUBE C;
+  C.push_back(olit); C.push_back(lit0); C.push_back(lit1);
+  Gates.push_back(C);
+
+} /* end of function add_triplet */
+
+
+
+/*=========================================
+
+     F I N D _ M A X _ A I G E R _ V A R
+
+  =========================================*/
+int CompInfo::find_max_aiger_var(DNF &Gates)
+{
+
+  int max_lit = -1;
+  for (size_t i=0; i < Gates.size(); i++) {
+    CUBE &C = Gates[i];
+    for (size_t j=0; j < C.size(); j++) 
+      if (C[j] > max_lit) max_lit = C[j];
+  }
+
+  assert(max_lit >= 0);
+  if (max_lit & 1) max_lit--;
+  return(max_lit >> 1);
+} /* end of function find_max_aiger_var */
+
+
+
+/*==========================================
+
+      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)
+{
+  CUBE &C  = Gates[out_ind];
+  assert(C.size() == 3);
+  int lit = C[0];  
+
+  if (const_true_prop) { // make sure that the output is always 0
+    assert(C[1] == C[2]);
+    if (C[1] == 1) lit++; // negate the conjunction of constants 1
+  }
+
+  if (const_false_prop) { // make sure that the output is always 1
+    if ((C[1] == 0) || (C[2] == 0)) // at least one of the inputs is 0
+      lit++;
+  }
+  fprintf(fp,"%d\n",lit);
+} /* end of function print_aiger_output */
+
+/*=============================================
+
+    A D D _ A I G E R _ A N D _ G A T E
+
+  ============================================*/
+void CompInfo::add_aiger_and_gate(DNF &Gates,int gate_ind)
+{
+
+  Gate &G = N->get_gate(gate_ind);
+  assert(G.Polarity.back() == 0);
+  int olit = find_aiger_lit1(gate_ind,0);
+  int lit0 = find_aiger_lit1(G.Fanin_list[0],G.Polarity[0]);
+  int lit1 = find_aiger_lit1(G.Fanin_list[1],G.Polarity[1]);
+
+  add_triplet(Gates,olit,lit0,lit1);
+ 
+ 
+} /* end of function add_aiger_and_gate */
+
+/*=============================================
+
+    A D D _ A I G E R _ B U F F E R
+
+  ============================================*/
+void CompInfo::add_aiger_buffer(DNF &Gates,int gate_ind)
+{
+
+  Gate &G = N->get_gate(gate_ind);
+  assert(G.Polarity.back() == 0);
+  int olit = find_aiger_lit1(gate_ind,0);
+  int ilit = find_aiger_lit1(G.Fanin_list[0],G.Polarity[0]);
+
+  add_triplet(Gates,olit,ilit,ilit);
+ 
+} /* end of function add_aiger_buffer */
+
+/*=================================
+
+  P R I N T _ F U N C _ T Y P E
+
+  ================================*/
+void print_func_type(Gate &G) 
+{
+
+  switch (G.func_type) {
+  case CONST:
+    printf("CONST");
+    break;
+  case BUFFER:
+    printf("BUFFER");
+    break;
+  case AND:
+    printf("AND");
+    break;
+  case OR:
+    printf("OR");
+    break;
+  case TRUTH_TABLE:
+    printf("TRUTH_TABLE");
+    break;
+  case COMPLEX:
+    printf("COMPLEX");
+    break;
+  default:
+    printf("wrong value of func_type\n");
+    exit(100);
+  }
+
+  printf("\n");
+
+} /* end of function print_func_type */
+
diff --git a/src/ic3/next_time_frame.cc b/src/ic3/next_time_frame.cc
index 05cb44b3a..8c2f93ac8 100644
--- a/src/ic3/next_time_frame.cc
+++ b/src/ic3/next_time_frame.cc
@@ -44,13 +44,15 @@ int CompInfo::next_time_frame()
   add_time_frame();
   empty_cnts();
   init_bst_sat_solver();
- 
+
+  bool triv_time_frame = true;
   while (true) {
     bool sat_form = check_sat1(Bst_sat);
     if (sat_form == false) {
       ret_val = 2;
       break;}
 
+    triv_time_frame = false;
     CUBE Nst,St,Inps;
     extr_cut_assgns1(Nst,Next_svars,Bst_sat);
     extr_next_inps(Inps,Bst_sat);
@@ -99,7 +101,7 @@ int CompInfo::next_time_frame()
   if (rem_subsumed_flag) rem_redund_clauses();  
   simplify_tf_solvers();
   Lgs_sat.Mst->simplify();
-  push_clauses_forward(); 
+  push_clauses_forward(triv_time_frame); 
  
   if (inv_ind >= 0) return(0);    
 
@@ -143,6 +145,8 @@ void CompInfo::add_time_frame()
   Tf.tot_num_ctis = 0;
   Tf.num_rcnt_ctis = 0;
   Tf.num_bnd_cls = 0;
+  Tf.num_seen_cls = 0;
+  Tf.num_redund_cls = 0;
 
   Time_frames.push_back(Tf);
 
diff --git a/src/ic3/p1arameters.cc b/src/ic3/p1arameters.cc
index 3d5f1ffb7..1c536e27b 100644
--- a/src/ic3/p1arameters.cc
+++ b/src/ic3/p1arameters.cc
@@ -35,16 +35,16 @@ void ic3_enginet::read_parameters()
     exit(0);
   }
 
-  if (cmdline.isset("prop")) {
-    std::string sval = cmdline.get_value("prop");
-    Ci.prop_ind = stoi(sval);
-    // assert(Ci.prop_ind >= 0);
-  }
+  if (cmdline.isset("property")) 
+    Ci.prop_name = cmdline.get_value("property");
+  
 
   if (cmdline.isset("constr")) 
     Ci.constr_flag = true;
 
 
+  if (cmdline.isset("new-mode"))
+    Ci.standard_mode = false;
 } /* end of function read_parameters */
 
 /*==============================
@@ -55,10 +55,9 @@ void ic3_enginet::read_parameters()
 void ic3_enginet::print_header()
 {
 
-  printf("ebmc verilog_file --ic3 [--p | --prop N]\n");
-  printf("p      -  print out information about available options\n");
-  printf("prop N -  check property number N (count starts with 0)\n");
-  
+  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");
 } /* end of function print_header */
 
 /*=====================================
@@ -89,7 +88,6 @@ void CompInfo::init_parameters()
   lift_sort_mode = FULL_SORT;
   ind_cls_sort_mode = FULL_SORT;
   gate_sort_mode = INPS_FIRST;
-  // gate_sort_mode = INIT_SORT;
   multiplier = 1.05;
   factor = 1.;
   max_act_val = 10000.;
@@ -97,10 +95,9 @@ void CompInfo::init_parameters()
   ctg_flag = true;
   max_ctg_cnt = 3;
   max_rec_depth = 1;
-  grl_heur = NO_JOINS;
   max_coi_depth = 10;
-  prop_ind = 0;
   constr_flag = false;
-
+  standard_mode = true;
+  
   } /* end of function init_parameters */
 
diff --git a/src/ic3/p2ush_clauses_forward.cc b/src/ic3/p2ush_clauses_forward.cc
index 4e4171b16..84a0688a3 100644
--- a/src/ic3/p2ush_clauses_forward.cc
+++ b/src/ic3/p2ush_clauses_forward.cc
@@ -21,7 +21,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
   P U S H _ C L A U S E S _ F O R W A R D
 
   ===========================================*/
-void CompInfo::push_clauses_forward()
+void CompInfo::push_clauses_forward(bool triv_time_frame)
 {
   if (verbose == 0) {
     printf("%*c",3,' ');
@@ -32,6 +32,8 @@ void CompInfo::push_clauses_forward()
 
   assert(tf_lind>=0 && (size_t) tf_lind < Time_frames.size());
   init_fields();
+
+  if (triv_time_frame) min_tf = tf_lind;
   for (size_t i=min_tf; i <= (size_t) tf_lind; i++) { 
     CUBE Pushed;
     CUBE &Clauses = Time_frames[i].Clauses;
@@ -67,7 +69,7 @@ void CompInfo::push_clauses_forward()
 	  add_copies(i,C);
 	  continue;}
       }
-      else  // C.size() == F[clause_ind.size()
+      else  // C.size() == F[clause_ind].size()
 	if (Clause_info[clause_ind].span < i) 
 	  continue;
 	
diff --git a/src/ic3/r0ead_input.cc b/src/ic3/r0ead_input.cc
index e7703d050..767bf1a51 100644
--- a/src/ic3/r0ead_input.cc
+++ b/src/ic3/r0ead_input.cc
@@ -75,9 +75,9 @@ void ic3_enginet::form_circ_from_ebmc()
   find_prop_lit();
  
   form_latched_gates();
- 
-  form_gates();
 
+  form_gates();
+ 
   CDNF Out_names;
   form_outp_buf(Out_names);
   form_invs();
@@ -85,6 +85,7 @@ void ic3_enginet::form_circ_from_ebmc()
  
   add_spec_buffs(N);
 
+  add_pseudo_inps(N);
  
   fill_fanout_lists(N);
   assign_gate_type(N,Out_names,true);
@@ -115,7 +116,8 @@ void ic3_enginet::form_inputs()
     if (var.is_input() == false) continue;
     for (size_t j=0; j < var.bits.size(); j++) {  
       literalt lit =var.bits[j].current;
-      int lit_val = lit.get();    
+      int lit_val = lit.get();
+      //      printf("lit_val = %d\n",lit_val);
       CCUBE Name;
       if (orig_names) {
 	bool ok = form_orig_name(Name,lit);
@@ -135,10 +137,6 @@ void ic3_enginet::form_inputs()
 } /* end of function form_inputs */
 
 
-
-
-
-
 /*=================================
 
        F O R M _ T A B L E
@@ -187,10 +185,6 @@ void CompInfo::form_max_pres_svar() {
   max_pres_svar = max;
 } /* end of function form_max_pres_svar */
 
-
-
-
-
 /*===================================
 
       F O R M _ V A R _ N U M S
@@ -207,3 +201,20 @@ void CompInfo::form_var_nums()
   max_num_vars = max_num_vars0 + num_prop_vars; // we need to take into account
   // that property needs to be specified in two time frames
 } /* end of function form_var_nums */
+
+/*================================================
+
+   A D D _ V E R I L O G _ C O N V _ C O N S T R S
+
+  ================================================*/
+void ic3_enginet::add_verilog_conv_constrs()
+{
+
+  for(literalt lit : netlist.constraints) {
+    if (lit.is_constant()) continue;
+    std::cout << "constraint literal " << lit.get() << "\n";
+     Ci.Init_clits.insert(lit.get());
+  }
+
+
+} /* end of function add_verlig_conv_constrs */
diff --git a/src/ic3/r1ead_input.cc b/src/ic3/r1ead_input.cc
index 0563d6609..a9633aef2 100644
--- a/src/ic3/r1ead_input.cc
+++ b/src/ic3/r1ead_input.cc
@@ -58,8 +58,14 @@ 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");
   
 } /* end of function find_prop_lit */
 
@@ -105,6 +111,8 @@ void ic3_enginet::form_latched_gates()
       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);
       add_new_latch(Latches,init_val,lit,next_lit);
     }
   }
diff --git a/src/ic3/r3ead_input.cc b/src/ic3/r3ead_input.cc
index a8d0d750e..5d08150e8 100644
--- a/src/ic3/r3ead_input.cc
+++ b/src/ic3/r3ead_input.cc
@@ -147,7 +147,11 @@ 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 */
 
 /*===============================
@@ -160,10 +164,17 @@ void ic3_enginet::form_gates()
 
   Circuit *N = Ci.N;
   aigt::nodest &Nodes = netlist.nodes;
- 
+
   for (size_t i=0; i <  Nodes.size(); i++) {  
     aigt::nodet &Nd = Nodes[i];
-    if (Nd.is_var()) continue;
+    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);
+      continue;
+    }
     CDNF Pin_names;
     CUBE Pol;    
     form_gate_pin_names(Pin_names,Pol,i);
@@ -185,10 +196,15 @@ void ic3_enginet::form_gates()
 void ic3_enginet::form_outp_buf(CDNF &Out_names)
 {
 
-  int olit = prop_l.get();
-  if (prop_l.is_constant() == 0) 
-    if (prop_l.sign()) olit--;
+ 
+  unsigned olit = prop_l.get();
+
+  Ci.const_false_prop = false;
+  Ci.const_true_prop = false;
   
+  if (prop_l.is_constant() == 0)
+    if (prop_l.sign()) 
+       olit--;
 
   assert(Ci.Inps.find(olit) == Ci.Inps.end());
   bool latch = false;
@@ -200,13 +216,15 @@ void ic3_enginet::form_outp_buf(CDNF &Out_names)
   Pin_names.push_back(Dummy);
   char Buff[MAX_NAME];
   if (prop_l.is_false())  {
-     sprintf(Buff,"c0");
-     conv_to_vect(Pin_names[0],Buff);
-     goto NEXT;  }
+    Ci.const_false_prop = true;
+    sprintf(Buff,"c0");
+    conv_to_vect(Pin_names[0],Buff);
+    goto NEXT;  }
   if (prop_l.is_true()) {
-     sprintf(Buff,"c1");
-     conv_to_vect(Pin_names[0],Buff);
-     goto NEXT;
+    Ci.const_true_prop = true;
+    sprintf(Buff,"c1");
+    conv_to_vect(Pin_names[0],Buff);
+    goto NEXT;
   }
   
   if (orig_names) 
@@ -219,7 +237,7 @@ void ic3_enginet::form_outp_buf(CDNF &Out_names)
 
  NEXT:
   char buff[MAX_NAME];
-  sprintf(buff,"p%zu",Ci.prop_ind);
+  sprintf(buff,"%s",Ci.prop_name.c_str());
   conv_to_vect(Pin_names[1],buff);
   Out_names.push_back(Pin_names[1]);
 
diff --git a/src/ic3/r4ead_input.cc b/src/ic3/r4ead_input.cc
index e0b1039e5..d9abcf276 100644
--- a/src/ic3/r4ead_input.cc
+++ b/src/ic3/r4ead_input.cc
@@ -21,6 +21,8 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include "m0ic3.hh"
 
 #include "ebmc_ic3_interface.hh"
+
+
 /*=========================================
 
       U P D _ G A T E _ C O N S T R S
@@ -84,6 +86,7 @@ int CompInfo::upd_gate_constr_tbl(int lit,int gate_ind)
 void ic3_enginet::store_constraints(const std::string &fname)
 {
 
+  add_verilog_conv_constrs();
   if (Ci.constr_flag == false) return;
 
   read_constraints(fname);
@@ -165,16 +168,35 @@ void ic3_enginet::ebmc_form_latches()
 
   for(var_mapt::mapt::const_iterator it=vm.map.begin();
       it!=vm.map.end(); it++)    {
-    const var_mapt::vart &var=it->second; 
+    const var_mapt::vart &var=it->second;
+    
+    if (var.vartype ==var_mapt::vart::vartypet::NONDET) {
+      assert(var.bits.size() > 0);
+      int val = (var.bits.size() == 1)?1:2;
+      for (size_t i=0; i < var.bits.size(); i++) {
+	literalt lit = var.bits[i].current;
+	int var_num = lit.var_no();
+	Nondet_vars[var_num] = val;
+      }
+      continue;
+    }
+    
     if (var.vartype !=var_mapt::vart::vartypet::LATCH) 
       continue;
 
     for (size_t j=0; j < var.bits.size(); j++) {
       literalt lit =var.bits[j].current;
-      Latch_val[lit.var_no()] = 2; // set the value of the latch to a don't care     
+      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);
+  }
   // set initial values
   bvt Ist_lits;
   gen_ist_lits(Ist_lits);
@@ -182,7 +204,14 @@ void ic3_enginet::ebmc_form_latches()
   for (size_t i=0; i < Ist_lits.size(); i++) {
     literalt &lit = Ist_lits[i];
     int var_num = lit.var_no();
-    assert(Latch_val.find(var_num) != Latch_val.end());
+    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);
+    }
     if (lit.sign()) Latch_val[var_num] = 0;
     else Latch_val[var_num] = 1;
   }
@@ -208,15 +237,24 @@ void ic3_enginet::gen_ist_lits(bvt &Ist_lits)
   while (stack.size() > 0) {
 
     literalt lit = stack.back();
+    assert(lit.is_constant() == false);
     size_t var_num = lit.var_no();
     stack.pop_back();
     if (Visited.find(lit) != Visited.end()) 
       continue;
-    assert(var_num < Nodes.size());
+    if (var_num >= Nodes.size()) {
+      p();
+      printf("var_num = %zd\n",var_num);
+      printf("Nodes.size() = %zu\n",Nodes.size());
+      exit(100);
+    }
     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);
       continue;
     }
 
diff --git a/src/ic3/r6ead_input.cc b/src/ic3/r6ead_input.cc
index 4294ddb29..dc3175f34 100644
--- a/src/ic3/r6ead_input.cc
+++ b/src/ic3/r6ead_input.cc
@@ -85,24 +85,23 @@ void ic3_enginet::read_constraints(const std::string &source_name)
 bool ic3_enginet::find_prop(propertyt &Prop)
 {
 
-  if (Ci.prop_ind >=  properties.size()) {
-    std::cout << "file " << cmdline.args[0] << " specifies only ";
-    std::cout  << properties.size() << " properties\n";
-    exit(100);
+  assert(properties.size() > 0);
+
+  if ((properties.size() >= 1) && (Ci.prop_name.size() == 0)) {
+    Prop = properties.front();
+    Ci.prop_name = id2string(Prop.name);
+    return(true);
   }
-  
-  for(const auto &p : properties) {
-    irep_idt Nm = p.name;
-    std::string Sn = short_name(Nm);
-    int ind = stoi(Sn);
-    assert(ind>0 && "Property Index must be greater than 0");
-    size_t index=(size_t) ind;
-    if (index-1 == Ci.prop_ind) {
+    
+  for(const auto &p : properties) 
+    if (p.status==propertyt::statust::UNKNOWN) {
+      assert(p.name == Ci.prop_name);
       Prop = p;
       return(true);
     }
-    //idx++;
-  }
+    
+   
+  
   return false;
 } /* end of function find_prop */
 
@@ -153,6 +152,7 @@ void ic3_enginet::form_orig_names()
 void ic3_enginet::print_nodes()
 {
 
+  printf("\n-----  Nodes ------\n");
   aigt::nodest &Nodes = netlist.nodes;
   for (size_t i=0; i <= Nodes.size(); i++) {  
     aigt::nodet &Nd = Nodes[i];
diff --git a/src/ic3/r7ead_input.cc b/src/ic3/r7ead_input.cc
index 61effcd10..8b53ec6b6 100644
--- a/src/ic3/r7ead_input.cc
+++ b/src/ic3/r7ead_input.cc
@@ -23,6 +23,120 @@ 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(std::ostream &out)
+{
+
+
+  printf("\n-----  Var Map ------\n");
+
+  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;
+
+      for(std::size_t i=0; i<var.bits.size(); i++)
+	{
+	  out << "  " << it->first;
+	  if(var.bits.size()!=1) out << "[" << i << "]";
+	  out << "=";
+
+	  literalt l_c=var.bits[i].current;
+
+	  if(l_c.is_true())
+	    out << "true";
+	  else if(l_c.is_false())
+	    out << "false";
+	  else
+	    {
+	      if(l_c.sign()) out << "!";
+	      out << l_c.var_no();
+	    }
+      
+	  if(var.vartype==var_mapt::vart::vartypet::LATCH)
+	    {
+	      out << "->";
+        
+	      literalt l_n=var.bits[i].next;
+
+	      if(l_n.is_true())
+		out << "true";
+	      else if(l_n.is_false())
+		out << "false";
+	      else
+		{
+		  if(l_n.sign()) out << "!";
+		  out << l_n.var_no();
+		}
+	    }
+       
+	  out << " ";
+
+	  switch(var.vartype)
+	    {
+	    case var_mapt::vart::vartypet::INPUT: out << "(input)"; break;
+	    case var_mapt::vart::vartypet::LATCH: out << "(latch)"; break;
+	    case var_mapt::vart::vartypet::NONDET: out << "(nondet)"; break;
+	    case var_mapt::vart::vartypet::WIRE:  out << "(wire)"; break;
+	    case var_mapt::vart::vartypet::OUTPUT:out << "(output)"; break;
+	    case var_mapt::vart::vartypet::UNDEF: out << "(?)"; break;
+	    }
+
+	  out << '\n';
+	}
+    }
+
+  out << '\n'
+      << "Total no. of variable bits: " << vm.reverse_map.size() << '\n'
+      << "Total no. of latch bits: " << vm.latches.size() << '\n'
+      << "Total no. of nondet bits: " << vm.nondets.size() << '\n'
+      << "Total no. of input bits: " << vm.inputs.size() << '\n'
+      << "Total no. of output bits: " << vm.outputs.size() << '\n';
+
+  
+
+    } /* end of function print_var_map */
+/*=========================================
+
+        A D D _ P S E U D O _ I N P S
+
+  ==========================================*/
+void ic3_enginet::add_pseudo_inps(Circuit *N)
+{
+
+
+  GCUBE &Gate_list = N->Gate_list;
+  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;
+    G.flags.active = 1; // mark this input as active 
+    G.flags.output = 0;
+    G.flags.transition = 0;
+    G.flags.output_function = 0;
+    G.flags.feeds_latch = 0;
+    G.level_from_inputs = 0; // set the topological level to 0
+    G.inp_feeds_latch = false;
+ 
+    //   Add it to the circuit
+   
+    N->Inputs.push_back(i);
+    N->ninputs++; // increment the number of inputs
+   
+  }
+
+} /*end of function add_pseudo_inps */
+
 /*=========================================
 
  F O R M _ I N I T _ C O N S T R _ L I T S
diff --git a/src/ic3/s1tat.cc b/src/ic3/s1tat.cc
index 52bb415ab..d73cc7c61 100644
--- a/src/ic3/s1tat.cc
+++ b/src/ic3/s1tat.cc
@@ -130,14 +130,15 @@ void CompInfo::print_time_frame_stat()
     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,
-           Time_frames[tf_lind].num_bnd_cls,tf_lind+1,
+           Tf.num_bnd_cls,tf_lind+1,
 	   Time_frames[tf_lind+1].num_bnd_cls);
 
 
   if (verbose > 0)  {
-    printf("num_pbs-s: %d\n",Time_frames[tf_lind].num_pbss);
+    printf("num_pbs-s: %d\n",Tf.num_pbss);
 
     printf("Cti-s:\n");
     int count = 0;
@@ -158,6 +159,8 @@ void CompInfo::print_time_frame_stat()
   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*/
 
 
diff --git a/src/ic3/s2horten_clause.cc b/src/ic3/s2horten_clause.cc
index fad864f3d..899687fb1 100644
--- a/src/ic3/s2horten_clause.cc
+++ b/src/ic3/s2horten_clause.cc
@@ -27,8 +27,9 @@ void CompInfo::shorten_clause(CLAUSE &C,int curr_tf,CLAUSE &C0,char st_descr,
 
   assert(curr_tf>=0 && (size_t) curr_tf < Time_frames.size());
   CLAUSE B0 = C0;
-  
+
   while (true) {
+    if (standard_mode) break;
     if (B0.size() < 10) break;
     CLAUSE B;  
     compos_short(B,B0,curr_tf,st_descr);
diff --git a/src/ic3/s3tat.cc b/src/ic3/s3tat.cc
index d30d17dd4..5f74f1052 100644
--- a/src/ic3/s3tat.cc
+++ b/src/ic3/s3tat.cc
@@ -101,14 +101,8 @@ void CompInfo::print_flags()
   printf("selector = %d\n",selector);
   printf("ctg_flag = %d\n",ctg_flag);
   printf("constr_flag = %d\n",constr_flag);
-
-  // print state of generalization heuristic
-  printf("generalization heuristic = ");
-  if (grl_heur == NO_JOINS) printf("NO_JOINS\n");
-  else {
-    assert(grl_heur == WITH_JOINS);
-    printf("WITH_JOINS\n");
-  }
+  printf("standard_mode = %d\n",standard_mode);
+ 
 
 
 
diff --git a/src/ic3/seq_circ/a2dd_gate.cc b/src/ic3/seq_circ/a2dd_gate.cc
index 13fd39477..43a0520d0 100644
--- a/src/ic3/seq_circ/a2dd_gate.cc
+++ b/src/ic3/seq_circ/a2dd_gate.cc
@@ -40,6 +40,7 @@ int assign_input_pin_number1(std::map<CCUBE,int> &pin_list,
     pin_list[name] = pin_num;
     G.flags.active = 0;
     G.gate_type = UNDEFINED;
+    G.Gate_name = name;
     gate_list.push_back(G); // add one more gate 
   }
   else /* an 'old' pin */
diff --git a/src/ic3/seq_circ/ccircuit.hh b/src/ic3/seq_circ/ccircuit.hh
index f676bea29..d037a6748 100644
--- a/src/ic3/seq_circ/ccircuit.hh
+++ b/src/ic3/seq_circ/ccircuit.hh
@@ -196,6 +196,7 @@ 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);
 
 #include "more_fun_prot.hh"
 
diff --git a/src/ic3/todo b/src/ic3/todo
index c64e98d06..3d414f4d8 100644
--- a/src/ic3/todo
+++ b/src/ic3/todo
@@ -3,7 +3,6 @@
 Finishing integration
 with ebmc
 =====================
-
 *) Add code freeing memory allocated by the Verilog reader after IC3
    converted this information into its internal data
    structure. (Keeping this memory is too expensive for large
@@ -21,8 +20,6 @@ Changes of the current implementation
    to finish a time frame, average size of inductive clauses,
    averages size of cubes generalizing bad states etc)
 
-*) Optimize the procedure of building the longest inductive clause for
-   the case of designs with a large number of latches
 
 *) Implement actual removal of subsumed clauses (currently they are
    just marked and ignored by the algorithm)
@@ -32,18 +29,21 @@ Changes of the current implementation
 Improvements of the basic algorithm
 ====================================
 
-*) Write a perl script meant for efficiently checking multiple
-   properties. The idea is to check properties one by one re-using
-   information found when proving (or disproving) previous properties.
+*) Implement a version of IC3 that combines property strengthening and
+   property relaxation. Combining strenthening and relation allows one
+   to "emulate" an algorithm that employs depth-first search.
 
-*) Implement the version of IC3 that fixes the problem with
-   convergence rate (by computing reachability of good states breaking
-   induction)
 
 *) Implement a "dual" IC3 where one over-approximates the set of
    states from which a bad state is reachable in j transitions (rather
    than the set of states reachable in j transitions from initial
    states).
 
-*) Implement a version of IC3 where one employs depth-first search
+*) Implement the version of IC3 that fixes the problem with
+   convergence rate (by computing reachability of good states breaking
+   induction)
+
+
+
+
 
diff --git a/src/ic3/u1til.cc b/src/ic3/u1til.cc
index f486ee59a..47ed70f97 100644
--- a/src/ic3/u1til.cc
+++ b/src/ic3/u1til.cc
@@ -36,10 +36,14 @@ void CompInfo::add_fclause1(CLAUSE &C,int last_ind,char st_descr)
   int prev_tf_ind = -1;
 
   if (Clause_table.find(C) != Clause_table.end()) {
+    TimeFrame &Tf = Time_frames[tf_lind];
+    if (st_descr <= CTG_STATE) Tf.num_seen_cls++;
     clause_ind1  = Clause_table[C];
     prev_tf_ind = Clause_info[clause_ind1].span;
-    if (update_fclause(clause_ind1,last_ind) == false) 
+    if (update_fclause(clause_ind1,last_ind) == false) {
+      if (st_descr <= CTG_STATE) Tf.num_redund_cls++;
       return;
+    }
     goto NEXT;
   }
 
diff --git a/src/ic3/u3til.cc b/src/ic3/u3til.cc
index 769d10d77..51f63bcba 100644
--- a/src/ic3/u3til.cc
+++ b/src/ic3/u3til.cc
@@ -184,3 +184,17 @@ void CompInfo::full_sort(CLAUSE &C1,CLAUSE &C, std::vector <ActInd> &V) {
 } /* end of function full_sort */
 
 
+/*===================================
+
+     P U S H _ O N _ T H E _ F L Y
+
+  =================================*/
+int CompInfo::push_on_the_fly(int last_ind,CLAUSE &C,char st_desc)
+{
+
+  int tf_ind = latest_succ_tf_ind(last_ind,C);
+  if (tf_ind < 0) tf_ind = last_ind-1;
+
+  return(tf_ind+1);
+
+} /* end of function push_on_the_fly */
diff --git a/src/ic3/v0erify.cc b/src/ic3/v0erify.cc
index db204f337..0119292b0 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("verification is ok\n");
+  printf("inductive invariant verification is ok\n");
   return(true);
 } /* end of function ver_trans_inv */
 
@@ -91,7 +91,7 @@ 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("verification failed\n");
+      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;
@@ -139,7 +139,7 @@ bool CompInfo::ver_prop()
 
   bool sat_form = check_sat1(Gen_sat);
   if (sat_form) {
-    printf("verification failed\n");
+    printf("inductive invariant verification failed\n");
     printf("Ist does not imply Prop\n");
     return(false);
   }
@@ -161,6 +161,7 @@ bool CompInfo::ver_ini_states(CNF &H)
   
   accept_new_clauses(Gen_sat,Ist);  
 
+  accept_constrs(Gen_sat);
   bool ok = ver_prop();
   if (!ok) return(false);
 
@@ -202,7 +203,7 @@ bool CompInfo::ver_ind_clauses1(CNF &H)
    
     bool sat_form = check_sat2(Gen_sat,Assmps);
     if (sat_form) {
-      printf("verification failed\n");  
+      printf("inductive invariant verification failed\n");  
       printf("clause F[%zu] excludes an initial state: ", i);
       std::cout << H[i] << std::endl;
       return(false);
diff --git a/src/ic3/v1erify.cc b/src/ic3/v1erify.cc
index 19c72718c..64a8c31d0 100644
--- a/src/ic3/v1erify.cc
+++ b/src/ic3/v1erify.cc
@@ -78,7 +78,7 @@ bool CompInfo::ver_cex()
   if (!ok) return(false);
 
  FINISH:
-  printf("verification is ok\n");
+  printf("cex verification is ok\n");
   return(true);
 } /* end of function ver_cex */
 
@@ -99,7 +99,7 @@ bool CompInfo::check_bad_state(CUBE &St)
   add_assumps1(Assmps,St);
   bool sat_form = check_sat2(Gen_sat,Assmps);
   if (sat_form == false) {
-    printf("verification failed\n");
+    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);
@@ -150,7 +150,7 @@ bool CompInfo::check_init_state(CUBE &St)
   
   bool sat_form = check_sat2(Gen_sat,Assmps);
   if (sat_form == false) {
-    printf("verification failed\n");
+    printf("cex verification failed\n");
     printf("Cex starts with a non-initial state\n");
     return(false);
   }
diff --git a/src/vcegar/abstractor.cpp b/src/vcegar/abstractor.cpp
index 2102978c2..8a5597c8e 100644
--- a/src/vcegar/abstractor.cpp
+++ b/src/vcegar/abstractor.cpp
@@ -572,8 +572,9 @@ void abstractort::calc_abstract_trans_rel(
     throw "unexpected result from predabs_sat1.solve()";
   }
 
-  print(9, "Generated "+
-    i2string(trans_cube_set.no_insertions())+" cube(s)");
+  debug() <<"Generated "
+          << i2string(trans_cube_set.no_insertions()) << " cube(s)"
+          << eom;
 
   if(show_cubes)
     std::cout << trans_cube_set;
@@ -693,8 +694,9 @@ void abstractort::calc_abstract_initial_states(
   }
 
   // std::cout<<" The abstract transition relation \n";
-  print(9, "Generated "+
-    i2string(initial.no_insertions())+" cube(s)\n");
+  debug() << "Generated " <<
+          << i2string(initial.no_insertions()) <, " cube(s)\n"
+          << eom;
 
   if(show_cubes)
     std::cout << initial;
diff --git a/src/vcegar/modelchecker_smv.cpp b/src/vcegar/modelchecker_smv.cpp
index d5ccf95d1..922346208 100644
--- a/src/vcegar/modelchecker_smv.cpp
+++ b/src/vcegar/modelchecker_smv.cpp
@@ -164,7 +164,7 @@ bool modelchecker_smvt::read_result_cadence_smv(
           counterexample);
 
 
-        print(9, "Cadence SMV counterexample sucessfully read");
+        debug() << "Cadence SMV counterexample sucessfully read" << eom;
 
         return false;
       }
diff --git a/src/verilog/verilog_language.cpp b/src/verilog/verilog_language.cpp
index 920a3fa01..32ad6198a 100644
--- a/src/verilog/verilog_language.cpp
+++ b/src/verilog/verilog_language.cpp
@@ -162,7 +162,7 @@ bool verilog_languaget::typecheck(
   if(verilog_typecheck(parse_tree, symbol_table, module, get_message_handler()))
     return true;
     
-  print(9, "Synthesis "+module);
+  debug() << "Synthesis " << module << eom;
 
   if(verilog_synthesis(symbol_table, module, get_message_handler(), options))
     return true;
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index 03a98c7aa..0228639a1 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -2026,6 +2026,9 @@ bool verilog_typecheck(
   message_handlert &message_handler,
   const namespacet &ns)
 {
+  const unsigned errors_before=
+    message_handler.get_message_count(messaget::M_ERROR);
+
   verilog_typecheck_exprt verilog_typecheck_expr(
     ns, module_identifier, message_handler);
 
@@ -2048,6 +2051,6 @@ bool verilog_typecheck(
   {
     verilog_typecheck_expr.error() << e << messaget::eom;
   }
-  
-  return verilog_typecheck_expr.get_error_found();
+
+  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
 }
diff --git a/src/vhdl/parser.y b/src/vhdl/parser.y
index b76873a40..1396907b3 100644
--- a/src/vhdl/parser.y
+++ b/src/vhdl/parser.y
@@ -53,7 +53,8 @@ int yyvhdlerror(const char *error_str)
   source_location.set_line(yyvhdllval.line);
   source_location.set_file(yyvhdllval.file);
 
-  PARSER.print(1, tmp, -1, source_location);
+  PARSER.error().source_location=source_location;
+  PARSER.error() << tmp << messaget::eom;
                   
   return strlen(error_str)+1;
 }