diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp
index 33c998041..421966377 100644
--- a/src/sat/smt/intblast_solver.cpp
+++ b/src/sat/smt/intblast_solver.cpp
@@ -437,10 +437,12 @@ namespace intblast {
                     continue;
                 if (sib->get_arg(0)->get_root() == r1)
                     continue;
-		auto a = eq_internalize(n, sib);
-		auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
-		ctx.mark_relevant(a);
-		ctx.mark_relevant(b);
+                if (bv.get_bv_size(r1->get_expr()) != bv.get_bv_size(sib->get_arg(0)->get_expr()))
+                    continue;
+                auto a = eq_internalize(n, sib);
+                auto b = eq_internalize(sib->get_arg(0), n->get_arg(0));
+                ctx.mark_relevant(a);
+                ctx.mark_relevant(b);
                 add_clause(~a, b, nullptr);
                 return sat::check_result::CR_CONTINUE;
             }