diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp
index 9a423452f..5958a9d38 100644
--- a/src/tactic/bv/bit_blaster_model_converter.cpp
+++ b/src/tactic/bv/bit_blaster_model_converter.cpp
@@ -148,8 +148,8 @@ struct bit_blaster_model_converter : public model_converter {
             for (expr* bit : *to_app(bs)) {
                 func_decl * bit_decl = to_app(bit)->get_decl();
                 expr * bit_val = old_model->get_const_interp(bit_decl);
-                CTRACE("bv", !bit_val, tout << mk_pp(bit, m()) << " " << *old_model << "\n");
-                SASSERT(bit_val);
+                if (!bit_val) 
+                    bit_val = m().mk_false();                
                 vals.push_back(bit_val);
             }
             if (TO_BOOL)