From a9550a389902bb6dbf09f8b7f5d190f8b60c4fab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Dec 2023 19:47:55 -0800 Subject: [PATCH] n/a --- src/sat/smt/polysat_core.cpp | 4 +--- src/sat/smt/polysat_solver.cpp | 3 +-- 2 files changed, 2 insertions(+), 5 deletions(-) diff --git a/src/sat/smt/polysat_core.cpp b/src/sat/smt/polysat_core.cpp index b97a223f7..b7ff2e740 100644 --- a/src/sat/smt/polysat_core.cpp +++ b/src/sat/smt/polysat_core.cpp @@ -267,9 +267,7 @@ namespace polysat { break; } } - } - - throw default_exception("nyi"); + } } void core::propagate_unsat_core() { diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp index e3aff6e5f..35b177754 100644 --- a/src/sat/smt/polysat_solver.cpp +++ b/src/sat/smt/polysat_solver.cpp @@ -152,8 +152,7 @@ namespace polysat { 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)); ctx.push(value_trail(m_var_eqs_head)); - unsigned index = 0; -// unsigned index = m_core.register_constraint(sc); + unsigned index = m_core.register_constraint(sc, solver_assertion(v1, v2)); m_core.assign_eh(index, sc, dependency(m_var_eqs_head, s().scope_lvl())); m_var_eqs_head++; }