1 files changed, 12 insertions, 5 deletions
diff --git a/src/specialize.ml b/src/specialize.ml
index 607084c8..a601974e 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -73,13 +73,13 @@ let typ_ord_specialization = {
 
 let int_specialization = {
     is_polymorphic = is_int_kopt;
-    instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false);
+    instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp (Nexp_aux (Nexp_constant _, _)), _) -> true | _ -> false);
     extern_filter = (fun externs -> match Ast_util.extern_assoc "c" externs with Some _ -> true | None -> false)
   }
 
 let int_specialization_with_externs = {
     is_polymorphic = is_int_kopt;
-    instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp _, _) -> true | _ -> false);
+    instantiation_filter = (fun _ arg -> match arg with A_aux (A_nexp (Nexp_aux (Nexp_constant _, _)), _) -> true | _ -> false);
     extern_filter = (fun _ -> false)
   }
 
@@ -391,7 +391,7 @@ let specialize_id_valspec spec instantiations id ast =
        let kopts, constraints = quant_split typq in
        let constraints = instantiate_constraints safe_instantiation constraints in
        let constraints = instantiate_constraints reverse constraints in
-       let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt)) kopts in
+       let kopts = List.filter (fun kopt -> not (spec.is_polymorphic kopt && KBindings.mem (kopt_kid kopt) safe_instantiation)) kopts in
        let typq =
          if List.length (typ_frees @ int_frees) = 0 && List.length kopts = 0 then
            mk_typquant []
@@ -490,6 +490,7 @@ let initial_calls = ref (IdSet.of_list
     mk_id "execute";
     mk_id "decode";
     mk_id "initialize_registers";
+    mk_id "prop";
     mk_id "append_64" (* used to construct bitvector literals in C backend *)
   ])
 
@@ -554,6 +555,7 @@ let reorder_typedefs (Defs defs) =
   Defs (List.rev !tdefs @ others)
 
 let specialize_ids spec ids ast =
+  let t = Profile.start () in
   let total = IdSet.cardinal ids in
   let _, ast =
     List.fold_left
@@ -572,11 +574,16 @@ let specialize_ids spec ids ast =
   | None -> ()
   end;
   let ast, _ = Type_error.check Type_check.initial_env ast in
-  let ast =
-    List.fold_left (fun ast id -> rewrite_polymorphic_calls spec id ast) ast (IdSet.elements ids)
+  let _, ast =
+    List.fold_left
+      (fun (n, ast) id ->
+        Util.progress "Rewriting " (string_of_id id) n total;
+        (n + 1, rewrite_polymorphic_calls spec id ast))
+      (1, ast) (IdSet.elements ids)
   in
   let ast, env = Type_error.check Type_check.initial_env ast in
   let ast = remove_unused_valspecs env ast in
+  Profile.finish "specialization pass" t;
   ast, env
 
 let rec specialize' n spec ast env =