mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

remove quantified lemmas for idiv/mod

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-19 13:19:48 -07:00
parent b5614bc93e
commit 341f7ceb17
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_arith_core.h
View file

@ -543,6 +543,10 @@ namespace smt {
} }
#endif #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)) { if (!m_util.is_numeral(divisor)) {
// //
// forall x . (or (= y 0) (= (div (* x y) y) x)) // forall x . (or (= y 0) (= (div (* x y) y) x))
@ -568,6 +572,7 @@ namespace smt {
pr = m.mk_asserted(fml); pr = m.mk_asserted(fml);
ctx.internalize_assertion(fml, pr, 0); ctx.internalize_assertion(fml, pr, 0);
} }
#endif
} }
} }