diff --git a/src/kernel_services/ast_queries/json_compilation_database.ml b/src/kernel_services/ast_queries/json_compilation_database.ml
index be68e37c853536203978b321ae5d56d7e7ed8646..b176d0032cff8d30cea31fbe32d9b8354a31272f 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ml
@@ -139,7 +139,9 @@ let split_command_args s =
     never need quotes. *)
 let quote_define_argument arg = Format.sprintf "%S" arg
 
-(* Filters and normalize useful flags: -I, -D, -U, ... *)
+(* Filters and normalize useful flags: -I, -D, -U, ...
+   This includes removing extraneous double quotes
+   (when the first and last characters are both '"') *)
 let filter_useful_flags ~requote option_list =
   let convert_define arg =
     if requote then quote_define_argument arg else arg
@@ -150,11 +152,20 @@ let filter_useful_flags ~requote option_list =
     | Define s -> s ^ convert_define suffix
     | Undefine s -> s ^ suffix
   in
+  let remove_extraneous_quotes arg =
+    let len = String.length arg in
+    if len = 0 then arg
+    else
+    if String.get arg 0 = '"' && String.get arg (len-1) = '"' then
+      String.sub arg 1 (len-2)
+    else arg
+  in
   (* we must process the arguments in-order, since several -D and -U may
      exist on the command line *)
   (* prev is the prefix of the previous argument (if any) *)
   let _, res =
     List.fold_left (fun (prev, acc_res) arg ->
+        let arg = remove_extraneous_quotes arg in
         match prev with
         | None -> begin
             match has_whitelisted_prefix arg with
diff --git a/tests/jcdb/compile_commands.json b/tests/jcdb/compile_commands.json
index 0636253c51623f06ae390c688eb0c77254aad822..6a872d8d3670bcaf2eb6ebd07df4edbff04ea962 100644
--- a/tests/jcdb/compile_commands.json
+++ b/tests/jcdb/compile_commands.json
@@ -12,7 +12,7 @@
       "file": "jcdb.c"
     },
     { "directory": ".",
-      "command": "/usr/bin/clang -D'MSG=\"a \\\" \\\"b\"'  -D'SINGLE_DOUBLE(a)=\"a \\\"with spaces and	tab \"' -DSOMEDEF=\"With spaces, quotes and \\-es.\" -D\"DOUBLE_SINGLE(a)=a \\\"macro with spaces and non-escaped \\\\'\\\"\"   -DEMPTY=''  -DEMPTY2= -DTEST=42	 -D'MACRO_FOR_INCR(s)=s+1' -DTOUNDEF -UTOUNDEF",
+      "command": "/usr/bin/clang -D'MSG=\"a \\\" \\\"b\"'  -D'SINGLE_DOUBLE(a)=\"a \\\"with spaces and	tab \"' -DSOMEDEF=\"With spaces, quotes and \\-es.\" -D\"DOUBLE_SINGLE(a)=a \\\"macro with spaces and non-escaped \\\\'\\\"\"   -DEMPTY=''  -DEMPTY2= -DTEST=42	 \"-DTEST2=43\" -D'MACRO_FOR_INCR(s)=s+1' -DTOUNDEF -UTOUNDEF",
       "file": "jcdb.c"
     }
 ]
diff --git a/tests/jcdb/jcdb.c b/tests/jcdb/jcdb.c
index 35173a2f0b1768c90e0b2efa639df5c2f11a4e6a..4a67e650879d0e577cb7a8ac7ddfe2be4a02744e 100644
--- a/tests/jcdb/jcdb.c
+++ b/tests/jcdb/jcdb.c
@@ -22,4 +22,4 @@ int main () {
   #ifndef __FRAMAC__
   printf("%s\n", s); // for GCC debugging
   #endif
-  return MACRO_FOR_INCR(TEST); }
+  return MACRO_FOR_INCR(TEST) - TEST2; }
diff --git a/tests/jcdb/oracle/jcdb.0.res.oracle b/tests/jcdb/oracle/jcdb.0.res.oracle
index e45d2536b38c7c7f50860238749d7a4ea11adcff..701b9f947391a28bed4f7d16394622056bba7d64 100644
--- a/tests/jcdb/oracle/jcdb.0.res.oracle
+++ b/tests/jcdb/oracle/jcdb.0.res.oracle
@@ -13,7 +13,7 @@ int main(void)
 {
   int __retres;
   char *s = (char *)"a macro with spaces and non-escaped \'";
-  __retres = 42 + 1;
+  __retres = (42 + 1) - 43;
   return __retres;
 }
 
diff --git a/tests/jcdb/oracle/jcdb.1.res.oracle b/tests/jcdb/oracle/jcdb.1.res.oracle
index a9218a4af1ffedd9465a9b7b7e0802b52f03cca2..0ded2f0b781283d8f7062ce838c706d29d614685 100644
--- a/tests/jcdb/oracle/jcdb.1.res.oracle
+++ b/tests/jcdb/oracle/jcdb.1.res.oracle
@@ -9,7 +9,7 @@ int main(void)
 {
   int __retres;
   char *s = (char *)"a macro with spaces and non-escaped \'";
-  __retres = 42 + 1;
+  __retres = (42 + 1) - 43;
   return __retres;
 }
 
diff --git a/tests/jcdb/with_arguments.json b/tests/jcdb/with_arguments.json
index 06834b15f346a460ccacc4d57a2018c6f1a73692..038eb7f04346f726b088dff98fe529d42d81bbbd 100644
--- a/tests/jcdb/with_arguments.json
+++ b/tests/jcdb/with_arguments.json
@@ -7,6 +7,7 @@
           "-DEMPTY=",
           "-DEMPTY2=",
           "-DTEST=42",
+          "\"-DTEST2=43\"",
           "-DMACRO_FOR_INCR(s)=s+1",
           "-DSINGLE_DOUBLE(a)=\"a \\\"with spaces and\ttab \"",
           "-DMSG=\"a \\\" \\\"b\"",