mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-22 20:32:05 +00:00
Code Activity

n/a

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-07 19:47:55 -08:00
parent bb03f1f1ec
commit f3fa6fdb84
2 changed files with 2 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/polysat_core.cpp
View file

@ -267,9 +267,7 @@ namespace polysat {
break; break;
} }
} }
} }
throw default_exception("nyi");
} }
void core::propagate_unsat_core() { void core::propagate_unsat_core() {

3
src/sat/smt/polysat_solver.cpp
View file

@ -152,8 +152,7 @@ namespace polysat {
auto sc = m_core.eq(p, q); auto sc = m_core.eq(p, q);
m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2)); m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2));
ctx.push(value_trail<unsigned>(m_var_eqs_head)); ctx.push(value_trail<unsigned>(m_var_eqs_head));
unsigned index = 0; unsigned index = m_core.register_constraint(sc, solver_assertion(v1, v2));
// unsigned index = m_core.register_constraint(sc);
m_core.assign_eh(index, sc, dependency(m_var_eqs_head, s().scope_lvl())); m_core.assign_eh(index, sc, dependency(m_var_eqs_head, s().scope_lvl()));
m_var_eqs_head++; m_var_eqs_head++;
} }