From e29abefb12330ee4c6a053a95c28f7ab129ae5c0 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sat, 24 Jan 2015 18:44:59 +0000
Subject: [PATCH] Merge branch 'unstable' of https://git01.codeplex.com/z3 into
ml-ng
Conflicts:
scripts/mk_util.py
+ Cosmetics
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
examples/ml/ml_example.ml | 12 +++++-------
1 file changed, 5 insertions(+), 7 deletions(-)
diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml
index 127a973aa..df062bde4 100644
--- a/examples/ml/ml_example.ml
+++ b/examples/ml/ml_example.ml
@@ -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))