From 2edab50f5301f779e52ef543dea5addb9d0da725 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 2 Mar 2020 20:53:56 -0800
Subject: [PATCH] fix #3099

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

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2ad825505..cd32c011d 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -955,6 +955,9 @@ class theory_lra::imp {
         }
         else {
             init_left_side(st);
+            if (m_left_side.empty()) {
+                return get_zero(a.is_int(term));
+            }
             theory_var v = mk_var(term);
             lpvar vi = get_lpvar(v);
             TRACE("arith", tout << mk_pp(term, m) << " v" << v << " vi " << vi << "\n";);