[aorai] don't forget to update loop invariant table when fixpoint is reached

... even if it already has an entry: said entry can come from another, unrelated
call.

src/plugins/aorai/aorai_dataflow.ml

@@ -416,9 +416,7 @@ module Computer(I: Init) = struct
       Data_for_aorai.pretty_state old Data_for_aorai.pretty_state cur;
     if Data_for_aorai.included_state cur old then begin
       Aorai_option.debug ~dkey:forward_dkey "Included";
-      if is_loop && Cil_datatype.Stmt.Set.mem stmt loops &&
-         Data_for_aorai.Aorai_state.Map.is_empty
-           (Data_for_aorai.get_loop_invariant_state stmt)
+      if is_loop && Cil_datatype.Stmt.Set.mem stmt loops
       then
         Data_for_aorai.set_loop_invariant_state stmt cur;
       None

src/plugins/aorai/tests/ya/observed.i

@@ -4,7 +4,9 @@
 
 void f(void) {}
 
-void g(void) {}
+void g(void) {
+  for (int i = 0; i < 1; i++) ;
+}
 
 void h(void) {
   g();

src/plugins/aorai/tests/ya/oracle/observed.res.oracle

@@ -183,6 +183,42 @@ void f(void)
  */
 void g(void)
 {
+  /*@ ghost int aorai_Loop_Init_4; */
+  int i = 0;
+  /*@ ghost aorai_Loop_Init_4 = 1; */
+  aorai_loop_4:
+  /*@ loop invariant Aorai: 0 ≡ aorai_intermediate_state;
+      loop invariant
+        Aorai:
+          1 ≡ aorai_intermediate_state_0 ∨
+          0 ≡ aorai_intermediate_state_0;
+      loop invariant Aorai: 0 ≡ final;
+      loop invariant Aorai: 1 ≡ first_step ∨ 0 ≡ first_step;
+      loop invariant Aorai: 0 ≡ init;
+      loop invariant
+        Aorai: 1 ≡ aorai_intermediate_state_0 ∨ 1 ≡ first_step;
+      loop invariant
+        Aorai:
+          aorai_Loop_Init_4 ≢ 0 ⇒
+          \at(1 ≡ aorai_intermediate_state_0,Pre) ⇒ 0 ≡ first_step;
+      loop invariant
+        Aorai:
+          aorai_Loop_Init_4 ≢ 0 ⇒
+          \at(1 ≡ first_step,Pre) ⇒ 0 ≡ aorai_intermediate_state_0;
+      loop invariant
+        Aorai:
+          aorai_Loop_Init_4 ≡ 0 ⇒
+          \at(0 ≡ first_step,aorai_loop_4) ⇒ 0 ≡ first_step;
+      loop invariant
+        Aorai:
+          aorai_Loop_Init_4 ≡ 0 ⇒
+          \at(0 ≡ aorai_intermediate_state_0,aorai_loop_4) ⇒
+          0 ≡ aorai_intermediate_state_0;
+  */
+  while (i < 1) {
+    /*@ ghost aorai_Loop_Init_4 = 0; */
+    i ++;
+  }
   return;
 }