Skip to content

Commit

Permalink
fix bug with handling theory symbols of bit-vector type. Happens for …
Browse files Browse the repository at this point in the history
…data-type accessors. Reported by Clemens Eisenhofer

Signed-off-by: Nikolaj Bjorner <[email protected]>
  • Loading branch information
NikolajBjorner committed Jan 27, 2025
1 parent 09e84e0 commit 7ffed86
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/ast/sls/sls_bv_eval.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down

0 comments on commit 7ffed86

Please sign in to comment.