mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-30 09:58:46 +00:00
Code Activity

#5518

Browse source 
@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.
This commit is contained in:
Nikolaj Bjorner 2021-08-31 14:52:45 -07:00
parent 34c8f598a5
commit ab2baa764c
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/fpa_decl_plugin.cpp
View file

@ -927,9 +927,8 @@ bool fpa_decl_plugin::is_unique_value(app* e) const {
case OP_FPA_NUM: /* see NaN */ case OP_FPA_NUM: /* see NaN */
return false; return false;
case OP_FPA_FP: case OP_FPA_FP:
return m_manager->is_unique_value(e->get_arg(0)) && return false; /*No; generally not because of clashes with +oo, -oo, +zero, -zero, NaN */
m_manager->is_unique_value(e->get_arg(1)) && // a refinement would require to return true only if there is no clash with these cases.
m_manager->is_unique_value(e->get_arg(2));
default: default:
return false; return false;
} }