mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-09 17:31:57 +00:00
Code Activity

call setup_assignment_solver instead of setup_solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-02 08:58:15 -07:00
parent ba378ed341
commit 874e8b3cfa
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/nra_solver.cpp
View file

@ -387,10 +387,10 @@ struct solver::imp {
lbool check_assignment() { lbool check_assignment() {
IF_VERBOSE(1, verbose_stream() << "nra::solver::check_assignment\n";); IF_VERBOSE(1, verbose_stream() << "nra::solver::check_assignment\n";);
setup_solver(); setup_assignment_solver();
lbool r = l_undef; lbool r = l_undef;
statistics &st = m_nla_core.lp_settings().stats().m_st; statistics &st = m_nla_core.lp_settings().stats().m_st;
nlsat::literal_vector clause; nlsat::literal_vector clause;
try { try {
nlsat::assignment rvalues(m_nlsat->am()); nlsat::assignment rvalues(m_nlsat->am());
for (auto [j, x] : m_lp2nl) { for (auto [j, x] : m_lp2nl) {