diff --git a/share/libc/unistd.c b/share/libc/unistd.c
index 3481dfecd31ec365ffb352b0ff77d68674bd56b8..e339084604fedc1922367700b8b2d8e4876886e7 100644
--- a/share/libc/unistd.c
+++ b/share/libc/unistd.c
@@ -36,8 +36,8 @@ int getopt(int argc, char * const argv[], const char *optstring) {
     return -1;
   }
   int nondet_ind = Frama_C_interval(1, argc - 1);
-  int nondet_indlen = Frama_C_interval(0, strlen(argv[nondet_ind]));
-  optarg = Frama_C_nondet_ptr(0, &argv[nondet_ind][nondet_indlen-1]);
+  int nondet_indlen = Frama_C_interval(0, strlen(argv[nondet_ind])-1);
+  optarg = Frama_C_nondet_ptr(0, &argv[nondet_ind][nondet_indlen]);
   optind = Frama_C_interval(1, argc + 1);
   return Frama_C_nondet(-1, Frama_C_unsigned_char_interval(0, UCHAR_MAX));
 }
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 8be076d9a807d2c005dae5b7f1b353568ead1437..57ab4d44afcf9a6fc36b3eda8ce4e28836227c5a 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -8600,11 +8600,10 @@ int getopt(int argc, char * const *argv, char const *optstring)
   }
   int nondet_ind = Frama_C_interval(1,argc - 1);
   tmp_0 = strlen((char const *)*(argv + nondet_ind));
-  tmp_1 = Frama_C_interval(0,(int)tmp_0);
+  tmp_1 = Frama_C_interval(0,(int)(tmp_0 - (size_t)1));
   int nondet_indlen = tmp_1;
   optarg = (char *)Frama_C_nondet_ptr((void *)0,
-                                      (void *)(*(argv + nondet_ind) + (
-                                               nondet_indlen - 1)));
+                                      (void *)(*(argv + nondet_ind) + nondet_indlen));
   optind = Frama_C_interval(1,argc + 1);
   tmp_2 = Frama_C_unsigned_char_interval((unsigned char)0,(unsigned char)255);
   tmp_3 = Frama_C_nondet(-1,(int)tmp_2);
diff --git a/tests/libc/oracle/unistd_c.res.oracle b/tests/libc/oracle/unistd_c.res.oracle
index 89baa32900348d9eab70e3b5c19cc194de764cf5..5321b25be6aec11f2d02be3c0c5e8ff8ff939638 100644
--- a/tests/libc/oracle/unistd_c.res.oracle
+++ b/tests/libc/oracle/unistd_c.res.oracle
@@ -47,17 +47,17 @@
 [eva:final-states] Values at end of function getopt:
   Frama_C_entropy_source ∈ [--..--]
   optarg ∈
-        {{ NULL ; "-this" + {-1; 0; 1; 2; 3; 4} ;
-           "is a" + {-1; 0; 1; 2; 3; 4} ; "Test0" + {-1; 0; 1; 2; 3; 4} }}
+        {{ NULL ; "-this" + {0; 1; 2; 3; 4} ; "is a" + {0; 1; 2; 3; 4} ;
+           "Test0" + {0; 1; 2; 3; 4} }}
   optind ∈ {1; 2; 3; 4; 5}
   nondet_ind ∈ {1; 2; 3}
-  nondet_indlen ∈ {0; 1; 2; 3; 4; 5}
+  nondet_indlen ∈ {0; 1; 2; 3; 4}
   __retres ∈ [-1..255]
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
   optarg ∈
-        {{ NULL ; "-this" + {-1; 0; 1; 2; 3; 4} ;
-           "is a" + {-1; 0; 1; 2; 3; 4} ; "Test0" + {-1; 0; 1; 2; 3; 4} }}
+        {{ NULL ; "-this" + {0; 1; 2; 3; 4} ; "is a" + {0; 1; 2; 3; 4} ;
+           "Test0" + {0; 1; 2; 3; 4} }}
   optind ∈ {1; 2; 3; 4; 5}
   argc ∈ {4}
   argv[0] ∈ {{ "program_name" }}