From f00c026272619cf2d7e78117ce21321dfe0b5780 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Mar 2020 17:51:00 +0100 Subject: [PATCH] fix #3173 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 113f3da3c..842c2d907 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1923,6 +1923,8 @@ public: TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";); continue; } + if (!can_get_ivalue(v)) + continue; lp::impq val_v = get_ivalue(v); if (val_v.y.is_zero() && val_v.x == div(r1.x, r2)) continue;