From d1f8b06ec4e5cc0c9e3b022c52a3e8662d0f2f71 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie@cmu.edu>
Date: Wed, 11 May 2016 22:33:41 -0400
Subject: [PATCH] bug fix in model_evaluator for array equality

---
 src/model/model_evaluator.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index e67e3cb5e..5cc3d27ab 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -150,7 +150,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
                     st = m_f_rw.mk_eq_core(args[0], args[1], result);
                 else if (s_fid == m_seq_rw.get_fid())
                     st = m_seq_rw.mk_eq_core(args[0], args[1], result);
-                else if (fid == m_ar_rw.get_fid())
+                else if (s_fid == m_ar_rw.get_fid())
                     st = mk_array_eq(args[0], args[1], result);
                 if (st != BR_FAILED)
                     return st;