diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp
index 061a51220..fe3294e4c 100644
--- a/src/tactic/bv/bit_blaster_model_converter.cpp
+++ b/src/tactic/bv/bit_blaster_model_converter.cpp
@@ -21,6 +21,7 @@ Notes:
 #include "tactic/model_converter.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp.h"
 #include "ast/ast_util.h"
 
 /**
@@ -40,9 +41,7 @@ struct bit_blaster_model_converter : public model_converter {
         obj_map<func_decl, expr*> const & const2bits, 
         ptr_vector<func_decl> const& newbits):
         m_vars(m), m_bits(m), m_newbits(m) {
-        for (auto const& kv : const2bits) {
-            func_decl * v = kv.m_key;
-            expr * bits   = kv.m_value;
+        for (auto const& [v, bits] : const2bits) {
             SASSERT(!TO_BOOL || is_app_of(bits, m.get_family_id("bv"), OP_MKBV));
             SASSERT(TO_BOOL  || is_app_of(bits, m.get_family_id("bv"), OP_CONCAT));
             m_vars.push_back(v);
diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp
index 0fc38f2db..d3f19d1bd 100644
--- a/src/tactic/bv/bv1_blaster_tactic.cpp
+++ b/src/tactic/bv/bv1_blaster_tactic.cpp
@@ -37,7 +37,7 @@ class bv1_blaster_tactic : public tactic {
         bv_util                            m_util;
         obj_map<func_decl, expr*>          m_const2bits;
         ptr_vector<func_decl>              m_newbits;
-        expr_ref_vector                    m_saved;
+        ast_ref_vector                     m_saved;
         expr_ref                           m_bit1;
         expr_ref                           m_bit0;
 
@@ -108,9 +108,11 @@ class bv1_blaster_tactic : public tactic {
             for (unsigned i = 0; i < bv_size; i++) {
                 bits.push_back(m().mk_fresh_const(nullptr, b));
                 m_newbits.push_back(to_app(bits.back())->get_decl());
+                m_saved.push_back(m_newbits.back());
             }
             r = butil().mk_concat(bits.size(), bits.data());
             m_saved.push_back(r);
+            m_saved.push_back(f);
             m_const2bits.insert(f, r);
             result = r;
         }