From 33c81524d2290eda1b55a1a3dfb7af2a28bb03a3 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 31 Jul 2017 15:57:29 -0400
Subject: [PATCH] optionally disable propagate variable equivalences in
 interp_tail_simplifier

---
 src/muz/transforms/dl_mk_interp_tail_simplifier.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
index 64a2a2aca..1559f4f65 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
@@ -27,6 +27,7 @@ Revision History:
 #include "muz/transforms/dl_mk_interp_tail_simplifier.h"
 #include "ast/ast_util.h"
 
+#include "fixedpoint_params.hpp"
 namespace datalog {
 
     // -----------------------------------
@@ -397,6 +398,8 @@ namespace datalog {
     }
 
     bool mk_interp_tail_simplifier::propagate_variable_equivalences(rule * r, rule_ref& res) {
+      if (!m_context.get_params ().xform_tail_simplifier_pve ())
+        return false;
         unsigned u_len = r->get_uninterpreted_tail_size();
         unsigned len = r->get_tail_size();
         if (u_len == len) {