From bdf7de170394b920711d033cf14af97708f783a8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jan=20Vran=C3=BD?= <82951+janvrany@users.noreply.github.com> Date: Thu, 17 Mar 2022 02:28:03 +0000 Subject: [PATCH] Care for root index being undefine while calling Z3_algebraic_get_i() (#5888) In some cases, Z3_algebraic_get_i() returned 0. For example, in the following Python snippet, the last assert would fail: import z3 x = z3.Real('x') s = z3.Solver() s.add( (x * x) - 2 == 0, x <= 0) s.check() val_x = s.model().get_interp(x) assert val_x.index() == 1 The problem was that `algebraic_numbers::manager::imp::get_i()` did not check whether the root index was properly initialized. This commit fixes this issue by checking whether root index is initialized the same way various other routines do. Fixes issue #5807. Signed-off-by: Jan Vrany --- src/math/polynomial/algebraic_numbers.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 5244de82c..57ce00e2c 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -2013,6 +2013,11 @@ namespace algebraic_numbers { } else { algebraic_cell * c = a.to_algebraic(); + if (c->m_i == 0) { + // undefined + c->m_i = upm().get_root_id(c->m_p_sz, c->m_p, lower(c)) + 1; + } + SASSERT(c->m_i > 0); return c->m_i; } }