mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 08:23:17 +00:00
Code Activity

#5338 #5349

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-16 16:01:34 -05:00
parent f95d0b7216
commit 29a2838bc9
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/tactic/arith/probe_arith.cpp
View file

@ -497,6 +497,7 @@ struct is_non_nira_functor {
if (m_linear && u.is_numeral(n->get_arg(1), r) && r.is_zero()) if (m_linear && u.is_numeral(n->get_arg(1), r) && r.is_zero())
throw_found(n); throw_found(n);
if (m_linear && u.is_numeral(n->get_arg(1), r) && !r.is_zero()) 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))) if (!is_ground(n->get_arg(0)) || !is_ground(n->get_arg(1)))
throw_found(n); throw_found(n);
return; return;