diff --git a/src/instance/itvAnalysis.ml b/src/instance/itvAnalysis.ml
index adcaa290..bfee5746 100644
--- a/src/instance/itvAnalysis.ml
+++ b/src/instance/itvAnalysis.ml
@@ -128,7 +128,7 @@ let inspect_aexp_bo : InterCfg.node -> AlarmExp.t -> Mem.t -> query list -> quer
     | Memmove (e1, e2, e3, loc) ->
         let v1 = ItvSem.eval (InterCfg.Node.get_pid node) e1 mem in
         let v2 = ItvSem.eval (InterCfg.Node.get_pid node) e2 mem in
-        let e3_1 = Cil.BinOp (Cil.MinusA, e3, Cil.mone, Cil.intType) in
+        let e3_1 = Cil.BinOp (Cil.MinusA, e3, Cil.one, Cil.intType) in
         let v3 = ItvSem.eval (InterCfg.Node.get_pid node) e3_1 mem in
         let lst1 = check_bo v1 (Some v3) in
         let lst2 = check_bo v2 (Some v3) in
diff --git a/src/semantics/itvSem.ml b/src/semantics/itvSem.ml
index f0a49084..28e80928 100644
--- a/src/semantics/itvSem.ml
+++ b/src/semantics/itvSem.ml
@@ -393,7 +393,8 @@ let model_strlen mode spec pid (lvo, exps) (mem, global) =
   | (Some lv, str::_) ->
     let str_val = eval ~spec pid str mem in
     let null_pos = ArrayBlk.nullof (ItvDom.Val.array_of_val str_val) in
-    let v = Val.of_itv (Itv.meet Itv.nat null_pos) in
+    let offset = ArrayBlk.offsetof (ItvDom.Val.array_of_val str_val) in
+    let v = Val.of_itv (Itv.meet Itv.nat (Itv.minus null_pos offset)) in
     (update mode spec global (eval_lv ~spec pid lv mem) v mem, global)
   | _ -> (mem,global)