From 792fdb915f7098177e6414e25a59373d3c7b9ca7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 12 Feb 2018 13:07:09 -0800 Subject: [PATCH] remove deprecated comments about bv2int/int2bv being treated as uninterpreted, raise in #1481 Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 5e5b84450b3..ea0c1615f3c 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -2857,9 +2857,8 @@ extern "C" { /** \brief Create an \c n bit bit-vector from the integer argument \c t1. - NB. 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 resulting bit-vector has \c n bits, where the i'th bit (counting + from 0 to \c n-1) is 1 if \c (t1 div 2^i) mod 2 is 1. 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. 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.