From e32020ba102f6236cbcbc369580e778d206c6af6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 11 Mar 2020 08:32:25 -0700
Subject: [PATCH] fix #3228

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index d9b34861a..a79a486e5 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1905,6 +1905,10 @@ public:
             VERIFY(a.is_idiv(n, p, q));
             theory_var v  = mk_var(n);
             theory_var v1 = mk_var(p);
+            if (!can_get_ivalue(v1))
+                continue;
+            if (!can_get_ivalue(v))
+                continue;
             lp::impq r1 = get_ivalue(v1);
             rational r2;