From feff1f7f9691a65c98ebe7d160d86c2668b0bf15 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 2 Oct 2019 14:40:11 -0700
Subject: [PATCH] fix #2609

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/model_evaluator.cpp    | 1 -
 src/qe/qsat.cpp                  | 4 ++--
 src/tactic/arith/probe_arith.cpp | 3 +++
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index fed7d768b..35c637ade 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -342,7 +342,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
             result = m_au.mk_int(0);
             return BR_DONE;
         }
-
         return BR_FAILED;
     }
 
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index fcac507fe..0a016f82d 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -503,8 +503,8 @@ namespace qe {
             if (is_uninterp_const(a)) { // TBD generalize for uninterpreted functions.
                 vars.push_back(a);
             }
-            for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                todo.push_back(a->get_arg(i));
+            for (expr* arg : *a) {
+                todo.push_back(arg);
             }
         }
     }
diff --git a/src/tactic/arith/probe_arith.cpp b/src/tactic/arith/probe_arith.cpp
index 922b505db..4f307c9f8 100644
--- a/src/tactic/arith/probe_arith.cpp
+++ b/src/tactic/arith/probe_arith.cpp
@@ -465,6 +465,7 @@ struct is_non_nira_functor {
         if (!compatible_sort(n))
             throw_found(n);
         family_id fid = n->get_family_id();
+        rational r;
         if (fid == m.get_basic_family_id())
             return; 
         if (fid == u.get_family_id()) {
@@ -484,6 +485,8 @@ struct is_non_nira_functor {
             case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
                 if (m_linear && !u.is_numeral(n->get_arg(1)))
                     throw_found(n); 
+                if (m_linear && u.is_numeral(n->get_arg(1), r) && r.is_zero())
+                    throw_found(n); 
                 if (!is_ground(n->get_arg(0)) || !is_ground(n->get_arg(1))) 
                     throw_found(n);
                 return;