To do #7600
Hack was used to go around OpenSMT problem in LRA incrementality.
This should be fixed now, so a new LRA solver does not need to be created in each iteration.
Rewrite the method so a single OpenSMT instance is used on LRA level.
Write tests for checking correctness.