mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Update inc_sat_solver.cpp

Browse source 
revert local change
This commit is contained in:
Nikolaj Bjorner 2019-12-31 11:55:00 -08:00
parent a7dc50362b
commit 17824df3cd
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -556,7 +556,8 @@ public:
mk_card2bv_tactic(m, m_params), // updates model converter mk_card2bv_tactic(m, m_params), // updates model converter
using_params(mk_simplify_tactic(m), simp2_p), using_params(mk_simplify_tactic(m), simp2_p),
mk_max_bv_sharing_tactic(m), mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m, m_bb_rewriter.get()) mk_bit_blaster_tactic(m, m_bb_rewriter.get()),
using_params(mk_simplify_tactic(m), simp2_p)
); );
while (m_bb_rewriter->get_num_scopes() < m_num_scopes) { while (m_bb_rewriter->get_num_scopes() < m_num_scopes) {
m_bb_rewriter->push(); m_bb_rewriter->push();