BV refinement must not touch the formula before requesting the model

A SAT instance that is satisfiable need not remain so when adding
clauses. Solvers strictly asserting this (such as Cadical) would refuse
getting the model of a satisfiable instance after having added further
clauses since the last solve() call.

Thus, request the values of all approximations first, and only then add
further constraints. Doing so makes cbmc-library/Float-div1-refine pass
again, even when using Cadical.

Author: tautschnig

src/solvers/refinement/bv_refinement_loop.cpp

@@ -123,6 +123,10 @@ void bv_refinementt::check_SAT()
 
   arrays_overapproximated();
 
+  // get values before modifying the formula
+  for(approximationt &approximation : this->approximations)
+    get_values(approximation);
+
   for(approximationt &approximation : this->approximations)
     check_SAT(approximation);
 }

src/solvers/refinement/refine_arithmetic.cpp

@@ -157,9 +157,6 @@ void bv_refinementt::get_values(approximationt &a)
 /// refine overapproximation
 void bv_refinementt::check_SAT(approximationt &a)
 {
-  // get values
-  get_values(a);
-
   // see if the satisfying assignment is spurious in any way
 
   const typet &type = a.expr.type();