Consider the following program, modified from the example in the documentation for gc-terms!

; Creates n unreachable terms of the form (+ a (+ a ...)).
> (define (unused-terms! n)
   (define-symbolic* a integer?)
   (let loop ([n n])
     (if (<= n 1)
         a
         (+ a (loop (- n 1)))))
   (void))
> (time (unused-terms! 50000))
cpu time: 357 real time: 365 gc time: 17
> (gc-terms!)        ; Use gc-terms! to change the representation.
> (collect-garbage)
> (length (terms))
50000

Logically speaking, these 50000 terms should no longer be reachable, so (length (terms)) should ideally return 0. However, it returns 50000 because of the use of parameters (terms), which don't work well with GC. To quote the documentation of parameters (https://docs.racket-lang.org/reference/parameters.html):

as far as the memory manager is concerned, the value originally associated with a parameter through parameterize remains reachable as long the continuation is reachable, even if the parameter is mutated.

In the above example, terms (actually current-terms) is initially a parameter that holds a hash retaining its keys strongly. Even when we assign terms to a hash retaining its keys weakly, the original hash is still unfortunately retained.

One possible fix is to clear the original hash explicitly. Another possibility is to initialize/parameterize current-terms to #f and immediately mutate it to the desired value afterward.