SMT errors when running without /prune

[atomb]

The test file Test/dafny/dafny-issue-4804.dfy introduced in PR #812 results in SMT errors when run without /prune.

$ dotnet Source/BoogieDriver/bin/Debug/net6.0/BoogieDriver.dll /proverOpt:O:auto_config=false /proverOpt:O:type_check=true /proverOpt:O:smt.qi.eager_threshold=100 /proverOpt:O:smt.delay_units=true /rlimit:10000 Test/dafny/dafny-issue-4804.bpl

Prover error: line 6647 column 7: push canceled

Prover error: line 3314 column 60: invalid declaration, constant '$_ModifiesFrame@0' (with the given signature) already declared

Prover error: line 3315 column 26: invalid declaration, constant 'e1#0' (with the given signature) already declared