From 6bdf377e11e6ba1969ddd87aa766eb7b1142751a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 28 Mar 2021 21:20:05 -0700
Subject: [PATCH] remove unneeded assertion fix #5131

---
 src/smt/theory_lra.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 689fa0187..216afc1b9 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3072,7 +3072,6 @@ public:
             return;
         if (x->get_root() == y->get_root())
             return;
-        SASSERT(a.is_numeral(y->get_expr()));
         reset_evidence();
         set_evidence(ci1, m_core, m_eqs);
         set_evidence(ci2, m_core, m_eqs);