From ec6e2139dd96ae10ba55103565bbda28d3984d1b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Jan 2024 17:49:29 -0800 Subject: [PATCH] fix unsound merge Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_bv_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index 3ae04231a..155faf575 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/src/ast/euf/euf_bv_plugin.cpp @@ -171,7 +171,7 @@ namespace euf { if (is_extract(p, lo, hi)) { auto val_p = mod2k(machine_div2k(val_x, lo), hi - lo + 1); - push_merge(bv.mk_extract(x->get_interpreted(), lo, hi), mk_value(val_p, width(p))); + push_merge(mk_extract(x->get_interpreted(), lo, hi), mk_value(val_p, width(p))); } }