From 3032c9315d72beb20fc7cfafaae1a243986dd2aa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 23 Jan 2023 14:31:24 -0800 Subject: [PATCH] handle to-real in variable mapping Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/bound_simplifier.h | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/ast/simplifiers/bound_simplifier.h b/src/ast/simplifiers/bound_simplifier.h index 9d6b09955..6977261c5 100644 --- a/src/ast/simplifiers/bound_simplifier.h +++ b/src/ast/simplifiers/bound_simplifier.h @@ -64,9 +64,13 @@ class bound_simplifier : public dependent_expr_simplifier { unsigned v = m_expr2var.get(e->get_id(), UINT_MAX); if (v == UINT_MAX) { v = m_var2expr.size(); - bp.mk_var(v, a.is_int(e)); + expr* core_e = e; + a.is_to_real(e, core_e); + bp.mk_var(v, a.is_int(core_e)); m_expr2var.setx(e->get_id(), v, UINT_MAX); - m_var2expr.push_back(e); + if (e != core_e) + m_expr2var.setx(core_e->get_id(), v, UINT_MAX); + m_var2expr.push_back(core_e); } return v; }