From 504ed14e9b2933dec31932ef0b74e0c985f276bb Mon Sep 17 00:00:00 2001
From: Yuheng Su <gipsyh.icu@gmail.com>
Date: Tue, 27 Aug 2024 09:50:54 +0800
Subject: [PATCH] bump aiger version and support arbitrary initialization
 functions in btor2aiger

Signed-off-by: Yuheng Su <gipsyh.icu@gmail.com>
---
 setup-deps.sh      | 8 ++++----
 src/btor2aiger.cpp | 8 +-------
 2 files changed, 5 insertions(+), 11 deletions(-)

diff --git a/setup-deps.sh b/setup-deps.sh
index 4450d4c..2595818 100755
--- a/setup-deps.sh
+++ b/setup-deps.sh
@@ -6,10 +6,10 @@ rm -rf deps
 mkdir -p deps
 
 # Setup AIGER
-rm -rf aiger-1.9.4.tar.gz
-wget http://fmv.jku.at/aiger/aiger-1.9.4.tar.gz
-tar xf aiger-1.9.4.tar.gz
-mv aiger-1.9.4 deps/aiger
+rm -rf aiger-1.9.18.tar.gz
+wget https://github.com/arminbiere/aiger/archive/refs/tags/rel-1.9.18.tar.gz
+tar xf rel-1.9.18.tar.gz
+mv aiger-rel-1.9.18 deps/aiger
 
 
 # Setup Boolector
diff --git a/src/btor2aiger.cpp b/src/btor2aiger.cpp
index c9a1d23..6fc42ea 100644
--- a/src/btor2aiger.cpp
+++ b/src/btor2aiger.cpp
@@ -414,16 +414,10 @@ add_state_to_aiger (Btor *btor,
 
   for (size_t i = 0; i < nbits; ++i)
   {
-    if (init_bits && init_bits[i] != 0 && init_bits[i] != 1)
-    {
-      /* Note: BTOR2 supports arbitrary initialization functions, but AIGER
-       * only supports 0/1/undefined. */
-      die ("Found non-constant initialization");
-    }
     sym = boolector_aig_get_symbol (amgr, state_bits[i]);
     if (next_bits)
     {
-      reset_val = init_bits ? init_bits[i] : state_bits[i];
+      reset_val = init_bits && init_bits[i] <= 1 ? init_bits[i] : state_bits[i];
       aiger_add_latch (aig, state_bits[i], next_bits[i], sym);
       aiger_add_reset (aig, state_bits[i], reset_val);
     }