Rustproof should return counterexample (call to get-model if SAT)

[selenesal]

[selenesal]

Currently, model is returned but the output is sort of ugly. It would be nice if we could extract the counterexample and format it nicely.

[arc3x]

Are you unhappy with the current printing?

(model 
  (define-fun x () (_ BitVec 32)
    #x7ffffffb)
)

[selenesal]

I'd prefer something like "Example: x = 1235908684i32"

[selenesal]

People who know Rustproof dont' necessarily need to know z3, or its syntax. What's a BitVec 32? Why are there hex strings? What's a define-fun? Rust doesn't have define-funs.

[arc3x]

I agree. Enhancement RFC