From 7e3676e24ac31d1c9b3f71c8a38f041142ff1069 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" <cwinter@microsoft.com> Date: Fri, 8 Jan 2016 13:25:14 +0000 Subject: [PATCH] bugfix for ML example --- examples/ml/ml_example.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index df062bde4..5b1c05069 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -287,16 +287,15 @@ let fpa_example ( ctx : context ) = (* ((_ to_fp 11 53) #x401c000000000000)) *) (* ((_ to_fp 11 53) RTZ 1.75 2))) *) (* ((_ to_fp 11 53) RTZ 7.0))) *) - let c1 = (mk_fp ctx - (mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1)) - (mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52)) - (mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11))) in + let c1 = (mk_fp ctx (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))) in let c2 = (mk_to_fp_bv ctx (mk_numeral_string ctx "4619567317775286272" (BitVector.mk_sort ctx 64)) (mk_sort ctx 11 53)) in let c3 = (mk_to_fp_int_real 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)) (FloatingPoint.mk_sort ctx 11 53)) in let c4 = (mk_to_fp_real ctx (RoundingMode.mk_rtz ctx)