From 0fc8ebc8ccf1f572973ba6ae6a461087930e1e33 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Apr 2020 18:56:10 -0700
Subject: [PATCH] fix #3683
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/math/polynomial/algebraic_numbers.cpp | 6 +++---
src/math/polynomial/algebraic_params.pyg | 2 +-
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index 0832909b8..1f61c2c22 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -2404,8 +2404,8 @@ namespace algebraic_numbers {
// all remaining variables are assigned.
// the unassigned variable vanished when we replaced the rational values.
DEBUG_CODE({
- for (unsigned i = 0; i < xs.size(); i++) {
- SASSERT(x2v.contains(xs[i]));
+ for (auto x : xs) {
+ SASSERT(x2v.contains(x));
}
});
return;
@@ -2415,7 +2415,7 @@ namespace algebraic_numbers {
polynomial_ref q(ext_pm);
q = p_prime;
polynomial_ref p_y(ext_pm);
- for (unsigned i = 0; i < xs.size() - 1; i++) {
+ for (unsigned i = 0; i + 1 < xs.size(); i++) {
checkpoint();
polynomial::var y = xs[i];
SASSERT(x2v.contains(y));
diff --git a/src/math/polynomial/algebraic_params.pyg b/src/math/polynomial/algebraic_params.pyg
index 92a2f10df..773548494 100644
--- a/src/math/polynomial/algebraic_params.pyg
+++ b/src/math/polynomial/algebraic_params.pyg
@@ -1,5 +1,5 @@
def_module_params('algebraic',
- description='real algebraic number package',
+ description='real algebraic number package. Non-default parameter settings are not supported',
export=True,
params=(('zero_accuracy', UINT, 0, 'one of the most time-consuming operations in the real algebraic number module is determining the sign of a polynomial evaluated at a sample point with non-rational algebraic number values. Let k be the value of this option. If k is 0, Z3 uses precise computation. Otherwise, the result of a polynomial evaluation is considered to be 0 if Z3 can show it is inside the interval (-1/2^k, 1/2^k)'),
('min_mag', UINT, 16, 'Z3 represents algebraic numbers using a (square-free) polynomial p and an isolating interval (which contains one and only one root of p). This interval may be refined during the computations. This parameter specifies whether to cache the value of a refined interval or not. It says the minimal size of an interval for caching purposes is 1/2^16'),