diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index a3ee5408c..fe5372e7a 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1272,6 +1272,8 @@ namespace arith {
             for (literal& c : m_core)
                 c.neg();
             DEBUG_CODE(for (literal c : m_core) { SASSERT(s().value(c) != l_true); });
+
+            for (literal c : m_core) { VERIFY(s().value(c) != l_true); }
             
             add_redundant(m_core, explain(ty));
         }