From 7eaa5562d8a94452e5eaff2a25c5386e77cec723 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Jan 2013 12:51:03 -0800 Subject: [PATCH] Fix http://z3.codeplex.com/workitem/19 Signed-off-by: Leonardo de Moura --- RELEASE_NOTES | 2 ++ src/cmd_context/check_logic.cpp | 3 +++ 2 files changed, 5 insertions(+) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index a2257c610..3145d3b62 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -55,6 +55,8 @@ Version 4.3.2 - Fixed bug reported at http://stackoverflow.com/questions/14307692/unknown-when-using-defs +- Relax check_logic procedure. Now, it accepts coercions (to_real) automatically introduced by Z3. (Thanks to Paul Jackson). This is a fix for http://z3.codeplex.com/workitem/19. + Version 4.3.1 ============= diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index 820ef59a4..dfee148b5 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -228,6 +228,9 @@ struct check_logic::imp { bool is_int(expr * t) { if (m_a_util.is_uminus(t)) t = to_app(t)->get_arg(0); + // Take care of coercions automatically added by Z3 + if (m_a_util.is_to_real(t)) + t = to_app(t)->get_arg(0); return m_a_util.is_numeral(t); }