When matching, successive recovery tactics only apply to the original state

[NatKarmios]

Recovery tactics only seem to apply to the initial state in matching, rather than successive recovery tactics "stacking" together on a single state.
I tried to change this (c793e01) but this caused a few test failures:

Gillian-C amazon test

gillian-c verify \
	header.c edk.c array_list.c ec.c byte_buf.c \
	hash_table.c string.c allocator.c \
	error.c base.c \
	--fstruct-passing --no-lemma-proof -l disabled
Parsing and compiling...
Preprocessing...
Obtaining specs to verify...
Obtaining lemmas to verify...
Obtained 39 symbolic tests in total
Running symbolic tests: 6.663270
Verifying lemma FirstProjAppendPair... s s Success
Verifying lemma FirstProjConcatSplit... s s Success
Verifying lemma FirstProjFunction... s s Success
Verifying lemma FirstProjToUtf8MapPairCompat... s s Success
Verifying lemma InListToUtf8... s s Success
Verifying lemma ListToSetFunction... s s Success
Verifying lemma ListToSetUnion... s s Success
Verifying lemma NotInListToUtf8... s s Success
Verifying lemma ProduceListToSet... s s Success
Verifying lemma UniqueConcatSplitNotInSuffix... s s Success
Verifying lemma array_list_content_pref_is_array... s s Success
Verifying lemma edk_array_list_data_is_freeable... s Success
Verifying lemma edk_array_list_data_is_freeable... s s Success
Verifying lemma optBytesConcat... s s s s Success
Verifying lemma toUtf8PairMapAppendPair... s s Success
Verifying lemma toUtf8PairMapInjective... s s s s s s s s s s s Success
Verifying lemma valid_aws_byte_cursor_ptr_facts... s s s Success
Verifying one spec of procedure aws_cryptosdk_algorithm_taglen... s Success
Verifying one spec of procedure aws_cryptosdk_algorithm_taglen... s Success
Verifying one spec of procedure aws_byte_cursor_read... s s s s Success
Verifying one spec of procedure aws_byte_buf_clean_up... s Success
Verifying one spec of procedure aws_byte_buf_clean_up... s s Success
Verifying one spec of procedure aws_byte_cursor_read_u8... s s s Success
Verifying one spec of procedure aws_byte_buf_init... s s Success
Verifying one spec of procedure aws_cryptosdk_algorithm_ivlen... s Success
Verifying one spec of procedure aws_cryptosdk_algorithm_ivlen... s Success
Verifying one spec of procedure aws_cryptosdk_hdr_parse... s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s v v s s v v s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s Success
Verifying one spec of procedure aws_byte_cursor_read_and_fill_buffer... s s s s s s Success
Verifying one spec of procedure aws_byte_cursor_read_be32... s s s Success
Verifying one spec of procedure aws_byte_cursor_read_be16... s s s Success
Verifying one spec of procedure aws_cryptosdk_algorithm_is_known... s Success
Verifying one spec of procedure aws_cryptosdk_algorithm_is_known... s s s s s s s s s s s Success
Verifying one spec of procedure aws_cryptosdk_hdr_clear... s s s s s s s s s s s s s s s s s s Success
Verifying one spec of procedure aws_cryptosdk_enc_ctx_deserialize... f f f f s s f f f f f f f f f f s s Failure
Verifying one spec of procedure aws_cryptosdk_enc_ctx_deserialize... s s Success
Verifying one spec of procedure aws_cryptosdk_enc_ctx_deserialize... s s Success
Verifying one spec of procedure parse_edk... s s s s s s s s s s s s s s s s s s s s s s Success
Verifying one spec of procedure aws_byte_cursor_advance... s s s s s s s s s s Success
Verifying one spec of procedure is_known_type... s s s Success
There were failures: 256.223624
Analysis failures!
1. Couldn't satisfy postcondition
2. Couldn't satisfy postcondition
3. Couldn't satisfy postcondition
4. Couldn't satisfy postcondition
5. Couldn't satisfy postcondition
6. Couldn't satisfy postcondition
7. Couldn't satisfy postcondition
8. Couldn't satisfy postcondition
9. Couldn't satisfy postcondition
10. Couldn't satisfy postcondition
11. Couldn't satisfy postcondition
12. Couldn't satisfy postcondition
13. Couldn't satisfy postcondition
14. Couldn't satisfy postcondition

JaVerT test

Verifying JaVerT examples
-------------------------
Verifying: BST.js
Parsing and compiling...
Preprocessing...
Obtaining specs to verify...
Obtaining lemmas to verify...
Obtained 5 symbolic tests in total
Running symbolic tests: 0.048326
Verifying one spec of procedure insert... s s s s Success
Verifying one spec of procedure remove... s s s s s s s f s Failure
Verifying one spec of procedure findMin... s s Success
Verifying one spec of procedure find... s s s s Success
Verifying one spec of procedure makeNode... s Success
There were failures: 0.398602
Analysis failures!
1. Couldn't satisfy postcondition