From cd79b51118122413981ae2f55549d2aeaf473b98 Mon Sep 17 00:00:00 2001
From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com>
Date: Mon, 11 Mar 2024 23:16:31 -0700
Subject: [PATCH 1/4] purify bv-array arguments

---
 src/mcsat/preprocessor.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/mcsat/preprocessor.c b/src/mcsat/preprocessor.c
index 58807edd1..0db5e5761 100644
--- a/src/mcsat/preprocessor.c
+++ b/src/mcsat/preprocessor.c
@@ -476,7 +476,6 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
     case ARITH_EQ_ATOM:      // equality (t == 0)
     case ARITH_BINEQ_ATOM:   // equality: (t1 == t2)  (between two arithmetic terms)
     case ARITH_GE_ATOM:      // inequality (t >= 0)
-    case BV_ARRAY:
     case BV_DIV:
     case BV_REM:
     case BV_SMOD:
@@ -895,6 +894,7 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
     case ARITH_RDIV:         // regular division (/ x y)
     case ARITH_IDIV:         // division: (div x y) as defined in SMT-LIB 2
     case ARITH_MOD:          // remainder: (mod x y) is y - x * (div x y)
+    case BV_ARRAY:           // bit array
     case UPDATE_TERM:        // update array
     {
       composite_term_t* desc = get_composite(terms, current_kind, current);

From d19f4406989a8970946948e06aaeb70ee09e568b Mon Sep 17 00:00:00 2001
From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com>
Date: Mon, 11 Mar 2024 23:17:49 -0700
Subject: [PATCH 2/4] add regression test

---
 tests/regress/mcsat/issue400.smt2         | 5 +++++
 tests/regress/mcsat/issue400.smt2.gold    | 2 ++
 tests/regress/mcsat/issue400.smt2.options | 1 +
 3 files changed, 8 insertions(+)
 create mode 100644 tests/regress/mcsat/issue400.smt2
 create mode 100644 tests/regress/mcsat/issue400.smt2.gold
 create mode 100644 tests/regress/mcsat/issue400.smt2.options

diff --git a/tests/regress/mcsat/issue400.smt2 b/tests/regress/mcsat/issue400.smt2
new file mode 100644
index 000000000..6002cc3c9
--- /dev/null
+++ b/tests/regress/mcsat/issue400.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-fun v () (_ BitVec 1))
+(declare-fun a () Int)
+(assert (distinct (= 0 a) (= v (_ bv1 1))))
+(check-sat)
\ No newline at end of file
diff --git a/tests/regress/mcsat/issue400.smt2.gold b/tests/regress/mcsat/issue400.smt2.gold
new file mode 100644
index 000000000..0d653d741
--- /dev/null
+++ b/tests/regress/mcsat/issue400.smt2.gold
@@ -0,0 +1,2 @@
+sat
+
diff --git a/tests/regress/mcsat/issue400.smt2.options b/tests/regress/mcsat/issue400.smt2.options
new file mode 100644
index 000000000..c326533a7
--- /dev/null
+++ b/tests/regress/mcsat/issue400.smt2.options
@@ -0,0 +1 @@
+--mcsat --incremental

From 9811212522de72c621c5002a2530e8937a94fb84 Mon Sep 17 00:00:00 2001
From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com>
Date: Mon, 11 Mar 2024 23:50:38 -0700
Subject: [PATCH 3/4] proper fix

---
 src/mcsat/preprocessor.c | 45 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 44 insertions(+), 1 deletion(-)

diff --git a/src/mcsat/preprocessor.c b/src/mcsat/preprocessor.c
index 0db5e5761..04fe15489 100644
--- a/src/mcsat/preprocessor.c
+++ b/src/mcsat/preprocessor.c
@@ -592,6 +592,50 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
       break;
     }
 
+    case BV_ARRAY:
+    {
+      composite_term_t* desc = get_composite(terms, current_kind, current);
+      bool children_done = true;
+      bool children_same = true;
+
+      n = desc->arity;
+
+      ivector_t children;
+      init_ivector(&children, n);
+
+      for (i = 0; i < n; ++ i) {
+        term_t child = desc->arg[i];
+        term_t child_pre = preprocessor_get(pre, child);
+        if (child_pre == NULL_TERM) {
+          children_done = false;
+          ivector_push(pre_stack, child);
+        } else {
+          if (is_arithmetic_literal(terms, child_pre)) {
+            // purify if arithmetic literal, i.e. a = 0 where a is of integer type
+            child_pre = preprocessor_purify(pre, child_pre, out);
+          }
+          if (child_pre != child) {
+            children_same = false;
+          }
+        }
+        if (children_done) {
+          ivector_push(&children, child_pre);
+        }
+      }
+
+      if (children_done) {
+        if (children_same) {
+          current_pre = current;
+        } else {
+          current_pre = mk_composite(pre, current_kind, n, children.data);
+        }
+      }
+
+      delete_ivector(&children);
+
+      break;
+    }
+
     case ARITH_ABS:
     {
       term_t arg = arith_abs_arg(terms, current);
@@ -894,7 +938,6 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is
     case ARITH_RDIV:         // regular division (/ x y)
     case ARITH_IDIV:         // division: (div x y) as defined in SMT-LIB 2
     case ARITH_MOD:          // remainder: (mod x y) is y - x * (div x y)
-    case BV_ARRAY:           // bit array
     case UPDATE_TERM:        // update array
     {
       composite_term_t* desc = get_composite(terms, current_kind, current);

From 99590ec210dd1784f8940c99bc1f34c707223e15 Mon Sep 17 00:00:00 2001
From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com>
Date: Mon, 11 Mar 2024 23:51:13 -0700
Subject: [PATCH 4/4] typo

---
 tests/regress/mcsat/issue400.smt2.gold | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tests/regress/mcsat/issue400.smt2.gold b/tests/regress/mcsat/issue400.smt2.gold
index 0d653d741..6b8a2c3d2 100644
--- a/tests/regress/mcsat/issue400.smt2.gold
+++ b/tests/regress/mcsat/issue400.smt2.gold
@@ -1,2 +1 @@
 sat
-