From ab2baa764c271d64a21b3c3c1c4c026276c1b2b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Aug 2021 14:52:45 -0700 Subject: [PATCH] #5518 @wintersteiger This example exposes a bug in is_unique_value ``` (assert (= (fp.to_real ((_ to_fp 8 24) (_ bv4286579200 32))) (fp.to_real ((_ to_fp 8 24) (_ bv4286578944 32))))) (check-sat) ``` It returns true for fp representations that map to NaN. It can only return true for fp values that are unique relative to having no other bit-vector representation so not corresponding to an equivalence class of values such as NaN. I am having it return false. If there is a way to refine the test it will catch some earlier inferences. --- src/ast/fpa_decl_plugin.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 941140a82..8d35a2982 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -927,9 +927,8 @@ bool fpa_decl_plugin::is_unique_value(app* e) const { case OP_FPA_NUM: /* see NaN */ return false; case OP_FPA_FP: - return m_manager->is_unique_value(e->get_arg(0)) && - m_manager->is_unique_value(e->get_arg(1)) && - m_manager->is_unique_value(e->get_arg(2)); + return false; /*No; generally not because of clashes with +oo, -oo, +zero, -zero, NaN */ + // a refinement would require to return true only if there is no clash with these cases. default: return false; }