From 1a0f0c16093412a6575802fd0e2583b8b40f2b50 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Dec 2013 20:54:15 -0800 Subject: [PATCH] feat(kernel/normalizer): let normalizer ignore 'undefined' constants Signed-off-by: Leonardo de Moura --- src/kernel/normalizer.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 18261cedf..1ea154337 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -202,10 +202,10 @@ class normalizer::imp { r = lookup(s, var_idx(a)); break; case expr_kind::Constant: { - object const & obj = env()->get_object(const_name(a)); - if (should_unfold(obj, m_unfold_opaque)) { + optional obj = env()->find_object(const_name(a)); + if (obj && should_unfold(*obj, m_unfold_opaque)) { freset reset(m_cache); - r = normalize(obj.get_value(), value_stack(), 0); + r = normalize(obj->get_value(), value_stack(), 0); } else { r = a; }