Bugfixing

2 files changed, 19 insertions, 7 deletions

diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index daf1b0ff..93abf498 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -81,16 +81,20 @@ let optimize_unit instrs =
   filter_instrs non_pointless_copy (map_instr_list unit_instr instrs)
 
 let flat_counter = ref 0
-let flat_id () =
-  let id = mk_id ("local#" ^ string_of_int !flat_counter) in
+let flat_id orig_id =
+  let id = mk_id (string_of_name orig_id ^ "_local#" ^ string_of_int !flat_counter) in
   incr flat_counter;
   name id
 
 let rec flatten_instrs = function
   | I_aux (I_decl (ctyp, decl_id), aux) :: instrs ->
-     let fid = flat_id () in
+     let fid = flat_id decl_id in
      I_aux (I_decl (ctyp, fid), aux) :: flatten_instrs (instrs_rename decl_id fid instrs)
 
+  | I_aux (I_init (ctyp, decl_id, cval), aux) :: instrs ->
+     let fid = flat_id decl_id in
+     I_aux (I_init (ctyp, fid, cval), aux) :: flatten_instrs (instrs_rename decl_id fid instrs)
+
   | I_aux ((I_block block | I_try_block block), _) :: instrs ->
      flatten_instrs block @ flatten_instrs instrs
 
@@ -169,9 +173,11 @@ let rec cval_subst id subst = function
 let rec instrs_subst id subst =
   function
   | (I_aux (I_decl (_, id'), _) :: _) as instrs when Name.compare id id' = 0 ->
+     prerr_endline ("DECL: " ^ string_of_name id);
      instrs
 
   | I_aux (I_init (ctyp, id', cval), aux) :: rest when Name.compare id id' = 0 ->
+     prerr_endline ("INIT: " ^ string_of_name id);
      I_aux (I_init (ctyp, id', cval_subst id subst cval), aux) :: rest
 
   | (I_aux (I_reset (_, id'), _) :: _) as instrs when Name.compare id id' = 0 ->
@@ -201,7 +207,7 @@ let rec instrs_subst id subst =
        | I_throw cval -> I_throw (cval_subst id subst cval)
        | I_comment str -> I_comment str
        | I_raw str -> I_raw str
-       | I_return cval -> I_return cval
+       | I_return cval -> I_return (cval_subst id subst cval)
        | I_reset (ctyp, id') -> I_reset (ctyp, id')
        | I_reinit (ctyp, id', cval) -> I_reinit (ctyp, id', cval_subst id subst cval)
      in
@@ -209,6 +215,10 @@ let rec instrs_subst id subst =
 
   | [] -> []
 
+let instrs_subst' id subst =
+  prerr_endline (string_of_name id ^ " => " ^ string_of_cval subst);
+  instrs_subst id subst
+
 let rec clexp_subst id subst = function
   | CL_id (id', ctyp) when Name.compare id id' = 0 ->
      if ctyp_equal ctyp (clexp_ctyp subst) then
@@ -263,7 +273,7 @@ let inline cdefs should_inline instrs =
           incr inlines;
           incr label_count;
           let inline_label = label "end_inline_" in
-          let body = List.fold_right2 instrs_subst (List.map name ids) args body in
+          let body = List.fold_right2 instrs_subst' (List.map name ids) args body in
           let body = List.map (map_instr fix_labels) body in
           let body = List.map (map_instr (replace_end inline_label)) body in
           let body = List.map (map_instr (replace_return clexp)) body in
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 78de9069..c094cdaa 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1320,7 +1320,8 @@ let smt_cdef props name_file env all_cdefs = function
           ) visit_order;
 
         let out_chan = open_out (name_file (string_of_id function_id)) in
-        output_string out_chan "(set-logic QF_AUFBVDT)\n";
+        output_string out_chan "(set-option :produce-models true)\n";
+        (*output_string out_chan "(set-logic QF_AUFBVDT)\n";*)
 
         (* let stack' = Stack.create () in
         Stack.iter (fun def -> Stack.push def stack') stack;
@@ -1328,7 +1329,8 @@ let smt_cdef props name_file env all_cdefs = function
         let queue = optimize_smt stack in
         Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") queue;
 
-        output_string out_chan "(check-sat)\n"
+        output_string out_chan "(check-sat)\n";
+        output_string out_chan "(get-model)\n"
 
      | _ -> failwith "Bad function body"
      end