From 341f7ceb1732c8abd617b158087821c396c0c8ec Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 19 Jun 2018 13:19:48 -0700
Subject: [PATCH] remove quantified lemmas for idiv/mod

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_arith_core.h | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index a052d1f98..cbd41f08c 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -543,6 +543,10 @@ namespace smt {
                 }
 #endif
             }
+#if 0
+            // e-matching is too restrictive for multiplication.
+            // also suffers from use-after free so formulas have to be pinned in solver.
+            // 
             if (!m_util.is_numeral(divisor)) {
                 //
                 // forall x . (or (= y 0) (= (div (* x y) y) x))
@@ -568,6 +572,7 @@ namespace smt {
                 pr = m.mk_asserted(fml);
                 ctx.internalize_assertion(fml, pr, 0);
             }
+#endif
         }
     }