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)));
             }
         }