Model Reconstruction #20
Description
Currently, model reconstruction via the bv_decide tactic for floats is (1) not easy to read and (2) includes the keywords "potentially spurious" which is not the case because the tactic is unaware that the projections it assigned values to completely determine the value of the float. We should consider improving bv_decide to give readable counterexamples.