add try in case some precondition fails
add finally to always dispose the z3 context
comment out some logging