CN: Fix free vars for lets in Z3 SMT

[dc-mak]

Commit 2b30e70 introduced a new solver backend for CN. This code included a work-around for Z3 (Z3Prover/z3#7268), which involved calculating free variables for expressions. For (let ((x term)) body), the code correctly looked in body but did not look in term.

This commit fixes that, whilst tidying up some debugging and logging code to make future debugging sessions easier.

It does not include a test because this bug was discovered during the development of a different feature (with file tests/cn/ptr_diff2.c) #494 which will be added in separately, later.

[dc-mak]

For cn verify tests/cn/ptr_diff2.c -p 10 the new output looks like (with -p < 10, it is the same as before).

[0.070180] failed to ack:
(define-fun cn_array_ptr_11 () cn_pointer_2
 (let
  ((a!1
    (bvadd
     (ite ((_ is cn_alloc_id_addr_4) &arr_536) (cn_addr_data_fld &arr_536)
      default_uf_10)
     (bvmul #x0000000000000004 #x0000000000000001))))
  (ite (= a!1 #x0000000000000000) cn_null_3
   (cn_alloc_id_addr_4
    (ite ((_ is cn_alloc_id_addr_4) &arr_536) (cn_alloc_id_data_fld &arr_536)
     default_uf_13)
    a!1))))
[0.070221]
|~~~~~~ Start Solver Dump ~~~~~~~|
# Symbols
# Basetypes
+---------------------------------
# Symbols
| call_f0 |-> call_f0_538
# Basetypes
| alloc_id |-> default_uf_13
+---------------------------------
# Symbols
# Basetypes
+---------------------------------
# Symbols
# Basetypes
+---------------------------------
# Symbols
| &arr |-> &arr_536
# Basetypes
| u64 |-> default_uf_10
+---------------------------------
# Symbols
# Basetypes
+---------------------------------
# Symbols
# Basetypes
+---------------------------------
# Symbols
# Basetypes
+---------------------------------
|~~~~~~ End Solver Dump ~~~~~~~~~|
cn: internal error, uncaught exception:
    UnexpectedSolverResponse((error "line 49 column 6: unknown constant default_uf_10"))
    ...