From 7ffed8613af40ea75a02e44ee6ccdd6c4499de27 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 27 Jan 2025 08:22:33 -0800
Subject: [PATCH] fix bug with handling theory symbols of bit-vector type.
 Happens for data-type accessors. Reported by Clemens Eisenhofer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/sls/sls_bv_eval.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
index a68a3a633..532cebe42 100644
--- a/src/ast/sls/sls_bv_eval.cpp
+++ b/src/ast/sls/sls_bv_eval.cpp
@@ -315,7 +315,7 @@ namespace sls {
                 val.set(val_el.bits());
             return;
         }
-        if (e->get_family_id() == null_family_id) {
+        if (e->get_family_id() != bv.get_fid()) {
             val.set(wval(e).bits());
             return;
         }