diff --git a/src/ast/sls/sls_arith_clausal.cpp b/src/ast/sls/sls_arith_clausal.cpp
index 45ef15470..f42796419 100644
--- a/src/ast/sls/sls_arith_clausal.cpp
+++ b/src/ast/sls/sls_arith_clausal.cpp
@@ -281,7 +281,7 @@ namespace sls {
                     tout << mk_bounded_pp(ctx.atom(bv), a.m) << "\n";
                     ctx.display(tout););
                 }
-                VERIFY(!a.get_ineq(bv) || a.get_ineq(bv)->is_true() == ctx.is_true(bv));
+                // VERIFY(!a.get_ineq(bv) || a.get_ineq(bv)->is_true() == ctx.is_true(bv));
             });
     }