diff --git a/src/reduction_engine.ml b/src/reduction_engine.ml
index 5b89f9f3e6ca53eea91d6c09428372fa4b2a6bae..cba302c08b0f0147e61d47b1772113209aca8192 100644
--- a/src/reduction_engine.ml
+++ b/src/reduction_engine.ml
@@ -14,6 +14,8 @@ open Term
 
 [@@@ocaml.warning "-9"]
 
+let debug = Debug.register_info_flag ~desc:"" "Reduction_engine"
+
 (* {2 Values} *)
 
 type value =
@@ -1074,7 +1076,7 @@ and reduce_app_no_equ engine st ls ~orig ty rem_cont =
     let args = List.map term_of_value args in
     match Ident.Mid.find ls.ls_name engine.known_map with
     | exception Not_found ->
-      Format.eprintf "Reduction engine, ident not found: %s@."
+      Debug.dprintf debug "Reduction engine, ident not found: %s@."
         ls.ls_name.Ident.id_string;
       {
         value_stack = Term (t_attr_copy orig (t_app ls args ty)) :: rem_st;
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index b26ab6d5bbbbe90f36e7ee4bd3a20a14f669dfc1..4e0f43efbf3dd0831987484a9b1022aedd64aaad 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -82,11 +82,13 @@ theory NN
 end
 
 theory Interpret
+  use bool.Bool
 
+  type input
   type dataset
 
   function open_dataset string: dataset
-
   function size dataset: int
 
+  predicate forall_ (d: dataset) (f: input -> bool)
 end
diff --git a/tests/interpretation.t b/tests/interpretation.t
index 3556e8f3b06238de4d7abfdb27268821d64f6d6f..409cc9239d81d2d7186d498aa9a25905b886d18b 100644
--- a/tests/interpretation.t
+++ b/tests/interpretation.t
@@ -1,4 +1,4 @@
-Test verify
+Test interpret
   $ caisar interpret -L . --format whyml - 2>&1 <<EOF | ./filter_tmpdir.sh
   > theory T
   >  use caisar.Interpret
@@ -14,7 +14,11 @@ Test verify
   >       let dataset = open_dataset "datasets/a" in
   >       size dataset = 2
   > 
+  >  predicate robust (i: input)
   > 
+  >   goal G5:
+  >       let dataset = open_dataset "datasets/a" in
+  >       forall_ dataset (fun i -> robust i)
   > end
   > EOF
   G1 : true
@@ -27,3 +31,6 @@ Test verify
   G4 : true
   caisar_op1,
   (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })
+  G5 : forall_ caisar_op2 (fun (i:input) -> robust i)
+  caisar_op2,
+  (Interpretation.Dataset { Interpretation.dataset = "datasets/a" })