There are currently no regression tests for --refine. See discussion on this PR: https://github.com/diffblue/cbmc/pull/1588 I tried to run the tests in regression/cbmc with --refine, and the test cbmc/Float-div1 seg faults.
