diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i b/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i
index 8198e9065e16169091f2f3c9374da8b9e88dbd96..7f71fcedc6f6b8a2c42ce17a0416b08fa9c38ebd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/empty.i
@@ -1,3 +1,3 @@
 /* run.config
-   COMMENT: testing the empty file
+   COMMENT: empty file
    OPT: -e-acsl-project p -then-on p -print */
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/false.i b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
new file mode 100644
index 0000000000000000000000000000000000000000..8a7597fd11a5cb6ac72cd080877651cb63d7b4b7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i
@@ -0,0 +1,6 @@
+/* run.config
+   COMMENT: assert \false */
+void main() {
+  int x = 0;
+  if (x) /*@ assert \false; */ ;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/trivial.i b/src/plugins/e-acsl/tests/e-acsl-runtime/false.i~
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/trivial.i
rename to src/plugins/e-acsl/tests/e-acsl-runtime/false.i~
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/not.i b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
new file mode 100644
index 0000000000000000000000000000000000000000..930555b04495575183c5933f99ef92f4b4e2cff9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/not.i
@@ -0,0 +1,7 @@
+/* run.config
+   COMMENT: predicate [!p] */
+void main() {
+  int x = 0;
+  /*@ assert ! \false; */
+  if (x) /*@ assert ! \true; */ ;
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.err.oracle
rename to src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b5118788d6a626bfab0c2fa388ae23e4a9ac66de
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
@@ -0,0 +1,34 @@
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+[value] Recording results for main
+[value] done for function main
+[dominators] computing for function main
+[dominators] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values for function main:
+          x ∈ {0; }
+/* Generated by Frama-C */
+/*@ terminates \false;
+    ensures \false;
+    assigns \nothing;  */
+extern void exit(int status ) ;
+/*@ assigns \nothing;  */
+extern void eprintf(char * ) ;
+void e_acsl_fail(char *msg ) 
+{
+  eprintf(msg);
+  exit(1);
+  return;
+}
+
+void main(void) 
+{
+  int x ;
+  x = 0;
+  if (x) { /*@ assert \false; */ ; e_acsl_fail((char *)"(\\false)"); }
+  return;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/trivial.res.oracle
rename to src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..476bc8a81612754428093f5f0dafb2aa37555d92
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -0,0 +1,35 @@
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+PROJECT_FILE:15:[value] Assertion got status valid.
+[value] Recording results for main
+[value] done for function main
+[dominators] computing for function main
+[dominators] done for function main
+[value] ====== VALUES COMPUTED ======
+[value] Values for function main:
+          x ∈ {0; }
+/* Generated by Frama-C */
+/*@ terminates \false;
+    ensures \false;
+    assigns \nothing;  */
+extern void exit(int status ) ;
+/*@ assigns \nothing;  */
+extern void eprintf(char * ) ;
+void e_acsl_fail(char *msg ) 
+{
+  eprintf(msg);
+  exit(1);
+  return;
+}
+
+void main(void) 
+{
+  int x ;
+  x = 0;
+  /*@ assert \true; */ ;
+  return;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/true.i b/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
new file mode 100644
index 0000000000000000000000000000000000000000..3eb6b45ebe88717428c133908609144e8f8913b9
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/true.i
@@ -0,0 +1,6 @@
+/* run.config
+   COMMENT: assert \true */
+void main() {
+  int x = 0;
+  /*@ assert \true; */
+}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 4bf69d84dd570b56ddcbc11f35a12bc9c18953c0..c3e545b2d88cee3a8855f64d9877887d32f7f318 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -55,11 +55,9 @@ let mk_if acc e p =
   let s = Instr(Call(None, f, [ mkString unknown_loc msg ], unknown_loc))in
   mkStmt(If(e, mkBlock [ mkStmt s ], mkBlock [], unknown_loc)) :: acc
 
-let convert_named_predicate acc generate p =
-  let mk_if e = mk_if acc e p in
-  match p.content with
-  | Pfalse -> if generate then mk_if (one ~loc:unknown_loc) else acc
-  | Ptrue -> if generate then mk_if (zero ~loc:unknown_loc) else acc
+let rec named_predicate_to_revexp p = match p.content with
+  | Pfalse -> one ~loc:unknown_loc
+  | Ptrue -> zero ~loc:unknown_loc
   | Papp _ -> not_yet "logic function application"
   | Pseparated _ -> not_yet "separated"
   | Prel _ -> not_yet "relation"
@@ -68,7 +66,7 @@ let convert_named_predicate acc generate p =
   | Pxor _ -> not_yet "xor"
   | Pimplies _ -> not_yet "==>"
   | Piff _ -> not_yet "<==>"
-  | Pnot _ -> not_yet "!"
+  | Pnot p -> named_predicate_to_revexp p
   | Pif _ -> not_yet "_ ? _ : _"
   | Plet _ -> not_yet "let _ = _ in _"
   | Pforall _ -> not_yet "\\forall"
@@ -81,6 +79,9 @@ let convert_named_predicate acc generate p =
   | Pfresh _ -> not_yet "\\fresh"
   | Psubtype _ -> not_yet "subtyping relation"
 
+let convert_named_predicate acc generate p =
+  if generate then mk_if acc (named_predicate_to_revexp p) p else acc
+
 let convert_annotation acc generate annot = match annot.annot_content with
   | AAssert(_l, p) -> convert_named_predicate acc generate p
   | AStmtSpec _ -> not_yet "stmt spec"