btorrewrite: Consider const arrays for apply/update propagations.

Boolector · Jan 14, 2020 · d46fb7b · d46fb7b
1 parent b60a3a1
commit d46fb7b
Showing 1 changed file with 10 additions and 3 deletions.
diff --git a/src/btorrewrite.c b/src/btorrewrite.c
@@ -5029,9 +5029,16 @@ apply_prop_apply_update (Btor *btor, BtorNode *e0, BtorNode *e1)
   /* propagated until 'cur', create apply on 'cur' */
   if (!result)
   {
-    BTOR_INC_REC_RW_CALL (btor);
-    result = btor_node_create_apply (btor, cur, e1);
-    BTOR_DEC_REC_RW_CALL (btor);
+    if (btor_node_is_const_array (cur))
+    {
+      result = btor_node_copy (btor, cur->e[1]);
+    }
+    else
+    {
+      BTOR_INC_REC_RW_CALL (btor);
+      result = btor_node_create_apply (btor, cur, e1);
+      BTOR_DEC_REC_RW_CALL (btor);
+    }
   }
   btor->stats.prop_apply_update += propagations;
   return result;