mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-03-20 21:27:00 -07:00
parent 70d2263a85
commit f840d5d965
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/nlsat_explain.cpp
View file

@ -1094,12 +1094,12 @@ namespace nlsat {
if (x < max_x) if (x < max_x)
add_cell_lits(ps, x); add_cell_lits(ps, x);
while (true) { while (true) {
TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
display(tout, ps); tout << "\n";);
if (all_univ(ps, x) && m_todo.empty()) { if (all_univ(ps, x) && m_todo.empty()) {
m_todo.reset(); m_todo.reset();
break; break;
} }
TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
display(tout, ps); tout << "\n";);
add_lc(ps, x); add_lc(ps, x);
psc_discriminant(ps, x); psc_discriminant(ps, x);
psc_resultant(ps, x); psc_resultant(ps, x);