mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into ml-ng

Browse source 
Conflicts:
	scripts/mk_util.py

+ Cosmetics

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-24 18:44:59 +00:00
parent 5c7d0380d3
commit e29abefb12
1 changed files with 5 additions and 7 deletions

12
examples/ml/ml_example.ml
View file

@ -282,13 +282,11 @@ let fpa_example ( ctx : context ) =
Printf.printf "Test passed.\n"
);
(* Show that the following are equal: *)
(* (fp #b0 #b10000000001 #xc000000000000) *)
(* ((_ to_fp 11 53) #x401c000000000000)) *)
(* ((_ to_fp 11 53) RTZ 1.75 2))) *)
(* ((_ to_fp 11 53) RTZ 7.0))) *)
let solver = (mk_solver ctx None) in
(* Show that the following are equal: *)
(* (fp #b0 #b10000000001 #xc000000000000) *)
(* ((_ 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))