mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
janitor services
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
38176256c4
commit
f5cd4e3ac0
|
@ -140,6 +140,7 @@ class interval_tester {
|
|||
std::cerr << l(-10, true) << "\n";
|
||||
std::cerr << r(10, true) << "\n";
|
||||
std::cerr << b(2, 10) << "\n";
|
||||
#if 0
|
||||
std::cerr << wd(b(-5, 5, true, false, 1, 2) * b(-5, 5, false, true, 3, 4)) << "\n";
|
||||
std::cerr << wd(l(2, false, 1) / b(2, 6, false, false, 2, 3)) << "\n";
|
||||
std::cerr << wd(expt(b(-2, 3, true, false, 1, 2), 2)) << "\n";
|
||||
|
@ -148,6 +149,7 @@ class interval_tester {
|
|||
std::cerr << wd(expt(b(0, 3, true, false, 1, 2), 2)) << "\n";
|
||||
std::cerr << wd(expt(b(-4, -2, true, false, 1, 2), 2)) << "\n";
|
||||
std::cerr << b(2, 10, false, false, 1, 2) << " * " << l(10, false, 3).inv() << " = " << wd(b(2, 10, false, false, 1, 2) / l(10, false, 3)) << "\n";
|
||||
#endif
|
||||
std::cerr << b(-2, -1, false, true) << " * " << b(-3,0) << " = "; std::cerr.flush();
|
||||
std::cerr << (b(-2, -1, false, true) * b(-3,0)) << "\n";
|
||||
std::cerr << b(1, 2, true, false) << " * " << b(0,3) << " = "; std::cerr.flush();
|
||||
|
|
Loading…
Reference in a new issue