Bugfix - syntactic error in the description of the transformation.

src/printer/smtv2.ml

@@ -309,7 +309,7 @@ let print_prop_decl args info fmt k pr f = match k with
             (Pp.print_list Pp.space (print_fmla info)) model_list;*)
 	  fprintf fmt "@[(get-value (";
 	  List.iter (fun f -> 
-	  fprintf str_formatter "%a" (print_fmla info) f;
+	    fprintf str_formatter "%a" (print_fmla info) f;
           let s = flush_str_formatter () in
           fprintf fmt "@\n;; %s@\n%s" s s;
           ) model_list;

src/transform/intro_projections_counterexmp.ml

@@ -9,10 +9,6 @@
 (*                                                                  *)
 (********************************************************************)
 
-(*
-  
-*)
-
 open Ident
 open Term
 open Decl
@@ -128,12 +124,14 @@ let meta_transform2 projs =
   let map_projs = build_projections_map projs in
   Trans.decl (introduce_projs map_projs) None
 
-let intro_projections_counterexmp = Trans.on_tagged_ls meta_projection meta_transform2
+let intro_projections_counterexmp = 
+  Trans.on_tagged_ls meta_projection meta_transform2
+
 
 let () = Trans.register_transform "intro_projections_counterexmp" intro_projections_counterexmp
-  ~desc:"Introduce@ new@ constant@ symbol@ for@ every@ term@ with@ model@ \
-         label@ that@ has@ the@ same@ type@ as@ an@ argument@ of@ some@ function@ \
-         labeled@ with@ meta@ model_projectionin@ the@ goal."
+  ~desc:"For@ each@ declared@ abstract@ function@ and@ predicate@ p@ labeled@ with@ label@ \
+model_projected@ for@ that@ it@ exists@ a@ projection@ function@ f@ creates@ declaration@ of@ \
+new@ constant@ c@ and@ axiom@ stating@ that c = f p"
 
 (*
 Local Variables:

src/transform/intro_projections_counterexmp.mli

@@ -10,7 +10,27 @@
 (********************************************************************)
 
 val intro_projections_counterexmp :  Task.task Trans.trans
- (** [intros G f] returns the declarations after introducing
-     new constant symbol for every term with model label that has the
-     same type as an argument of some function labeled with meta
-     model_projection in the goal [goal G : f] *)
+ (**
+    Transformation that for each declared abstract function and predicate 
+    p labeled with label "model_projected" for that it exists a projection
+    function f creates declaration of new constant c and axiom stating that
+    c = f p
+
+    Projection functions are functions tagged with meta "model_projection".
+    Function f is projection function for abstract function and predicate p
+    if f is tagged with meta "model_projection" and has a single argument
+    of the same type as is the type of p.
+
+    This transformation is needed in situations when we want to display not
+    value of a variable, but value of a projection function applied to a variable.
+    
+    Note that since Why3 supports namespaces (different projection functions
+    can have the same name) and input languages of solvers typically not,
+    Why3 renames projection functions to avoid name clashes.
+    This is why it is not possible to just store the name of the projection
+    function in a label and than query the solver directly for the value of
+    the projection.
+    Also, it means that this transformation should thus be executed before 
+    this renaming.
+ *)
+