mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

remove deprecated comments about bv2int/int2bv being treated as uninterpreted, raise in #1481

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-12 13:07:09 -08:00
parent e1100af52c
commit 792fdb915f
1 changed files with 2 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/api/z3_api.h
View file

@ -2857,9 +2857,8 @@ extern "C" {
/** /**
\brief Create an \c n bit bit-vector from the integer argument \c t1. \brief Create an \c n bit bit-vector from the integer argument \c t1.
NB. This function is essentially treated as uninterpreted. The resulting bit-vector has \c n bits, where the i'th bit (counting
So you cannot expect Z3 to precisely reflect the semantics of this function from 0 to \c n-1) is 1 if \c (t1 div 2^i) mod 2 is 1.
when solving constraints with this function.
The node \c t1 must have integer sort. The node \c t1 must have integer sort.
@ -2874,9 +2873,6 @@ extern "C" {
and in the range \ccode{[0..2^N-1]}, where N are the number of bits in \c t1. and in the range \ccode{[0..2^N-1]}, where N are the number of bits in \c t1.
If \c is_signed is true, \c t1 is treated as a signed bit-vector. If \c is_signed is true, \c t1 is treated as a signed bit-vector.
This function is essentially treated as uninterpreted.
So you cannot expect Z3 to precisely reflect the semantics of this function
when solving constraints with this function.
The node \c t1 must have a bit-vector sort. The node \c t1 must have a bit-vector sort.