diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index f9cfa246d8a5669933d08bc833b43e20966e2abf..44868650b2fe56cbef8ca546f02e4993bed86486 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2317,6 +2317,13 @@ struct
          - host is memory access -> check if it is a const field access
       *)
       | TLval (lhost,loff) ->
+        let rec offsets = function
+          | TNoOffset -> true
+          | TIndex (_, n) -> offsets n
+          | TModel (_, n) -> m.accept_models && offsets n
+          | TField (f, n) ->
+            (not (Cil.isConstType f.ftype) || m.accept_const) && offsets n
+        in
         (not (isLogicArrayType t.term_type) || m.accept_array) &&
         (match lhost with
          | TVar v -> begin
@@ -2334,10 +2341,7 @@ struct
            end
          | TResult _ -> m.accept_models
          | _ -> true) &&
-        (match snd (Logic_utils.remove_term_offset loff) with
-         | TModel _ -> m.accept_models
-         | TField(f, _) -> not (Cil.isConstType f.ftype) || m.accept_const
-         | _ -> true)
+        offsets loff
       | TAddrOf lv when is_fct_ptr lv -> m.accept_func_ptr
       | TAddrOf lv | TStartOf lv ->
         m.accept_addrs &&
diff --git a/tests/spec/assignable_location.i b/tests/spec/assignable_location.i
index 70968c3735ad313c5896d7125e9f350e4c4a509d..eac66f9fe9a3551bf4b2c8cb1beab1220f3f072b 100644
--- a/tests/spec/assignable_location.i
+++ b/tests/spec/assignable_location.i
@@ -53,3 +53,22 @@ int * from_address_to_reject(int f){
   //@ behavior rej_1: assigns l \from &lx ;
   return (void*)0 ;
 }
+
+typedef struct _M {
+  int x;
+} M;
+
+struct N {
+  int y;
+};
+
+//@ model M { struct N z; };
+//@ model M { int t; };
+
+M m;
+
+//@ requires x == &m.t;
+void refuse_address_of_model_field(int* x);
+
+//@ requires x == &m.z.y;
+void refuse_subfield_of_model_field(int* x);
diff --git a/tests/spec/assigns_const.i b/tests/spec/assigns_const.i
index b12e589cd954ce0aef0421fc5c9e0dea6ecf9215..add0174e6fe283ae1103c1d98f575f9aa07b9417 100644
--- a/tests/spec/assigns_const.i
+++ b/tests/spec/assigns_const.i
@@ -42,3 +42,14 @@ void accept_partial_const_struct(void)
 {
     z.y = 1;
 }
+
+struct T {
+  const struct Z z ;
+};
+struct T t ;
+
+
+//@ assigns t.z.y ; // y is not const but z is
+void refuse_const_path(void){
+
+}
diff --git a/tests/spec/oracle/assignable_location.res.oracle b/tests/spec/oracle/assignable_location.res.oracle
index 775b7573457de6e89e8f89b34a7728b717a216c2..572a9b7f59133948a6eabf5d9d90b5bfa91fab37 100644
--- a/tests/spec/oracle/assignable_location.res.oracle
+++ b/tests/spec/oracle/assignable_location.res.oracle
@@ -25,3 +25,7 @@
   unbound logic variable l. Ignoring logic specification of function from_address_to_reject
 [kernel:annot-error] tests/spec/assignable_location.i:53: Warning: 
   not an addressable left value: lx. Ignoring code annotation
+[kernel:annot-error] tests/spec/assignable_location.i:70: Warning: 
+  not an addressable left value: m.t. Ignoring specification of function refuse_address_of_model_field
+[kernel:annot-error] tests/spec/assignable_location.i:73: Warning: 
+  not an addressable left value: m.z.y. Ignoring specification of function refuse_subfield_of_model_field
diff --git a/tests/spec/oracle/assigns_const.res.oracle b/tests/spec/oracle/assigns_const.res.oracle
index 3a2391c45fe329f7ca6a743d44a8f7b8254d0d34..31b54355d13d0452923385d4eaca7b001078ab9b 100644
--- a/tests/spec/oracle/assigns_const.res.oracle
+++ b/tests/spec/oracle/assigns_const.res.oracle
@@ -9,6 +9,8 @@
   not an assignable left value: y.a[4].f. Ignoring specification of function refuse_const_field
 [kernel:annot-error] tests/spec/assigns_const.i:25: Warning: 
   not an assignable left value: ptr->a[4].f. Ignoring specification of function refuse_field_via_pointer
+[kernel:annot-error] tests/spec/assigns_const.i:52: Warning: 
+  not an assignable left value: t.z.y. Ignoring logic specification of function refuse_const_path
 /* Generated by Frama-C */
 struct X {
    int const f ;
@@ -20,6 +22,9 @@ struct Z {
    int const x ;
    int y ;
 };
+struct T {
+   struct Z const z ;
+};
 int i;
 int const c;
 /*@ assigns i; */
@@ -38,4 +43,10 @@ void accept_partial_const_struct(void)
   return;
 }
 
+struct T t;
+void refuse_const_path(void)
+{
+  return;
+}
+