From 29a2838bc9a9d9667faf17497700a26d9e9f5523 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 16 Jun 2021 16:01:34 -0500
Subject: [PATCH] #5338 #5349

---
 src/tactic/arith/probe_arith.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp
index 24ccfcb9e..179bd6473 100644
--- a/src/tactic/arith/probe_arith.cpp
+++ b/src/tactic/arith/probe_arith.cpp
@@ -497,6 +497,7 @@ struct is_non_nira_functor {
                 if (m_linear && u.is_numeral(n->get_arg(1), r) && r.is_zero())
                     throw_found(n); 
                 if (m_linear && u.is_numeral(n->get_arg(1), r) && !r.is_zero())
+                    return;
                 if (!is_ground(n->get_arg(0)) || !is_ground(n->get_arg(1))) 
                     throw_found(n);
                 return;