Merge pull request #495 from SRI-CSL/mcsat-bv-array-purify

fixes #400

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:
@@ -593,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);

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)

tests/regress/mcsat/issue400.smt2.gold

@@ -0,0 +1 @@
+sat

tests/regress/mcsat/issue400.smt2.options

@@ -0,0 +1 @@
+--mcsat --incremental