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;