mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-30 07:49:53 +00:00
Code Activity

unsound state

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-16 09:17:21 -10:00
parent 55150f36c5
commit 9fc7e6cfe0
1 changed files with 0 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/nlsat/levelwise.cpp
View file

@ -949,9 +949,6 @@ namespace nlsat {
::nlsat::display(tout, m_solver, a) << "\n";
::nlsat::display(tout,m_solver, b)<< "\nresultant:"; ::nlsat::display(tout, m_solver, r) << "\n");
if (is_zero(r)) {
std::cout << "resultant of(" << pair.first << "," << pair.second << "):";
::nlsat::display(std::cout << "\n", m_solver, a) << "\n";
::nlsat::display(std::cout,m_solver, b)<< "\nresultant:"; ::nlsat::display(std::cout, m_solver, r) << "\n";
SASSERT(same_polynomial_up_to_constant(a, b));
continue;
}