From f1a1267d4c6cbdf25e36774f329a892921bd394f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 17 Apr 2015 16:08:53 +0100 Subject: [PATCH 1/3] Added missing notes on fpToIEEEBV in Python. --- src/api/python/z3.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index cf4bcd87c..ce1cc2103 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8480,7 +8480,13 @@ def fpToReal(x): return ArithRef(Z3_mk_fpa_to_real(x.ctx_ref(), x.ast), x.ctx) def fpToIEEEBV(x): - """Create a Z3 floating-point conversion expression, from floating-point expression to IEEE bit-vector. + """\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. + + The size of the resulting bit-vector is automatically determined. + + Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion + knows only one NaN and it will always produce the same bit-vector represenatation of + that NaN. >>> x = FP('x', FPSort(8, 24)) >>> y = fpToIEEEBV(x) From 7d88d045149ae10da2609455be1a608ec82f1564 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Apr 2015 00:55:30 +0200 Subject: [PATCH 2/3] fix crash reported by Jojanovich, github issue 45' Signed-off-by: Nikolaj Bjorner --- src/tactic/arith/fix_dl_var_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 693066ee1..6d9f98f39 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -282,7 +282,7 @@ class fix_dl_var_tactic : public tactic { expr_ref new_curr(m); proof_ref new_pr(m); unsigned size = g->size(); - for (unsigned idx = 0; idx < size; idx++) { + for (unsigned idx = 0; !g->inconsistent() && idx < size; idx++) { expr * curr = g->form(idx); m_rw(curr, new_curr, new_pr); if (produce_proofs) { From 6c1a5390ef202499d86fdb41415dada7db1c9d76 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Apr 2015 10:20:06 +0200 Subject: [PATCH 3/3] fix big-int bug for shift amounts, github issue 44, reported by Dejan Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index b579d698e..a30c0d32c 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -902,6 +902,7 @@ template void bit_blaster_tpl::mk_shl(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { numeral k; if (is_numeral(sz, b_bits, k)) { + if (k > numeral(sz)) k = numeral(sz); unsigned n = static_cast(k.get_int64()); if (n >= sz) n = sz; unsigned pos; @@ -947,6 +948,7 @@ template void bit_blaster_tpl::mk_lshr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { numeral k; if (is_numeral(sz, b_bits, k)) { + if (k > numeral(sz)) k = numeral(sz); unsigned n = static_cast(k.get_int64()); unsigned pos = 0; for (unsigned i = n; i < sz; pos++, i++) @@ -989,6 +991,7 @@ template void bit_blaster_tpl::mk_ashr(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { numeral k; if (is_numeral(sz, b_bits, k)) { + if (k > numeral(sz)) k = numeral(sz); unsigned n = static_cast(k.get_int64()); unsigned pos = 0; for (unsigned i = n; i < sz; pos++, i++)