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

fix #5446

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-01 05:09:58 -07:00
parent 490dc66ec2
commit 50f5cafb50
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/arith/fm_tactic.cpp
View file

@ -162,7 +162,7 @@ class fm_tactic : public tactic {
fm_model_converter(ast_manager & _m):m(_m) {} fm_model_converter(ast_manager & _m):m(_m) {}
~fm_model_converter() override { ~fm_model_converter() override {
m.dec_array_ref(m_xs.size(), m_xs.data()); m.dec_array_ref(m_xs.size(), m_xs.data());
vector<clauses>::iterator it = m_clauses.begin(); vector<clauses>::iterator it = m_clauses.begin();
vector<clauses>::iterator end = m_clauses.end(); vector<clauses>::iterator end = m_clauses.end();
for (; it != end; ++it) for (; it != end; ++it)
@ -1598,7 +1598,7 @@ class fm_tactic : public tactic {
report_tactic_progress(":fm-cost", m_counter); report_tactic_progress(":fm-cost", m_counter);
if (!m_inconsistent) { if (!m_inconsistent) {
copy_remaining(); copy_remaining();
m_new_goal->add(concat(g->mc(), m_mc.get())); m_new_goal->add(m_mc.get());
} }
} }
reset_constraints(); reset_constraints();