fix #3966

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 15, 2020 · d0f9405 · d0f9405
1 parent 068f65c
commit d0f9405
Showing 1 changed file with 8 additions and 14 deletions.
diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -258,6 +258,7 @@ class reduce_invertible_tactic : public tactic {
     // TBD: could be made to be recursive, by walking multiple layers of parents.
 
     bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var = 0) {
+        rational r;
         if (m_parents.size() <= v->get_id()) {
             return false;
         }
@@ -308,7 +309,6 @@ class reduce_invertible_tactic : public tactic {
             if (!rest) return false;
 
             // so far just support numeral
-            rational r;
             if (!m_bv.is_numeral(rest, r)) 
                 return false;
 
@@ -373,6 +373,8 @@ class reduce_invertible_tactic : public tactic {
                 }
             }
             if (!rest) return false;
+            if (!m_arith.is_numeral(rest, r) || r.is_zero())
+                return false;
             expr_ref zero(m_arith.mk_real(0), m);
             new_v = m.mk_ite(m.mk_eq(zero, rest), zero, v);
             if (mc) {
@@ -385,24 +387,16 @@ class reduce_invertible_tactic : public tactic {
 
 
         expr* e1 = nullptr, *e2 = nullptr;
-
-        // t / v -> if t = 0 then 0 else v 
-        // inverse: t = 0 then 1 else v / t
-        if (m_arith.is_div(p, e1, e2) && e2 == v) {
-            expr_ref zero(m_arith.mk_real(0), m);
-            new_v = m.mk_ite(m.mk_eq(zero, e1), zero, v);
+
+        // v / t unless t != 0
+        if (m_arith.is_div(p, e1, e2) && e1 == v && m_arith.is_numeral(e2, r) && !r.is_zero()) {
+            new_v = v;
             if (mc) {
                 ensure_mc(mc);
-                expr_ref def(m.mk_ite(m.mk_eq(zero, e1), m_arith.mk_real(1), m_arith.mk_div(e1, v)), m);
-                (*mc)->add(v, def);
+                (*mc)->add(v, m_arith.mk_mul(e1, e2));
             }
             return true;
         }
-
-        // v / t unless t != 0
-        if (m_arith.is_div(p, e1, e2) && e1 == v) {
-            return false;
-        }
 
         if (m.is_eq(p, e1, e2)) {
             TRACE("invertible_tactic", tout << mk_pp(v, m) << "\n";);