Zustre backend

configure.ac

@@ -79,7 +79,7 @@ AS_IF([test "x$seal" = "xyes"], [
 
 # z3
 AC_MSG_CHECKING(z3 library (optional))
-define([z3path], esyscmd([ocamlfind query z3]))
+define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
 
 AS_IF([ocamlfind query z3 >/dev/null 2>&1],
     [z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],

src/backends/C/c_backend.ml

@@ -48,7 +48,7 @@ let gen_files funs basename prog machines dependencies =
   (match !Options.main_node with
   | "" ->  () (* No main node: we do not generate main *)
   | main_node -> (
-    match Machine_code_common.get_machine_opt main_node machines with
+    match Machine_code_common.get_machine_opt machines main_node with
     | None -> begin
       Global.main_node := main_node;
       Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
@@ -70,7 +70,7 @@ let gen_files funs basename prog machines dependencies =
   | "" ->  ()
   | mauve -> (
     (* looking for the main node *)
-    match Machine_code_common.get_machine_opt mauve machines with
+    match Machine_code_common.get_machine_opt machines mauve  with
     | None -> begin
       Global.main_node := mauve;
       Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;

src/backends/Horn/horn_backend_collecting_sem.ml

@@ -49,7 +49,7 @@ let collecting_semantics machines fmt node machine =
   (* Init case *)
   let _ = 
     (* Special case when the main node is stateless *)
-    if is_stateless machine then (
+    if Machine_code_common.is_stateless machine then (
       let step_name = pp_machine_stateless_name in
       fprintf fmt "; Initial set: One Step(m,x)  -- Stateless node! @.";
       fprintf fmt "(declare-rel INIT_STATE ())@.";
@@ -86,7 +86,7 @@ let collecting_semantics machines fmt node machine =
   in
 
   let step_name = 
-    if is_stateless machine then 
+    if Machine_code_common.is_stateless machine then 
       pp_machine_stateless_name
     else
       pp_machine_step_name
@@ -142,7 +142,7 @@ let cex_computation machines fmt node machine =
 
     (* Special case when the cex node is stateless *)
   let reset_name, step_name =
-    if is_stateless machine then
+    if Machine_code_common.is_stateless machine then
       pp_machine_stateless_name, pp_machine_stateless_name
     else
       pp_machine_reset_name, pp_machine_step_name

src/backends/Horn/horn_backend_common.ml

@@ -14,6 +14,8 @@ open Lustre_types
 open Machine_code_types
 open Corelang
 
+let get_machine = Machine_code_common.get_machine
+
 let machine_reset_name id = id ^ "_reset"
 let machine_step_name id = id ^ "_step" 
 let machine_stateless_name id = id ^ "_fun" 
@@ -78,13 +80,6 @@ let rename_mid_list = List.map rename_mid
 let rename_next = rename (fun n -> n ^ "_x")
 let rename_next_list = List.map rename_next
 
-let get_machine machines node_name =
-(*  try *)
-  List.find (fun m  -> m.mname.node_id = node_name) machines
-(* with Not_found -> Format.eprintf "Unable to find machine %s in machines %a@.@?"  *)
-(*   node_name *)
-(*   (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines *)
-(*   ; assert false *)
 
 let local_memory_vars machines machine =
   rename_machine_list machine.mname.node_id machine.mmemory
@@ -153,6 +148,7 @@ let reset_vars machines m =
   @ (rename_mid_list (full_memory_vars machines m))
 
 
+
 (* Local Variables: *)
 (* compile-command:"make -C ../.." *)
 (* End: *)

src/backends/Horn/horn_backend_printers.ml

@@ -419,7 +419,6 @@ let pp_machine_reset machines fmt m =
 
 (**************************************************************)
 
-let is_stateless m = m.minstances = [] && m.mmemory = []
 
 (* Print the machine m:
    two functions: m_init and m_step

src/machine_code_common.ml

@@ -116,6 +116,8 @@ let rec is_const_value v =
 let get_stateless_status m =
  (m.mname.node_dec_stateless, try Utils.desome m.mname.node_stateless with _ -> failwith ("stateless status of machine " ^ m.mname.node_id ^ " not computed"))
 
+let is_stateless m = m.minstances = [] && m.mmemory = []
+
 let is_input m id =
   List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs
 
@@ -223,7 +225,7 @@ let new_instance =
     end
 
 
-let get_machine_opt name machines =
+let get_machine_opt machines name =
   List.fold_left
     (fun res m ->
       match res with
@@ -231,6 +233,15 @@ let get_machine_opt name machines =
       | None -> if m.mname.node_id = name then Some m else None)
     None machines
 
+let get_machine machines node_name =
+ try
+  List.find (fun m  -> m.mname.node_id = node_name) machines
+ with Not_found -> Format.eprintf "Unable to find machine %s in machines %a@.@?"
+   node_name
+   (Utils.fprintf_list ~sep:", " (fun fmt m -> Format.pp_print_string fmt m.mname.node_id)) machines
+   ; assert false
+     
+    
 let get_const_assign m id =
   try
     match get_instr_desc (List.find

src/machine_code_common.mli

@@ -4,6 +4,7 @@ val is_output: Machine_code_types.machine_t -> Lustre_types.var_decl -> bool
 val is_const_value: Machine_code_types.value_t -> bool
 val get_const_assign: Machine_code_types.machine_t -> Lustre_types.var_decl -> Machine_code_types.value_t
 val get_stateless_status: Machine_code_types.machine_t -> bool * bool
+val is_stateless: Machine_code_types.machine_t -> bool
 val mk_val: Machine_code_types.value_t_desc -> Types.type_expr -> Machine_code_types.value_t
 val mk_conditional: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> Machine_code_types.instr_t list -> Machine_code_types.instr_t list -> Machine_code_types.instr_t
 val empty_machine: Machine_code_types.machine_t
@@ -14,6 +15,11 @@ val dimension_of_value:Machine_code_types.value_t -> Dimension.dim_expr
 val pp_instr: Format.formatter -> Machine_code_types.instr_t -> unit
 val pp_instrs: Format.formatter -> Machine_code_types.instr_t list -> unit
 val pp_machines: Format.formatter -> Machine_code_types.machine_t list -> unit
-val get_machine_opt: string -> Machine_code_types.machine_t list -> Machine_code_types.machine_t option
+val get_machine_opt: Machine_code_types.machine_t list -> string -> Machine_code_types.machine_t option
+
+(* Same function but fails if no such a machine  exists *)
+val get_machine: Machine_code_types.machine_t list -> string -> Machine_code_types.machine_t
+
+  
 val get_node_def: string -> Machine_code_types.machine_t -> Lustre_types.node_desc
 val join_guards_list: Machine_code_types.instr_t list -> Machine_code_types.instr_t list

src/tools/zustre_verifier.ml

-open LustreSpec
-open Machine_code
+open Lustre_types
+open Machine_code_types
+open Machine_code_common
 open Format
 (* open Horn_backend_common
  * open Horn_backend *)
@@ -16,12 +17,22 @@ let rename_current_list = HBC.rename_current_list
 let rename_mid_list = HBC.rename_mid_list
 let rename_next_list = HBC.rename_next_list
 let full_memory_vars = HBC.full_memory_vars
-   
-let active = ref false
-let ctx = ref (Z3.mk_context [])
+let inout_vars = HBC.inout_vars
+let reset_vars = HBC.reset_vars
+let step_vars = HBC.step_vars
+let local_memory_vars = HBC.local_memory_vars
+  
 let machine_reset_name = HBC.machine_reset_name 
 let machine_stateless_name = HBC.machine_stateless_name 
 
+let rename_mid = HBC.rename_mid
+
+let preprocess = Horn_backend.preprocess
+  
+let active = ref false
+let ctx = ref (Z3.mk_context [])
+let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx)
+
 (** Sorts
 
 A sort is introduced for each basic type and each enumerated type.
@@ -105,7 +116,7 @@ let decl_rel name args =
   
 
 
-(** conversion functions
+(** Conversion functions
 
 The following is similar to the Horn backend. Each printing function
    is rephrased from pp_xx to xx_to_expr and produces a Z3 value.
@@ -168,7 +179,8 @@ let rec horn_default_val t =
    * | Types.Ttuple(l) -> assert false
    * |_ -> *) assert false
 
-
+(* Conversion of basic library functions *)
+    
 let horn_basic_app i val_to_expr vl =
   match i, vl with
   | "ite", [v1; v2; v3] ->
@@ -445,10 +457,39 @@ let instance_call_to_exprs machines reset_instances m i inputs outputs =
     in
     [expr]
   )
+
+
+    
+(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
+(* let rec value_suffix_to_expr self value = *)
+(*  match value.value_desc with *)
+(*  | Fun (n, vl)  ->  *)
+(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
     
+(*  |  _            -> *)
+(*    horn_val_to_expr self value *)
+
 
+(* type_directed assignment: array vs. statically sized type
+   - [var_type]: type of variable to be assigned
+   - [var_name]: name of variable to be assigned
+   - [value]: assigned value
+   - [pp_var]: printer for variables
+*)
+let assign_to_exprs m var_name value =
+  let self = m.mname.node_id in
+  let e =
+    Z3.Boolean.mk_eq
+      !ctx
+      (horn_val_to_expr ~is_lhs:true self var_name)
+      (horn_val_to_expr self value)
+  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
+  in
+  [e]
+
+    
 (* Convert instruction to Z3.Expr and update the set of reset instances *)
-let rec instr_to_expr machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
+let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
   match Corelang.get_instr_desc instr with
   | MComment _ -> [], reset_instances
   | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
@@ -459,12 +500,12 @@ let rec instr_to_expr machines reset_instances (m: machine_t) instr : Z3.Expr.ex
     i::reset_instances
   | MLocalAssign (i,v) ->
     assign_to_exprs
-      m (horn_var_to_expr) 
+      m  
       (mk_val (LocalVar i) i.var_type) v,
     reset_instances
   | MStateAssign (i,v) ->
     assign_to_exprs
-      m (horn_var_to_expr) 
+      m 
       (mk_val (StateVar i) i.var_type) v,
     reset_instances
   | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
@@ -487,82 +528,99 @@ let rec instr_to_expr machines reset_instances (m: machine_t) instr : Z3.Expr.ex
        statement. *)
     let self = m.mname.node_id in
     let branch_to_expr (tag, instrs) =
-      Z3.Boolean.mk_implies
-        (Z3.Boolean.mk_eq !ctx 
-           (horn_val_to_expr self g)
-	   (horn_tag_to_expr tag))
-        (machine_instrs_to_exprs machines reset_instances m instrs)
+      let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in
+      let e =
+	Z3.Boolean.mk_implies !ctx
+          (Z3.Boolean.mk_eq !ctx 
+             (horn_val_to_expr self g)
+	     (horn_tag_to_expr tag))
+          branch_def in
+
+      [e], branch_resets
+	  
     in
-    List.map branch_to_expr hl,
-    reset_instances 
+    List.fold_left (fun (instrs, resets) b ->
+      let b_instrs, b_resets = branch_to_expr b in
+      instrs@b_instrs, resets@b_resets 
+    ) ([], reset_instances) hl 
 
 and instrs_to_expr machines reset_instances m instrs = 
-  let instr_to_expr rs i = instr_to_expr machines rs m i in
-  match instrs with
-  | [x] -> instr_to_expres reset_instances x 
-  | _::_ -> (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *)
-
-      List.fold_left (fun (exprs, rs) i -> 
-          let exprs_i, rs = ppi rs i in
-          expr@exprs_i, rs
-        )
-        ([], reset_instances) instrs 
-    
-    
-  | [] -> [], reset_instances
-
-
-let basic_library_to_horn_expr i vl =
-  match i, vl with
-  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
-
-  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
-  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
-  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
-  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
-  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
-  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
-  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
-  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
-  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
-  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
-  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
-  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
-  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
-(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
-
-*)
+  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
+  let e_list, rs = 
+    match instrs with
+    | [x] -> instr_to_exprs reset_instances x 
+    | _::_ -> (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *)
+       
+       List.fold_left (fun (exprs, rs) i -> 
+         let exprs_i, rs_i = instr_to_exprs rs i in
+         exprs@exprs_i, rs@rs_i
+       )
+         ([], reset_instances) instrs 
+	 
+	 
+    | [] -> [], reset_instances
+  in
+  let e = 
+    match e_list with
+    | [e] -> e
+    | [] -> Z3.Boolean.mk_true !ctx
+    | _ -> Z3.Boolean.mk_and !ctx e_list
+  in
+  e, rs
 
         
-(* Prints a [value] indexed by the suffix list [loop_vars] *)
-let rec value_suffix_to_expr self value =
- match value.value_desc with
- | Fun (n, vl)  -> 
-   basic_library_to_horn_expr n (value_suffix_to_expr self vl)
- |  _            ->
-   horn_val_to_expr self value
+let machine_reset machines m =
+  let locals = local_memory_vars machines m in
+  
+  (* print "x_m = x_c" for each local memory *)
+  let mid_mem_def =
+    List.map (fun v ->
+      Z3.Boolean.mk_eq !ctx
+	(horn_var_to_expr (rename_mid v))
+	(horn_var_to_expr (rename_current v))
+    ) locals
+  in
 
-        
-(* type_directed assignment: array vs. statically sized type
-   - [var_type]: type of variable to be assigned
-   - [var_name]: name of variable to be assigned
-   - [value]: assigned value
-   - [pp_var]: printer for variables
-*)
-let assign_to_exprs m var_name value =
-  let self = m.mname.node_id in
-  let e =
-    Z3.Boolean.mk_eq
-      !ctx
-      (horn_val_to_expr ~is_lhs:true self var_name)
-      (value_suffix_to_expr self value)
+  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
+     Special treatment for _arrow: _first = true
+  *)
+
+  let reset_instances =
+    
+    List.map (fun (id, (n, _)) ->
+      let name = node_name n in
+      if name = "_arrow" then (
+	Z3.Boolean.mk_eq !ctx
+	  (
+	    let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
+	    Z3.Expr.mk_const_f !ctx vdecl
+	  )
+	  (Z3.Boolean.mk_true !ctx)
+	  
+      ) else (
+	let machine_n = get_machine machines name in 
+	
+	Z3.Expr.mk_app
+	  !ctx
+	  (get_fdecl (name ^ "_reset"))
+	  (List.map (horn_var_to_expr)
+	     (rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
+	  )
+	  
+      )
+    ) m.minstances
+      
+      
   in
-  [e]
+  
+  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
+    
+        
 
-(*                TODO: empty list means true statement *)
+(*  TODO: empty list means true statement *)
 let decl_machine machines m =
-  if m.Machine_code.mname.node_id = Machine_code.arrow_id then
-    (* We don't print arrow function *)
+  if m.mname.node_id = Arrow.arrow_id then
+    (* We don't do arrow function *)
     ()
   else
     begin
@@ -571,42 +629,47 @@ let decl_machine machines m =
       	  (
 	    (inout_vars machines m)@
 	      (rename_current_list (full_memory_vars machines m)) @
-	        (rename_mid_list (full_memory_vars machines m)) @
-	          (rename_next_list (full_memory_vars machines m)) @
-	            (rename_machine_list m.mname.node_id m.mstep.step_locals)
+	      (rename_mid_list (full_memory_vars machines m)) @
+	      (rename_next_list (full_memory_vars machines m)) @
+	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
 	  )
       in
       
       if is_stateless m then
 	begin
 	  (* Declaring single predicate *)
-	  let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in          
-          match m.mstep.step_asserts with
+	  let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in
+	  let horn_body, _ (* don't care for reset here *) =
+	    instrs_to_expr
+	      machines
+	      ([] (* No reset info for stateless nodes *) )
+	      m
+	      m.mstep.step_instrs
+	  in
+	  let horn_head = 
+	    Z3.Expr.mk_app
+	      !ctx
+	      (get_fdecl (machine_stateless_name m.mname.node_id))
+	      (List.map (horn_var_to_expr) (inout_vars machines m))
+	  in
+	  match m.mstep.step_asserts with
 	  | [] ->
 	     begin
-
-	       (* Rule for single predicate *)
-	       fprintf fmt "; Stateless step rule @.";
-	       fprintf fmt "@[<v 2>(rule (=> @ ";
-	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
-	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
-		 pp_machine_stateless_name m.mname.node_id
-		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (inout_vars machines m);
+	       (* Rule for single predicate : "; Stateless step rule @." *)
+	       Z3.Fixedpoint.add_rule !fp
+		 (Z3.Boolean.mk_implies !ctx horn_body horn_head)
+		 None
 	     end
 	  | assertsl ->
 	     begin
-	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
-	       
-	       fprintf fmt "; Stateless step rule with Assertions @.";
-	       (*Rule for step*)
-	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
-	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
-	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
-		 pp_machine_stateless_name m.mname.node_id
-		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
-	  
+	       (*Rule for step "; Stateless step rule with Assertions @.";*)
+	       let body_with_asserts =
+		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
+	       in
+	       Z3.Fixedpoint.add_rule !fp
+		 (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
+		 None
 	     end
-	       
 	end
       else
 	begin
@@ -615,36 +678,54 @@ let decl_machine machines m =
           let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in
 
 	  (* Rule for reset *)
-	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
-	    (pp_machine_reset machines) m 
-	    pp_machine_reset_name m.mname.node_id
-	    (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (reset_vars machines m);
 
-          match m.mstep.step_asserts with
+	  let horn_reset_body = machine_reset machines m in	    
+	  let horn_reset_head = 
+	    Z3.Expr.mk_app
+	      !ctx
+	      (get_fdecl (machine_reset_name m.mname.node_id))
+	      (List.map (horn_var_to_expr) (reset_vars machines m))
+	  in
+	  
+	  let _ =
+	    Z3.Fixedpoint.add_rule !fp
+	      (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
+	      None
+	  in
+
+	  (* Rule for step*)
+	  let horn_step_body, _ (* don't care for reset here *) =
+	    instrs_to_expr
+	      machines
+	      []
+	      m
+	      m.mstep.step_instrs
+	  in
+	  let horn_step_head = 
+	    Z3.Expr.mk_app
+	      !ctx
+	      (get_fdecl (machine_step_name m.mname.node_id))
+	      (List.map (horn_var_to_expr) (step_vars machines m))
+	  in
+	  match m.mstep.step_asserts with
 	  | [] ->
 	     begin
-	       fprintf fmt "; Step rule @.";
-	       (* Rule for step*)
-	       fprintf fmt "@[<v 2>(rule (=> @ ";
-	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
-	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
-		 pp_machine_step_name m.mname.node_id
-		 (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (step_vars machines m);
+	       (* Rule for single predicate *)
+	       Z3.Fixedpoint.add_rule !fp
+		 (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
+		 None
 	     end
-	  | assertsl -> 
+	  | assertsl ->
 	     begin
-	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
-	       (* print_string pp_val; *)
-	       fprintf fmt "; Step rule with Assertions @.";
-	       
-	       (*Rule for step*)
-	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
-	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
-	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
-		 pp_machine_step_name m.mname.node_id
-		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
+	       (* Rule for step Assertions @.; *)
+	       let body_with_asserts =
+		 Z3.Boolean.mk_and !ctx
+		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
+	       in
+	       Z3.Fixedpoint.add_rule !fp
+		 (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
+		 None
 	     end
-	       
      	       
 	end
     end
@@ -679,7 +760,7 @@ module Verifier =
       Backends.get_normalization_params ()
 
     let setup_solver () =
-      let fp = Z3.Fixedpoint.mk_fixedpoint !ctx in
+      fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
       (* let help = Z3.Fixedpoint.get_help fp in
        * Format.eprintf "Fp help : %s@." help;
        * 
@@ -744,18 +825,18 @@ module Verifier =
         P.add_bool params (mks "xform.inline_linear") false;
         P.add_bool params (mks "xform.inline_eager") false
       );
-      Z3.Fixedpoint.set_parameters fp params
-        
+      Z3.Fixedpoint.set_parameters !fp params
+              
       
     let run basename prog machines =
-      let machines = Machine_code.arrow_machine::machines in
+      let machines = Machine_code_common.arrow_machine::machines in
       let machines = preprocess machines in
       setup_solver ();
       decl_sorts ();
       List.iter (decl_machine machines) (List.rev machines);
-
-      
       ()
+      
+      
 
   end: VerifierType.S)