From 2c7a39d580194d2f63cfea4b828be22c0c73ec7a Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 31 Jul 2017 16:00:36 -0400
Subject: [PATCH] Optionally blast arrays

This changes the default behavior of always blasting arrays.
The old behavior can be restored using

   fixedpoint.xform.array_blast=true
---
 src/muz/transforms/dl_mk_array_blast.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp
index 373edcd4b..8fe3f0e43 100644
--- a/src/muz/transforms/dl_mk_array_blast.cpp
+++ b/src/muz/transforms/dl_mk_array_blast.cpp
@@ -319,6 +319,9 @@ namespace datalog {
     
     rule_set * mk_array_blast::operator()(rule_set const & source) {
 
+        if (!m_ctx.array_blast ()) {
+            return 0;
+        }
         rule_set* rules = alloc(rule_set, m_ctx);
         rules->inherit_predicates(source);
         rule_set::iterator it = source.begin(), end = source.end();