mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

bugfix for ML example

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-01-08 13:25:14 +00:00
parent 98f750f90d
commit 7e3676e24a
1 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
examples/ml/ml_example.ml
View file

@ -287,16 +287,15 @@ let fpa_example ( ctx : context ) =
(* ((_ to_fp 11 53) #x401c000000000000)) *) (* ((_ to_fp 11 53) #x401c000000000000)) *)
(* ((_ to_fp 11 53) RTZ 1.75 2))) *) (* ((_ to_fp 11 53) RTZ 1.75 2))) *)
(* ((_ to_fp 11 53) RTZ 7.0))) *) (* ((_ to_fp 11 53) RTZ 7.0))) *)
let c1 = (mk_fp ctx let c1 = (mk_fp ctx (mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1))
(mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1)) (mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11))
(mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52)) (mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52))) in
(mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11))) in
let c2 = (mk_to_fp_bv ctx let c2 = (mk_to_fp_bv ctx
(mk_numeral_string ctx "4619567317775286272" (BitVector.mk_sort ctx 64)) (mk_numeral_string ctx "4619567317775286272" (BitVector.mk_sort ctx 64))
(mk_sort ctx 11 53)) in (mk_sort ctx 11 53)) in
let c3 = (mk_to_fp_int_real ctx let c3 = (mk_to_fp_int_real ctx
(RoundingMode.mk_rtz ctx) (RoundingMode.mk_rtz ctx)
(mk_numeral_string ctx "2" (Integer.mk_sort ctx)) (mk_numeral_string ctx "2" (Integer.mk_sort ctx))
(mk_numeral_string ctx "1.75" (Real.mk_sort ctx)) (mk_numeral_string ctx "1.75" (Real.mk_sort ctx))
(FloatingPoint.mk_sort ctx 11 53)) in (FloatingPoint.mk_sort ctx 11 53)) in
let c4 = (mk_to_fp_real ctx (RoundingMode.mk_rtz ctx) let c4 = (mk_to_fp_real ctx (RoundingMode.mk_rtz ctx)