diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index 47e3ee551..32e64e2b5 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -15,6 +15,8 @@ Author:
 
 --*/
 
+#include "util/cancel_eh.h"
+#include "util/scoped_timer.h"
 #include "ast/ast_util.h"
 #include "ast/scoped_proof.h"
 #include "sat/smt/euf_solver.h"
@@ -242,4 +244,21 @@ namespace arith {
 
         return m.mk_app(symbol(name), args.size(), args.data(), m.mk_proof_sort());
     }
+
+    bool solver::validate_conflict() {
+        scoped_ptr<::solver> vs = mk_smt2_solver(m, ctx.s().params(), symbol::null);
+        for (auto lit : m_core)
+            vs->assert_expr(ctx.literal2expr(lit));
+
+        for (auto [a, b] : m_eqs)
+            vs->assert_expr(m.mk_eq(a->get_expr(), b->get_expr()));
+
+        cancel_eh<reslimit> eh(m.limit());
+        scoped_timer timer(1000, &eh);
+        bool result = l_true != vs->check_sat();
+        CTRACE("arith", !result, vs->display(tout));
+        CTRACE("arith", !result, s().display(tout));
+        SASSERT(result);
+        return result;
+    }
 }
diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index ed49092fd..00038cf8b 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -472,7 +472,7 @@ namespace arith {
         bool _has_var = has_var(t);
         mk_enode(t);
         theory_var v = mk_evar(t);
-
+                                      
         if (!_has_var) {
             svector<lpvar> vars;
             for (expr* n : *t) {
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 9b4e40242..b2a466779 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1251,6 +1251,9 @@ namespace arith {
             for (literal c : m_core) tout << c << ": " << literal2expr(c) << "\n";
             for (auto p : m_eqs) tout << ctx.bpp(p.first) << " == " << ctx.bpp(p.second) << "\n";);
 
+        if (ctx.get_config().m_arith_validate)
+            VERIFY(validate_conflict());
+
         if (is_conflict) {
             DEBUG_CODE(
                 for (literal c : m_core) VERIFY(s().value(c) == l_true);
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index cbf4206a9..af9df0798 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -483,6 +483,7 @@ namespace arith {
         arith_proof_hint const* explain_conflict(hint_type ty, sat::literal_vector const& core, euf::enode_pair_vector const& eqs);
         void explain_assumptions(lp::explanation const& e);
 
+        bool validate_conflict();
 
     public:
         solver(euf::solver& ctx, theory_id id);