From f920079aacfe272db89b7efcc64a3d2ddfe0386b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Jun 2021 16:30:52 -0700
Subject: [PATCH] #5324

---
 src/sat/smt/arith_axioms.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index 8a7fa431b..7e41aeb46 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -331,6 +331,8 @@ namespace arith {
     }
 
     void solver::new_diseq_eh(euf::th_eq const& e) {
+        ensure_column(e.v1());
+        ensure_column(e.v2());
         m_delayed_eqs.push_back(std::make_pair(e, false));
         ctx.push(push_back_vector<svector<std::pair<euf::th_eq, bool>>>(m_delayed_eqs));
     }