Printing SMT formula or SSA form of a program

[sepideha]

CBMC version: cbmc-5.69.0
Operating system: MacOsBigSur 11.5.2
Exact command line resulting in the issue: ./cbmc --smt2 --outfile formula.smt example.c
What behaviour did you expect: Full SMT formula corresponding to example.c
What happened instead: The body of SMT formula was not printed, only the following headers

cat formula.smt
; SMT 2
; Generated for MathSAT
(set-info :source "Generated by CBMC 5.69.0 (cbmc-5.69.0-dirty)")
(set-option :produce-models true)
(set-logic QF_AUFBV)

Question: How can I dump the SMT formula corresponding to the following example.c
I'm also interested in printing SSA form of this example. Does CBMC have any printing options for these?

 int main(){
    int a=1;
    a=3;
    int* p = &a;
    a=4;
    *p = 5;  //-> a=5;
    a = a+1;
    assert( *p >= 6);
    return *p;  
 }

[tautschnig]

You could use one of --no-propagation or --no-simplify (both of which are intentionally undocumented). The effect of using these will be that we can no longer determine that the property is true without the help of the SMT solver.

For the SSA form use one of --program-only or --show-vcc.

[tautschnig]

Closing, please feel free to re-open in case the above answer was insufficient!