diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index 29fdc70e0..eb81aeb26 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/src/ebmc/ebmc_parse_options.cpp
@@ -264,8 +264,10 @@ void ebmc_parse_optionst::help()
     " --ic3 [options]                   use IC3 engine with options described below\n"
     "       --property <nm>                  check property named <nm>\n"
     "       --constr                         use constraints specified in 'file.cnstr'\n"
-    "       --help                           print out help information\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 1415a3489..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)(property):(constr)(h)(new-mode)"
+    "(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/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/m0ic3.hh b/src/ic3/m0ic3.hh
index 681bb1bcc..e6a31e385 100644
--- a/src/ic3/m0ic3.hh
+++ b/src/ic3/m0ic3.hh
@@ -24,7 +24,9 @@ public:
                  // Ordering[i] == i
  
   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'
@@ -263,6 +265,7 @@ public:
   void form_consts(Circuit *N);
   void form_constr_lits();
   void add_constrs();
+  void print_aiger_format();
 
 protected:
 
diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc
index e9b5bcb03..d37334d08 100644
--- a/src/ic3/m1ain.cc
+++ b/src/ic3/m1ain.cc
@@ -81,6 +81,12 @@ int ic3_enginet::operator()()
   
   
   read_ebmc_input();
+  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 c8f0cc01d..a8fec08b5 100644
--- a/src/ic3/m2ethods.hh
+++ b/src/ic3/m2ethods.hh
@@ -206,5 +206,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..7e9e9a181
--- /dev/null
+++ b/src/ic3/m4y_aiger_print.cc
@@ -0,0 +1,239 @@
+#include <iostream>
+#include <list>
+#include <vector>
+#include <queue>
+#include <set>
+#include <map>
+#include <stdio.h>
+#include <stdlib.h>
+#include <strings.h>
+#include <string.h>
+#include <time.h>
+#include <algorithm>
+#include <ctime>
+#include <climits>
+#include <cassert>
+#include <sys/time.h>
+#include <sys/resource.h>
+#include <unistd.h>
+
+#include <ebmc/ebmc_base.h>
+
+#include "minisat/core/Solver.h"
+#include "minisat/simp/SimpSolver.h"
+
+
+using namespace std;
+#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);
+  // printf("num_buffs = %d\n",num_buffs);
+  assert(num_consts <= 2);
+  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,"%d ",N->ninputs);
+  fprintf(fp,"%d ",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 = %d\n",i);
+	printf("N->Gate_list.size() = %d\n",(int) N->Gate_list.size());
+	printf("G.ninputs = %d\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..bef3621c4
--- /dev/null
+++ b/src/ic3/m5y_aiger_print.cc
@@ -0,0 +1,196 @@
+#include <iostream>
+#include <list>
+#include <vector>
+#include <queue>
+#include <set>
+#include <map>
+#include <stdio.h>
+#include <stdlib.h>
+#include <strings.h>
+#include <string.h>
+#include <time.h>
+#include <algorithm>
+#include <ctime>
+#include <climits>
+#include <cassert>
+#include <sys/time.h>
+#include <sys/resource.h>
+#include <unistd.h>
+
+#include <ebmc/ebmc_base.h>
+
+#include "minisat/core/Solver.h"
+#include "minisat/simp/SimpSolver.h"
+
+using namespace std;
+#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/r3ead_input.cc b/src/ic3/r3ead_input.cc
index e4dd77b32..0b00cbec8 100644
--- a/src/ic3/r3ead_input.cc
+++ b/src/ic3/r3ead_input.cc
@@ -185,9 +185,19 @@ 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());
@@ -200,13 +210,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) 
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/ttodo b/src/ic3/ttodo
index a79158ede..210500342 100644
--- a/src/ic3/ttodo
+++ b/src/ic3/ttodo
@@ -3,6 +3,11 @@
      T O   D O
  
 =====================
+*) polish the header part of 'm4y_aiger_print.cc
+   and 'm5y_aiger_print.cc' (take into account
+   Matthias' PR)
+
+
 *) add code to the procedures affected by
    the value of 'standard_mode'
 
@@ -13,18 +18,10 @@
  
 
 
-
-
-
-
-*) modify pushing for trivial time frames
-
 *) add parameter --stat
 
 *) add perl script that checks all the properties in a straightforward way
 
-*) remove grl_heur flag and the related code
-
 *) remove all the extra files I have added (scripts and so on)
 
 
@@ -64,4 +61,9 @@
     +) set_long_param("act_obl",0);
     +) set_long_param("mult_tried",0);
     +) set_long_param("brad_obl",1);
-    +) set_long_param("dyn_push",1);
\ No newline at end of file
+    +) set_long_param("dyn_push",1);
+*) modify pushing for trivial time frames
+*) remove grl_heur flag and the related code
+*) remove add_final_gates
+*) add option to print out the circuit in
+   the aiger format
\ No newline at end of file