re-enable extraction of results in SMTBackend.solve, fix examples

[bpowers]

Examples and tests were broken due to trivial changes to APIs (and
renaming of the crate from libsmt -> rustproof_libsmt).

One thing is that this reverts 'bug fix for hanging', which I think
was due to calling '(exit)' twice in the case of a Sat result from
solve(). I think the right thing to do is not call exit at all -- z3
will exit on its own if the write end of its stdin is closed
(returning EOF to z3), as should happen when the rust process exits,
and besides, we might want to iteratively invoke solve (with
appropriate push/pop context calls) on the same z3 instance.

[bpowers]

let me know if you want me to split this up into 2 PRs -- its sort of messy as is.

[arc3x]

This is fine. We will review it this weekend.

Thanks!