Which lemmas are destroyed on pop?

[sreeshmaheshwar]

In the following use case (using the default smt engine, not sat and no simplifiers)

 ; Activate solver 2, and add a bunch of assertions
(push) (assert (...)) (assert (...)) (assert (...)) (assert (...))

; Querying a single one repeatedly, surrounded by push/pop
(push) (assert (...)) (check-sat) (pop) 
(push) (assert (...)) (check-sat) (pop)
...

am I actually solving incrementally using prior learned lemmas (I'm pretty sure I am but not concretely sure why)? This https://stackoverflow.com/a/23739636 makes me think that lemmas regarding the asserts at the start are maintained after the pop and so can be reused, but https://stackoverflow.com/a/40427658 makes me think that returning to the frozen state on pop discards all lemmas learnt during (check-sat) (which I'd guess is all of them?).

[NikolajBjorner]

All assertions are removed after pop.

[sreeshmaheshwar]

Sorry, just to clarify then @NikolajBjorner - all lemmas derived during the (check-sat)s are destroyed (even those relevant to the assertions that remain post-pop)?

[sreeshmaheshwar]

I am also wondering whether lemmas are derived on the (assert)s then.

[NikolajBjorner]

It is unsound to keep lemmas and assertions created under a push.