diff --git a/tests/jcdb/logic-pp-include/no-stdio.c b/tests/jcdb/logic-pp-include/no-stdio.c
index 78444816bb2ae859c54f7156033ff7df90c39aa0..5dfc21439f01527a4f67a7a1ebcb44a153b668b7 100644
--- a/tests/jcdb/logic-pp-include/no-stdio.c
+++ b/tests/jcdb/logic-pp-include/no-stdio.c
@@ -1,4 +1,6 @@
 // compile_commands.json must have "-includestdio.h" and define ZERO
+
+//@ ensures \result == ZERO;
 int main(){
   printf("bla\n");
   return ZERO;
diff --git a/tests/jcdb/oracle/logic-pp-include.res b/tests/jcdb/oracle/logic-pp-include.res
index a6aedf5c3dda4ac6f804a2708246461654bef1c8..a8432079471806a65084e802c433a6492980d71e 100644
--- a/tests/jcdb/oracle/logic-pp-include.res
+++ b/tests/jcdb/oracle/logic-pp-include.res
@@ -4,6 +4,7 @@
 #include "stdarg.h"
 #include "stddef.h"
 #include "stdio.h"
+/*@ ensures \result ≡ 0; */
 int main(void)
 {
   int __retres;