From af5fd1014f453976c9b34d053b0ca0cb70780c01 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 8 Aug 2021 17:33:49 -0700
Subject: [PATCH] #5460

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

diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index 7e41aeb46..b1398c836 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -418,6 +418,7 @@ namespace arith {
             expr* p = nullptr, * q = nullptr;
             VERIFY(a.is_idiv(n, p, q));
             theory_var v1 = internalize_def(p);
+            ensure_column(v1);
             lp::impq r1 = get_ivalue(v1);
             rational r2;