Project

General

Profile

Revision 51106b7e src/tools/zustre/zustre_cex.ml

View differences:

src/tools/zustre/zustre_cex.ml
57 57
      (* Recall that MAIN args are in@mems@out *)
58 58
      let args = Z3.Expr.get_args conj in
59 59
      if List.length args = 1 + nb_inputs + nb_mems + nb_outputs then
60
	let id = Z3.Arithmetic.Integer.get_int (List.hd args) in
60
        (* Should be done with get_int but that function vanished from the opam Z3 API *)
61
	let id = Big_int.int_of_big_int (Z3.Arithmetic.Integer.get_big_int (List.hd args)) in
61 62
	let input_values = Utils.List.extract args 1 (1 + nb_inputs) in
62 63
	let output_values = Utils.List.extract args (1+nb_inputs+nb_mems) (1 + nb_inputs + nb_mems + nb_outputs) in
63 64
	(id, (input_values, output_values))::main, funs

Also available in: Unified diff