We address the problem of verifying safety properties for iterative numerical programs. This problem amounts in, given a program and its specification (a pair of pre and post conditions), to find a strong enough inductive invariant allowing to establish correctness. The verification problem being undecidable in general, our aim is to provide a powerful invariant synthesis method allowing to handle automatically a large number of programs in practice. We propose such a method based on a data-driven approach that is enhanced with symbolic bounded reachability analysis. Our method builds on prior work we published in CAV’22 [6] where we defined an invariant learning procedure based on a new technique for generating relevant decision-tree attributes extracted from convex separators of samples (sets of program states seen as vectors of integers). In this work, we show that by coupling the previous method with a symbolic bounded model checker it is possible to improve significantly performances both in terms of running time and in the number of solved cases. The model checker can help in two ways: it might prove faster that a program is unsafe (by hitting error states), or more interestingly, it can provide interpolants (showing unreachability of error states) which can be used as attributes to speed-up the convergence of the learning procedure. We have implemented our new algorithm and shown that it is quite competitive with state-of-the-art tools such as Spacer, CVC4/5, solving globally more cases than these tools on the SyGuS and SV-COMP benchmarks.