diff --git a/src/core/model_parser.ml b/src/core/model_parser.ml
index 478fa582399e8ea80ac46f14b43d22d22cec7b4b..e935b8d1f2edd46eb94fc693b45c238e673066b3 100644
--- a/src/core/model_parser.ml
+++ b/src/core/model_parser.ml
@@ -311,6 +311,48 @@ let build_model raw_model printer_mapping =
   build_model_rec raw_model printer_mapping.queried_terms empty_model
 
 
+(*
+***************************************************************
+**  Filtering the model
+***************************************************************
+*)
+
+let add_loc orig_model new_model position =
+  (* Add a given location from orig_model to new_model *)
+
+  let (file_name, line_num, _, _) = (Loc.get position) in
+  let orig_model_file = get_model_file orig_model file_name in
+  let new_model_file = get_model_file new_model file_name in
+
+  if IntMap.mem line_num new_model_file then
+    (* the location already is in new_model *)
+    new_model
+  else
+    try
+      (* get the location from original model *)
+      let line_map = IntMap.find line_num orig_model_file in
+      (* add the location to new model *)
+      let new_model_file = IntMap.add line_num line_map new_model_file in
+      StringMap.add file_name new_model_file new_model
+    with Not_found ->
+      new_model
+
+let add_first_model_line filename model_file model =
+  let (line_num, cnt_info) = IntMap.min_binding model_file in
+  let mf = get_model_file model filename in
+  let mf = IntMap.add line_num cnt_info mf in
+  StringMap.add filename mf model
+
+let model_for_positions_and_decls model ~positions =
+  (* Start with empty model and add locations from model that
+     are in locations *)
+  let model_filtered = List.fold_left (add_loc model) empty_model positions in
+  (* For each file add mapping corresponding to the first line of the
+     counter-example from model to model_filtered.
+     This corresponds to function declarations *)
+  StringMap.fold add_first_model_line model model_filtered
+
+
 (*
 ***************************************************************
 ** Registering model parser
diff --git a/src/core/model_parser.mli b/src/core/model_parser.mli
index dc2cadf5e11d3dfd1adade9fb2da23f788060c25..d63abd2c20cdadc3e096a5dd91c1031a57b8d521 100644
--- a/src/core/model_parser.mli
+++ b/src/core/model_parser.mli
@@ -10,7 +10,7 @@
 (********************************************************************)
 
 (*
-*************************************************************** 
+***************************************************************
 **  Counter-example model values
 ****************************************************************
 *)
@@ -27,19 +27,19 @@ and model_array = {
   arr_indices : arr_index list;
 }
 
-val array_create_constant : 
-  value : model_value -> 
+val array_create_constant :
+  value : model_value ->
   model_array
 (** Creates constant array with all indices equal to the parameter value. *)
 
-val array_add_element : 
-  array : model_array -> 
-  index : model_value -> 
-  value : model_value -> 
+val array_add_element :
+  array : model_array ->
+  index : model_value ->
+  value : model_value ->
   model_array
-(** Adds an element to the array. 
+(** Adds an element to the array.
     @param array : the array to that the element will be added
-    
+
     @param index : the index on which the element will be added.
     Note that the index must be of value model_value.Integer
 
@@ -50,13 +50,13 @@ val print_model_value : Format.formatter -> model_value -> unit
 
 
 (*
-*************************************************************** 
+***************************************************************
 **  Model elements
 ***************************************************************
 *)
 (** Counter-example model elements. Each element represents
     a counter-example for a single source-code element.*)
-type model_element = { 
+type model_element = {
   me_name     : string;
     (** The name of the source-code element.  *)
   me_value    : model_value;
@@ -67,33 +67,33 @@ type model_element = {
     (** Why term corresponding to the element.  *)
 }
 
-val create_model_element : 
-  name     : string -> 
-  value    : model_value -> 
-  ?location : Loc.position -> 
+val create_model_element :
+  name     : string ->
+  value    : model_value ->
+  ?location : Loc.position ->
   ?term     : Term.term ->
   unit ->
   model_element
-(** Creates a counter-example model element. 
+(** Creates a counter-example model element.
     @param name : the name of the source-code element
 
     @param value  : counter-example value for the element
 
-    @param location : source-code location of the element 
-    
+    @param location : source-code location of the element
+
     @param term : why term corresponding to the element *)
 
 (*
-*************************************************************** 
+***************************************************************
 **  Model definitions
 ***************************************************************
-*)   
-type model 
+*)
+type model
 
 val empty_model : model
 
 (*
-*************************************************************** 
+***************************************************************
 **  Quering the model
 ***************************************************************
 *)
@@ -106,22 +106,41 @@ val print_model_json : Format.formatter -> model -> unit
 
 val model_to_string_json : model -> string
 
-val interleave_with_source : 
+val interleave_with_source :
   ?start_comment:string ->
   ?end_comment:string ->
-  model -> 
-  string -> 
-  string -> 
+  model ->
+  string ->
+  string ->
   string
 
 (*
-*************************************************************** 
+***************************************************************
+**  Filtering the model
+***************************************************************
+*)
+val model_for_positions_and_decls : model ->
+  positions: Loc.position list -> model
+(** Given a model and a list of source-code positions returns model
+    that contains only elements from the input model that are on these
+    positions plus for every file in the model, elements that are
+    in the positions of function declarations. Elements with other
+    positions are filtered out.
+
+    Assumes that for each file the element on the first line of the model
+    has position of function declaration.
+
+    Only filename and line number is used to identify positions.
+*)
+
+(*
+***************************************************************
 ** Registering model parser
 ***************************************************************
 *)
 type model_parser =  string -> Printer.printer_mapping -> model
-(** Parses the input string into model elements, estabilishes 
-    a mapping between these elements and mapping from printer 
+(** Parses the input string into model elements, estabilishes
+    a mapping between these elements and mapping from printer
     and builds model data structure.
 *)