From eae17a43a2dc66b99d12c7596044b82b933760fa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 5 Feb 2016 11:00:17 +0000
Subject: [PATCH] Fix #430: disable rewriting of concatentations with constants
 because it breaks equality propagation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/solve_eqs_tactic.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 1923869a4..f23d874a6 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -111,6 +111,7 @@ class solve_eqs_tactic : public tactic {
                 if (m_produce_proofs) {
                     pr = m().mk_commutativity(m().mk_eq(lhs, rhs));
                 }
+                return true;
             }
             return false;
         }