diff --git a/src/kernel_internals/parsing/logic_preprocess.mll b/src/kernel_internals/parsing/logic_preprocess.mll
index 91018631d2efcede80e905a502b411a8b51215c5..fa62499bcecf47ac00171cbd2012916937ce1da0 100644
--- a/src/kernel_internals/parsing/logic_preprocess.mll
+++ b/src/kernel_internals/parsing/logic_preprocess.mll
@@ -434,6 +434,9 @@ and string annot = parse
   | "\\\"" { is_newline:=CHAR;
              Buffer.add_string preprocess_buffer "\\\"";
              string annot lexbuf }
+  | "\\\\" { is_newline:=CHAR;
+             Buffer.add_string preprocess_buffer "\\\\";
+             string annot lexbuf }
   | eof { abort_preprocess "eof while parsing a string literal" }
   | _ as c { is_newline:=CHAR;
              Buffer.add_char preprocess_buffer c;
diff --git a/tests/spec/oracle/preprocess.res.oracle b/tests/spec/oracle/preprocess.res.oracle
index 87f4ad15feb4ee1c94ba44b510f74e0e81ca932a..e1244f0f338b9e14776e4cdc73fd0181c562f916 100644
--- a/tests/spec/oracle/preprocess.res.oracle
+++ b/tests/spec/oracle/preprocess.res.oracle
@@ -13,6 +13,10 @@
 [eva] Recording results for f
 [eva] Done for function f
 [eva] tests/spec/preprocess.c:25: assertion got status valid.
+[eva] tests/spec/preprocess.c:28: 
+  cannot evaluate ACSL term, unsupported ACSL construct: constant strings
+[eva:alarm] tests/spec/preprocess.c:28: Warning: 
+  assertion 'backslash_string' got status unknown.
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -21,3 +25,31 @@
 [eva:final-states] Values at end of function main:
   y_0 ∈ {84}
   __retres ∈ {0}
+/* Generated by Frama-C */
+int x = 1;
+/*@ predicate test(int x) = x ≥ 42;
+ */
+int y = 1;
+/*@ requires x_0 ≥ 42;
+    
+    behavior default:
+      ensures test(\result) ∧ 2 ≡ 2;
+ */
+int f(int x_0)
+{
+  int __retres;
+  __retres = x_0 + 42;
+  return __retres;
+}
+
+int main(void)
+{
+  int __retres;
+  int y_0 = f(42);
+  /*@ assert x ≡ 1; */ ;
+  /*@ assert backslash_string: *("\\" + 0) ≡ '\\'; */ ;
+  __retres = 0;
+  return __retres;
+}
+
+
diff --git a/tests/spec/preprocess.c b/tests/spec/preprocess.c
index f22fa57e73e4e7db835a8ea52069c59e3a6c5033..64b0e62aeec278a03dfd822ddc33e5f539566b1f 100644
--- a/tests/spec/preprocess.c
+++ b/tests/spec/preprocess.c
@@ -1,5 +1,5 @@
 /* run.config
-   OPT: -pp-annot -eva @EVA_CONFIG@ -journal-disable
+   OPT: -eva @EVA_CONFIG@ -journal-disable -print
 */
 
 // see bts 1357
@@ -23,5 +23,8 @@ int f(int x) { return (x + MIN_X); }
 int main() {
   int y = f(MIN_X);
   //@ assert (x) == 1;
+
+  // BTS 2307
+  /*@ assert backslash_string: "\\"[0] == '\\'; */
   return 0;
 }