From cc001ad6825074743fd62818e40e9dc63c208f26 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 2 Feb 2021 06:16:06 -0800
Subject: [PATCH] fix regression

---
 src/ast/rewriter/enum2bv_rewriter.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
index ff9868735..eb50461a6 100644
--- a/src/ast/rewriter/enum2bv_rewriter.cpp
+++ b/src/ast/rewriter/enum2bv_rewriter.cpp
@@ -99,7 +99,7 @@ struct enum2bv_rewriter::imp {
             }
             else if (m_dt.is_recognizer(f) && reduce_arg(args[0], a0)) {
                 unsigned idx = m_dt.get_recognizer_constructor_idx(f);
-                a1 = value2bv(idx, a0->get_sort());
+                a1 = value2bv(idx, args[0]->get_sort());
                 result = m.mk_eq(a0, a1);
                 return BR_DONE;
             }