mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

remove incorrect check for quantifier

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-01 00:04:08 -08:00
parent e5984dd397
commit a96b7d243a
1 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/simplifiers/bit2int.h
View file

@ -34,8 +34,6 @@ public:
proof_ref pr(m); proof_ref pr(m);
for (unsigned idx : indices()) { for (unsigned idx : indices()) {
auto const& d = m_fmls[idx]; auto const& d = m_fmls[idx];
if (!has_quantifiers(d.fml()))
continue;
m_rewriter(d.fml(), r, pr); m_rewriter(d.fml(), r, pr);
m_fmls.update(idx, dependent_expr(m, r, d.dep())); m_fmls.update(idx, dependent_expr(m, r, d.dep()));
} }