mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

print roots as part of test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-24 15:28:51 -07:00
parent af51d98a32
commit 69783db5e8
2 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polynomial/algebraic_numbers.cpp
View file

@ -575,7 +575,6 @@ namespace algebraic_numbers {
auto& a = r[i]; auto& a = r[i];
for (unsigned j = 0; j < r.size(); ++j) { for (unsigned j = 0; j < r.size(); ++j) {
auto& b = r[j]; auto& b = r[j];
bool ltab = lt(a, b);
for (unsigned k = 0; k < r.size(); ++k) { for (unsigned k = 0; k < r.size(); ++k) {
auto& c = r[k]; auto& c = r[k];
bool b_lt_a = lt(b, a); bool b_lt_a = lt(b, a);

4
src/test/algebraic.cpp
View file

@ -602,6 +602,10 @@ static void tst_sturm() {
b = rs1[3]; b = rs1[3];
am.isolate_roots(q, rs2); am.isolate_roots(q, rs2);
c = rs2[3]; c = rs2[3];
display_anums(std::cout, rs1);
display_anums(std::cout, rs2);
am.display_decimal(std::cout << "a:", a) << "\n"; am.display_decimal(std::cout << "a:", a) << "\n";
am.display_interval(std::cout << "a:", a) << "\n"; am.display_interval(std::cout << "a:", a) << "\n";
am.display_root(std::cout << "a:", a) << "\n"; am.display_root(std::cout << "a:", a) << "\n";