mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

defer ho-matching to lazy mam

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-07 14:59:50 -07:00
parent 165a4a42bc
commit 7040a74d1a
1 changed files with 1 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_quantifier.cpp
View file

@ -867,10 +867,7 @@ namespace smt {
<< " compiled=" << (p1 != mp)
<< " p1=" << mk_pp(p1, m) << "\n");
if (p1 != mp) {
if (!unary && j >= num_eager_multi_patterns)
m_lazy_mam->add_pattern(q1, p1);
else
m_mam->add_pattern(q1, p1);
m_lazy_mam->add_pattern(q1, p1);
}
}
if (!unary)