Add additional assertion

Signed-off-by: Wenjie Ma <[email protected]>
anvil-verifier · Aug 25, 2023 · aec117e · aec117e
1 parent 75f5198
commit aec117e
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/controller_examples/rabbitmq_controller/proof/safety.rs b/src/controller_examples/rabbitmq_controller/proof/safety.rs
@@ -359,6 +359,10 @@ proof fn lemma_always_response_at_after_get_stateful_set_step_is_sts_get_respons
                         assert(s.message_in_flight(msg));
                         assert(sts_get_response_msg(key)(msg));
                     },
+                    Step::ExternalAPIStep(input) => {
+                        assert(input.get_Some_0() != msg);
+                        assert(s.message_in_flight(msg));
+                    },
                     _ => {
                         assert(sts_get_response_msg(key)(msg));
                     }