fix Z3Prover#1800 by converting large integers to strings

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

Diff for: examples/ml/ml_example.ml

@@ -65,8 +65,7 @@ let  model_converter_test ( ctx : context ) =
 	| None -> raise (TestFailedException "")
 	| Some (m) -> 
 	  Printf.printf "Solver says: %s\n" (string_of_status q) ;
-	  Printf.printf "Model: \n%s\n" (Model.to_string m) ;
-	  Printf.printf "Converted Model: \n%s\n" (Model.to_string (convert_model ar 0 m))
+	  Printf.printf "Model: \n%s\n" (Model.to_string m) 
   )
 
 (**
@@ -330,12 +329,14 @@ let _ =
 	let ss = (Symbol.mk_string ctx "mySymbol") in
 	let bs = (Boolean.mk_sort ctx) in
 	let ints = (Integer.mk_sort ctx) in
-	let rs = (Real.mk_sort ctx) in
+        let rs = (Real.mk_sort ctx) in
+	let v = (Arithmetic.Integer.mk_numeral_i ctx 8000000000) in
 	Printf.printf "int symbol: %s\n" (Symbol.to_string is);
 	Printf.printf "string symbol: %s\n" (Symbol.to_string ss);
 	Printf.printf "bool sort: %s\n" (Sort.to_string bs);
 	Printf.printf "int sort: %s\n" (Sort.to_string ints);
 	Printf.printf "real sort: %s\n" (Sort.to_string rs);
+	Printf.printf "integer: %s\n" (Expr.to_string v);
 	basic_tests ctx ;
 	quantifier_example1 ctx ;
 	fpa_example ctx ;

Diff for: src/api/ml/z3.ml

@@ -43,6 +43,14 @@ let mk_list f n =
   in
   mk_list' 0 []
 
+let check_int32 v = v = Int32.to_int (Int32.of_int v)
+
+let mk_int_expr ctx v ty = 
+   if not (check_int32 v) then
+      Z3native.mk_numeral ctx (string_of_int v) ty
+   else
+      Z3native.mk_int ctx v ty
+    
 let mk_context (settings:(string * string) list) =
   let cfg = Z3native.mk_config () in
   let f e = Z3native.set_param_value cfg (fst e) (snd e) in
@@ -531,7 +539,7 @@ end = struct
   let mk_fresh_const (ctx:context) (prefix:string) (range:Sort.sort) = Z3native.mk_fresh_const ctx prefix range
   let mk_app (ctx:context) (f:FuncDecl.func_decl) (args:expr list) = expr_of_func_app ctx f args
   let mk_numeral_string (ctx:context) (v:string) (ty:Sort.sort) = Z3native.mk_numeral ctx v ty
-  let mk_numeral_int (ctx:context) (v:int) (ty:Sort.sort) = Z3native.mk_int ctx v ty
+  let mk_numeral_int (ctx:context) (v:int) (ty:Sort.sort) = mk_int_expr ctx v ty
   let equal (a:expr) (b:expr) = AST.equal a b
   let compare (a:expr) (b:expr) = AST.compare a b
 end
@@ -1036,7 +1044,7 @@ struct
     let mk_mod = Z3native.mk_mod
     let mk_rem = Z3native.mk_rem
     let mk_numeral_s (ctx:context) (v:string) = Z3native.mk_numeral ctx v (mk_sort ctx)
-    let mk_numeral_i (ctx:context) (v:int) = Z3native.mk_int ctx v (mk_sort ctx)
+    let mk_numeral_i (ctx:context) (v:int) = mk_int_expr ctx v (mk_sort ctx)
     let mk_int2real = Z3native.mk_int2real
     let mk_int2bv = Z3native.mk_int2bv
   end
@@ -1061,11 +1069,13 @@ struct
     let mk_numeral_nd (ctx:context) (num:int) (den:int) =
       if den = 0 then
         raise (Error "Denominator is zero")
+      else if not (check_int32 num) || not (check_int32 den) then
+        raise (Error "numerals don't fit in 32 bits")
       else
         Z3native.mk_real ctx num den
 
     let mk_numeral_s (ctx:context) (v:string) = Z3native.mk_numeral ctx v (mk_sort ctx)
-    let mk_numeral_i (ctx:context) (v:int) = Z3native.mk_int ctx v (mk_sort ctx)
+    let mk_numeral_i (ctx:context) (v:int) = mk_int_expr ctx v (mk_sort ctx)
     let mk_is_integer = Z3native.mk_is_int
     let mk_real2int = Z3native.mk_real2int
 
@@ -1155,11 +1165,6 @@ struct
   let is_bv_xor3 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_XOR3)
   let get_size (x:Sort.sort) = Z3native.get_bv_sort_size (Sort.gc x) x
 
-  let get_int (x:expr) =
-    match Z3native.get_numeral_int (Expr.gc x) x with
-    | true, v -> v
-    | false, _ -> raise (Error "Conversion failed.")
-
   let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x
   let mk_const (ctx:context) (name:Symbol.symbol) (size:int) =
     Expr.mk_const ctx name (mk_sort ctx size)

Diff for: src/api/ml/z3.mli

@@ -1152,9 +1152,6 @@ sig
     (** Create a new integer sort. *)
     val mk_sort : context -> Sort.sort
 
-    (** Retrieve the int value. *)
-    val get_int : Expr.expr -> int
-
     (** Get a big_int from an integer numeral *)
     val get_big_int : Expr.expr -> Big_int.big_int
 
@@ -1543,9 +1540,6 @@ sig
   (** The size of a bit-vector sort. *)
   val get_size : Sort.sort -> int
 
-  (**  Retrieve the int value. *)
-  val get_int : Expr.expr -> int
-
   (** Returns a string representation of a numeral. *)
   val numeral_to_string : Expr.expr -> string